Операционная семантика

Операционная семантика объясняет смысл программы в терминах исполнения так называемой языковой машины. Для того, чтобы работа этой машины была понятна, она должна быть либо определена как формальная вычислительная модель (например, машина Тьюринга), либо иметь достаточно точное и полное описание. Определим языковую машину для нашего модельного языка. Состояние этой машины будет содержать:

1. текущую точку исполнения программы, которую будем изображать символом @. Поскольку программа представлена в виде дерева абстрактного синтаксиса, то точка исполнения должна быть привязана к некоторой вершине. Мы будем допускать положение точки исполнения как перед, так и после вершины. Например,

    @ (биноп оп:">"

              левое: (перем имя:"n") правое:(конст знач: "0"))

будет означать, что машина собирается вычислять применение бинарной операции,

      (биноп оп:">"

              левое: (перем имя:"n")@

                   правое:(конст знач: "0"))

- закончилось вычисление левого подвыражения и надо переходить к вычислению правого и т.п.;

2. состояние памяти обрабатываемой программы;

3. дополнительные атрибуты, которые можно задавать для вершин дерева абстрактного синтакиса. Например, для вершины-выражения мы можем определить дополнителный атрибут "результат" целого типа.

Описание операционной семантики заключается в наборе правил, переводящих текущее состояние языковой машины в следующее. Далее мы будем обозначать текущее состояние памяти обрабатываемой программы М, а следующее состояние памяти M '.

При вычислении константы в атрибут-результат дублируется хранящееся в вершине значение, и текущая точкая переставляется в конец выражения:

@((конст знач: val))

              => ((конст знач: val результат: val) @

При вычислении переменной в результат помещается значение, извлекаемое по имени переменной из памяти[9], и текущая точка переставляется в конец выражения

@(перем имя: name)

              => (перем имя: ­name результат:M(name)) @

Для вычисления бинарной операции сначала точка управления переставляется в начало левой части:

@(биноп оп: op левое: lhs правое: rhs)

              => (биноп оп: op левое:@ lhs правое: rhs)

Когда точка управления оказалась в конце левой части, переставляем её в начало правой:

(биноп оп: op левое: lhs @ правое: rhs)

              => (биноп оп: op левое: lhs правое: @ rhs)

Когда же точка управления оказалась в конце правой части, то извлекаются сохранённые значения аргументов, удаляется атрибут-результат из вершин-подвыражений, вычисляется и добавляется атрибут-результат ко всему выражению, и точка управления переставляется в его конец:

 (биноп оп: op левое:(....результат: lval) правое:(... результат: rval) @)

              => (биноп оп: op левое:(....) правое: (...)

                       результат: Func (op)(lval, rval)) @

Вычисление пустой последовательности операторов состоит просто в перестановке точки управления за эту последовательность:

@{} => {}@

Если последовательность не пуста, то точка управления помещается перед первым оператором последовательности:

@{S...} => {@S...}

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

{...S1@ S2...} => {... S1 @S2...}

После выполнения последнего оператора вся последовательность операторов считается законченной:

{... S@} => {... S}@

Вычисления оператора присваивания начинается с вычисления источника:

@ (присв получатель: var источник: expr)

              => (присв получатель: var источник: @ expr)

По завершению вычисления источника изменяется текущее состояние памяти и точка управления переставляется в конец оператора:

 (присв получатель: var источник:(... результат: val) @)

  =>   (присв получатель: var источник:(...)) @

                                 и положить M ' = M [ var => val ]

Вычисление условного оператора начинается с выполнения условия:

@(if условие: cond то: then_seq иначе: else_seq)  

              => (if условие:@ cond то: then_seq иначе: else_seq) 

По завершению выполнения условия точка управления переставляется в начало либо то-, либо иначе-части:

 (if условие:(... результат: val) @ то: then_seq иначе: else_seq) 

              = если val!= 0

              то  (if условие:(...) то:@ then_seq иначе: else_seq)

              иначе (if условие:(...) то: then_seq иначе:@ else_seq)

Когда завершается выполнение то- или иначе-части, завершается выполнение всего условного оператора:

(if условие: cond то: then_seq@ иначе: else_seq)  

              => (if условие: cond то: then_seq иначе: else_seq)@

(if условие: cond то: then_seq иначе: else_seq@)  

              => (if условие: cond то: then_seq иначе: else_seq)@

Аналогично, для выполнения цикла сначала надо вычислить условие:

@(while условие: cond тело: seq)

              => (while условие: @ cond тело: seq)

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

(while условие:(... результат: val)@ тело: seq)

              => если val!= 0

              то (while условие:(...) тело:@ seq)

              иначе (while условие:(...) тело: seq)@

Наконец, после завершения тела цикла, точка управления переставляется в начало условия:

(while условие: cond тело: seq@)

              => (while условие:@ cond тело: seq)

В отличие от денотационной семантики нам не пришлось использовать оператор неподвижной точки. Однако, очевидно, что выполнение программы может быть бесконечным и точка управления никогда не достигнет её конца.

Отметим, что операционная семантика оказалась более сложной, чем денотационная, в частности, ввиду неочевидного перемещения точки управления по выражениям. От этого можно было бы избавиться, разбив сложные выражения, считая их своего рода синтаксическим сахаром. По-существу, мы осуществим промежуточную трансляцию в подъязык, в котором не остаётся выражений.

программа::= оператор*

оператор::= (while условие:строка тело:оператор*)

                       | (if условие:строка то:оператор* иначе:оператор*)

                       | (инициализация имя:строка знач:число)

                       | (пересылка получатель:строка источник:строка)

                       | (операция получатель:строка источник:строка)

                       | (биноп получатель:строка

                                 оп:(+,-,...) левое:выр правое:выр)

Исходная программа может быть легко преобразована в следующую:

r0 = 0;

r1 = n>r0;

while (r1)

{

 r2 = 2; r3=n%r2;

if (r3)

  y = y*x;

x = x*x;

n = n / r2;

 r1 = n>r0;

}

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