Часть II. Формальное описание языков программирования ( Формальная спецификация формальных языков ) Операционная семантика

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

Подход Задается система вывода (proof system) Если σ - состояние и e – выражение, что будет результатом вычисления e? -> n для арифметических выражений -> bv для булевских выражений Пусть ae, be: parse trees; n: integer; bv: boolean Если состояние is σ и выполнение оператора c завершается, каково будет результирующее состояние? – -> σ (где c – дерево разбора)

Простой императивный язык 1 ::= skip | := | 2 ; 3 | if then 2 else 3 | while do 2 1 ::= | | | | 2 * 3 1 ::= true | false | 1 = 2 | 1 2 | ¬ 2 | 2 3 | 2 3

Вычисление арифметических выражений a ::= n | X | a0 + a1 | a0 – a1 | a0 * a1 n σ(X) n0 n1 n Аналогично для a0–a1 и a0*a1 Например if σ(P) = 4 и σ(Q) = 6, 10

Правила вывода Семантика задается правилами вывода: задается ноль или большее число предположений (promises) Заключение Условия применимости (задаются справа) Отдельные правила применяются к фрагментам кода, с тем, чтобы «извлечь» доказательство

Вычисление булевских выражений (1) b ::= true | false | a0 = a1 | a0 < a1 | ¬b | b0 b1 | b0 b1 true false n0 n1 true n0 n1 false n0 and n1 are equal n0 and n1 are

Вычисление булевских выражений (2) n0 n1 true n0 n1 false true false false true n0 меньше, чем n1 n0 больше, чем или равен n1

Вычисление булевских выражений (3) t0 t1 t t0 t1 t t равно true iff t0 и t1 равны true t равно false iff t0 и t1 равны false

Выполнение операторов (1) σ[m/X] все значения в σ сохраняются, за исключением X σ[m/X](Y) = σ(Y) если Y не совпадает с X σ[m/X](X) = m то же самое - σ[X m] m σ σ[m/X] σ σ σ

Выполнение операторов (2) true σ σ false σ σ false σ true σ σ σ

Эквивалентность Выражения x и y эквивалентны iff для любых σ и z, z iff z например, a+b эквивалентно b-5+a+5 Операторы (statements) x и y iff для любых σ и σ, σ σ например,c:=a+b; d:=c; эквивалентно d:=b-5+a+5; c:=d; Важно для верификации оптимизирующих компиляторов Оптимизированный код должен быть эквивалентен неоптимизированному.

Пример Loop peeling: доказать, что преобразование while b do c в if b then (c; while b do c) else skip эквивалентно