Денотационная семантика

Целью денотационной семантики является определение для каждой синтаксической категории так называемой семантической функции, которая сопоставляет каждой синтаксической категории реализуемые ей функции. Пусть D обозначает множество значений, с которыми работает программа. В нашем случае это множество целых чисел. Пусть X обозначает множество всех возможных имён переменных. Состоянием памяти в нашем языке можно считать частичное отображение вида

M: X → D

сопоставляющее имени некоторое значение. Тогда вычисление выражения осуществляет отображение вида M → D, а вычисление оператора и последовательности операторов - отображение вида M → M. Семантическую функцию, сопоставленную конструкции s, мы будем обозначать Sem [ s ][8]. Для определения семантики мы воспользуемся структурной индукцией, то есть семантика сложной конструкции будет определяться через семантику её составных частей. Для вычисления выражений семантическая функция задаётся следующими правилами.

    Вычисление константы просто извлекает это значение из дерева абстрактного синтаксиса:

Sem [(конст знач: val)](M) = val

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

Sem [(перем имя: name)](M) = M (name)

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

Sem [(биноп оп: op левое: lhs правое: rhs)](M) =

              = Func (op) (Sem [ lhs ](M), Sem [ rhs ](M))

Для обычных арифметических операций функция Func определена естественным образом, например, Func (+)(x, y) = x + y. Однако, надо понимать, что хотя оба "+" в этом равенстве выглядят совершенно одинаково, в первом случае это некоторый код операции, а во втором - абстрактная математическая функция. Для логических операций Func определена несколько сложнее, поскольку у нас в языке нет булевых значений, например,

    Func (>) (x, y) = если x > y то 1 иначе 0

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

Sem [{}](M) = M

Для вычисления непустой последовательности операторов надо выполнить первый оператор и вычислить остальные операторы на новом состоянии памяти:

Sem [{ stat...}](M) = Sem [{...}] (Sem [ stat ] (M))

Для вычисления присваивания необходимо вычислить значение источника присваивания, а новое состояние памяти отличается от данного только для переменной-получителя:

Sem [(присв получатель: var источник: expr)](M) =

              = M [ var => Sem [ expr ](M)]

Вычисление условного оператора начинается с вычисления условия и затем сводится к вычислению либо то-, либо иначе части в зависимости от того, отлично ли от нуля полученное значение:

Sem [(if условие: cond то: then_seq иначе: else_seq)] =

              = если Sem [ cond ](M)!= 0

              то Sem [ then_seq ](M)

              иначе Sem [ else_seq ](M)

Если при вычислении цикла условие оказалось ненулевым, то цикл возвращает данное состояние памяти. В противном случае, необходимо вычислить тело цикла, получить новое состояние памяти и снова применить к нему семантику цикла:

Sem [(while условие: cond тело: seq)] (M) =

              = если Sem [ cond ](M)!= 0

              то M

              иначе Sem [(while условие: cond тело: seq)] (Sem [ seq ] (M))

Заметим, что это последнее определение некорректно, поскольку оно нарушает принцип структурной индукции и определяет семантику цикла через саму себя. К решению этой проблемы можно подойти следующим образом. Обозначим

f = Sem [(while условие: cond тело: seq)]

Тогда определение можно трактовать так, что f не изменятся в результате следующего преобразования

f = если Sem [ cond ](M)!= 0 то M иначе f (Sem [ seq ] (M))

Функций f, удовлетворяющих этому условию, может быть бесконечно много, и нам необходимо выбрать самую "информативную" из них. Это достигается с помощью оператора неподвижной точки, который обычно обозначается fix и находит для любого монотонного функционала F наименьшую неподвижную точку, то есть, если f = fix (F), то f = F (f). Функционал F в нашем случае определяется как

F (f)(M) = если Sem [ cond ](M)!= 0 то M иначе f (Sem [ seq ] (M)).

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

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

n=n/2;

Для краткости будет записывать вместо абстрактного синтаксиса конструкций сами конструкции. Тогда

Sem [n=n/2;](M) =

= M [n => Sem [n/2](M)] =

= M [n => Func (/) (Sem [n](M), Sem [2](M))] =

= M [n => M(n) /  2]

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