- •6. Исчисление последовательных программ.
- •Часть 6 развивает изложение программного исчисления для последовательных программ, что позволяет нам сформулировать правила проектирования операторов begin, которые выполняются корректно.
- •6.1. Значение частей программы.
- •6.1.1. Состояния выполнения.
- •6.1.2. Значение заголовка программы и точки.
- •6.1.3. Композиция отношений и функций.
- •6.1.4. Значение объявлений.
- •6.1.5. Значение блоков.
- •6.2.1. Оператор присвоения.
- •6.2. Значение последовательных выражений.
- •6.2.2. Пустой оператор.
- •6.2.3. Оператор begin
- •6.2.4. Оператор write.
- •6.2.5. Оператор read
- •6.2.6. Простые процедуры.
- •6.3. Анализ последовательных выражений
- •6.3.1. Одновременные присваивания.
- •6.3.2. Символическое выполнение и таблицы трассировки.
6.3.2. Символическое выполнение и таблицы трассировки.
Одновременное присваивание для оператора BEGIN может быть определено напрямую или через функцию частного значения. Однако, для сложных операторов BEGIN есть необходимость в быстром и аккуратном способе прямого определения одновременного присваивания. Например:
BEGIN
V1 := V2;
V2 := V4;
V3 := V1;
V4 := V3
END
Кажется утомительным использовать для анализа функцию частного значения, прямое определение может дать неверный ответ.
Символическое выполнение – метод трассировки (отслеживания) значений переменных через использование их имен, а не значений. Таблица трассировки – систематический метод проведения символического выполнения.
Подобно таблице выполнения, таблица трассировки имеет строку для каждого выполняемого оператора и столбец для каждой переменной, которая может приобрести новое значение в процессе выполнения. Однако «значения» в трассировочной таблице являются выражениями и строки отслеживают текущие выражения в терминах изначальных выражений. Например, таблица трассировки для приведенного выше оператора BEGIN с четырьмя операторами присваивания будет:
-
V1
V2
V3
V4
V1 := V2
V2 := V4
V3 := V1
V4 := V3
V2
V2
V2
V2
V2
V4
V4
V4
V3
V3
V2
V2
V4
V4
V4
V2
Выражения в столбцах представляют исходные значения соответствующих переменных. Таким образом, перед тем как было выполнено первое присваивание, переменные имели их исходные значения. Но после первого присваивания, (первая строка в таблице, V1 приняла значение, которое изначально имела V2, и это показано значением V2 в столбце V1. Остальные переменные не были изменены, их значения соответствуют заголовкам столбцов. Во второй строке V2 приобрела значение V4 (которое на тот момент было ее исходным значением). В третьей строчке V2 приходит в столбец V3 из столбца V1, потому что V3 принимает текущее значение V1, которое уже равно оригинальному значению V2.
Правило таково, что в таблице используются только оригинальные значения, но имена переменных всегда доступны в верхней строчке.
Одновременное присваивание для оператора BEGIN может быть записано прямо из трассировочной таблицы, используя список идентификаторов в заголовке таблицы в левой части и список в последней строчке таблицы в правой части. Для примера выше одновременное присваивание будет:
V1, V2, V3, V4 := V2, V4, V2. V2
Таблица трассировки упрощается, если мы опустим неизменяемые значения. Для приведенного выше примера с некорректной попыткой обменять значения V2 и V3 получим таблицу выполнения:
-
V1
V2
V3
V1 := V2
V3 := V1
V2 := V3
V2
V2
V2
С одновременным присваиванием:
V1, V2, V3 := V2, V2, V2
что эквивалентно:
V1, V3 := V2, V2
Трассировочная таблица для оператора BEGIN
BEGIN
V1 := V4;
V2 := V3;
V3 := V2;
V4 := V1
END
будет:
-
V1
V2
V3
V4
V1 := V4
V2 := V3
V3 := V2
V4 := V1
V4
V3
V3
V4
Полученное одновременное присваивание комментирует оператор BEGIN
BEGIN {V1, V2 := V4, V3}
V1 := V4;
V2 := V3;
V3 := V2;
V4 := V1
END
Может оказаться сюрпризом, что одновременное присваивание показывает, что последние два оператора присвоения не нужны. Обстоятельства могут быть таковы, что программист хотел сделать что-то другое, а нахождение одновременного присваивания выявило ошибку.