6.3. Анализ последовательных выражений

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

Новые идеи: одновременное присваивание, символическое выполнение, трассировочные таблицы

Программное исчисление имеет своей целью вычисление значения P для любой программы P. В основу положен простой принцип, определение значения частей программы с последующей их композицией позволяет получить значение программы в целом. На практике, однако, такое определение значения программы может оказаться утомительно процедурой. В этом разделе даются упрощенные (стенографические) методы, которые делают практический анализ программ проще.

6.3.1. Одновременные присваивания.

Оператор BEGIN может присвоить значение более чем одной переменной. Возможность обобщения эффекта оператора BEGIN настолько важна, что она будет сделана в виде комментария к CF Pascal, называемого одновременным присваиванием (concurrent assignment).

Паскаль-машина не имеет возможности выполнять одновременные присваивания – они не являются частью синтаксиса Паскаля. Однако, в формате комментария будет присутствовать как простое расширение оператора присваивания CF Pascal. Список переменных, встречающихся слева от оператора присваивания и список выражений встречающихся справа, оба эти списка одинаковой длины. Одновременное присваивание выражает знание, что выражения, вычисленные одновременно, являются значениями соответствующих переменных. Например, результат выполнения оператора BEGIN:

BEGIN

V1 := ‘A’;

V2 := ‘B’

END

Может быть представлен одновременным присваиванием:

<V1, V2> := <’A’, ‘B’>

Тогда как результат выполнения оператора

BEGIN

V1 := ‘A’;

V2 := ‘B’

END

будет представлен:

<V1 > := <‘B’>

Угловые скобки списков могут быть опущены, если это не вызовет путаницы, например:

V1, V2 := ’A’, ‘B’

С использованием одновременного присваивания получаются отличные комментарии, потому что они точно выражают, каков должен быть результат оператора BEGIN.

Например:

BEGIN {V1 := ‘B’}

V1 := ‘A’;

V2 := ‘B’

END

Комментарий уточняет, что такая конструкция сделана намеренно, а не по ошибке.

Для любых символов x, y, z

BEGIN V3 := V2; V2 : V1 END ({V1x, V2y, V3z, …}) = {V1x, V2x, V3y, …}

Одновременное присваивание

BEGIN

V3 := V2;

V2 := V1

END

Может быть представлено в комментированной версии:

BEGIN {V2, V3 := V1, V2}

V3 := V2;

V2 := V1

END

Преимущество одновременного присваивания над частным значением то, что в нем присутствуют только измененные переменные. Другие переменные могут присутствовать в состоянии выполнения, но если они не появляются в левой части одновременного присваивания, их значение не меняется.

Одновременные присваивания помогают определить значение части программы. Примеры операторов BEGIN приведенные выше были простыми, рассмотрим другие:

E	F
BEGIN V1 : V2; V2 := V3; V3 := V1 END	BEGIN V1 : V2; V3 := V1; V2 := V3 END

Второе и третье присваивания поменяли местами. Мы можем вычислить фугкции частного значения для E и F, принимая x, y, z – любые символы.

E({V1x, V2y V3z, …})

= (V1 := V2◦V2 := V3◦V3 := V1)({V1x, V2y V3z, …})

= (V2 := V3◦V3 := V1)({V1y, V2y V3z, …})

= (V3 := V1)({V1y, V2z V3z, …})

= {V1y, V2z V3y, …}

и

F({V1x, V2y V3z, …})

= (V1 := V2◦V3 := V1◦V2 := V3)({V1x, V2y V3z, …})

= (V3 := V1◦V2 := V3)({V1y, V2y V3z, …})

= (V2 := V3)({V1y, V2y V3y, …})

= {V1y, V2y V3y, …}

В E совокупный эффект - уничтожение старого значения V1 и обмен значениями V2 и V3, что обобщается одновременным присваиванием:

V1, V2, V3 := V2, V3, V2

F имеет несколько иное значение, а именно – присвоить всем переменным изначальное значение V2:

V1, V3 := V2, V2

Добавление к операторам BEGIN комментариев с одновременным присваиванием делает их понимание более ясным:

E	F
BEGIN {V1, V2, V3 := V2, V3, V2} V1 : V2; V2 := V3; V3 := V1 END	BEGIN {V1, V3 := V2, V2} V1 : V2; V3 := V1; V2 := V3 END

E – пример часто встречающегося блока, который обменивает значения V2 и V3, используя V1 как переменную для сохранения промежуточного значения. Такие блоки как F обычно пишутся по ошибке.