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

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

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

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

4 Простой императивный язык 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

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

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

7 Вычисление булевских выражений (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

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

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

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

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

12 Эквивалентность Выражения 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; Важно для верификации оптимизирующих компиляторов Оптимизированный код должен быть эквивалентен неоптимизированному.

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