Символическое выполнение и таблицы трассировки.

Одновременное присваивание для оператора BEGIN может быть определено напрямую или через функцию частного значения. Однако, для сложных операторов BEGIN есть необходимость в быстром и аккуратном способе прямого определения одновременного присваивания. Например:

BEGIN

V1 := V2;

V2 := V4;

V3 := V1;

V4 := V3

END

Кажется утомительным использовать для анализа функцию частного значения, прямое определение может дать неверный ответ.

Символическое выполнение – метод трассировки (отслеживания) значений переменных через использование их имен, а не значений. Таблица трассировки – систематический метод проведения символического выполнения.

Подобно таблице выполнения, таблица трассировки имеет строку для каждого выполняемого оператора и столбец для каждой переменной, которая может приобрести новое значение в процессе выполнения. Однако «значения» в трассировочной таблице являются выражениями и строки отслеживают текущие выражения в терминах изначальных выражений. Например, таблица трассировки для приведенного выше оператора BEGIN с четырьмя операторами присваивания будет:

Выражения в столбцах представляют исходные значения соответствующих переменных. Таким образом, перед тем как было выполнено первое присваивание, переменные имели их исходные значения. Но после первого присваивания, (первая строка в таблице, 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 := V2, V2, V2

что эквивалентно:

V1, V3 := V2, V2

Трассировочная таблица для оператора BEGIN

BEGIN

V1 := V4;

V2 := V3;

V3 := V2;

V4 := V1

END

будет:

Полученное одновременное присваивание комментирует оператор BEGIN

BEGIN {V1, V2 := V4, V3}

V1 := V4;

V2 := V3;

V3 := V2;

V4 := V1

END

Может оказаться сюрпризом, что одновременное присваивание показывает, что последние два оператора присвоения не нужны. Обстоятельства могут быть таковы, что программист хотел сделать что-то другое, а нахождение одновременного присваивания выявило ошибку.