2.2. ЕСТЕСТВЕННЫЙ МЕТОД ОПИСАНИЯ СЕМАНТИКИ

Для описания процесса выполнения программ на Рефале Плюс будет использован метод, известный под названием "естественная семантика" или "структурная операционная семантика" [Плоткин 1983] , [Апт 1983] .

Название "естественная семантика" объясняется сходством этого метода описания с генценовским естественным выводом в математической логике. При таком способе описания, семантикой языка является неупорядоченное множество утверждений о программах и фрагментах программ.

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

Env,St' |- E => X,St"

где E - выражение языка, Env - среда, которая связывает переменные с их значениями в том контексте, в котором находится E, St' и St" - глобальное состояние до начала вычисления E и после вычисления E, а X - результат вычисления E. Глобальное состояние может включать состояние памяти, состояние файлов и т.п.

Смысл таких утверждений неформально может быть истолкован следующим образом: если вычисление выражения E начинается в среде Env и глобальном состоянии St', оно может завершиться получением значения X в глобальном состоянии St".

Знак "|-" (который можно читать как "влечет" или "вызывает") служит напоминанием о том, что результат вычисления выражения E зависит от среды Env, в которой вычисляется выражение, ибо это выражение может содержать переменные.

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

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

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

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

Например, предположим, что в описываемом языке имеется конструкция

if E then E' else E"

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

Вычислить E. Если получится true, то вычислить E' и полученный результат считать результатом вычисления всей конструкции. Если же в результате вычисления E получилось false, то вычислить E" и полученный результат считать результатом вычисления всей конструкции.

Недостатком такого описания является то, что мы забыли указать, в какой среде происходит вычисление каждого из выражений E, E' и E". Поэтому переформулируем описание более точно.

Если результатом вычисления выражения E в среде Env является true, а результатом вычисления выражения E' в среде Env является X, то X является результатом вычисления конструкции

if E then E' else E" в среде Env.

Если результатом вычисления выражения E в среде Env является false, а результатом вычисления выражения E" в среде Env является X, то X является результатом вычисления конструкции

if E then E' else E" в среде Env.

Это многословное определение можно записать в более краткой и наглядной форме в виде двух правил вывода:

Env,St |- E => true,St'

Env,St'|- E' => X,St"

---------------------------------------

Env,St |- if E then E' else E" => X,St"

 

Env,St |- E => false,St'

Env,St'|- E" => X,St"

---------------------------------------

Env,St |- if E then E' else E" => X,St"

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