СЕМАНТИКА ПРОГРАММ

Формальная семантика программ – это область теоретической информатики, занимающаяся математическим изучением моделей вычислений и смысла программ.

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

▪ Операционная семантика. Эта семантика связана с интерпретацией предложений программы как процесса вычисления на абстрактных автоматах или вывода в формальных системах;

▪ Денотационная семантика. Эта семантика связана с «компиляцией» программ в математических структурах (а не в других компьютерных языках, как это делается при обычной компиляции);

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

Замечание. На самом деле эта классификация не является четкой: часто используется комбинация этих семантик.

1. ОПЕРАЦИОННАЯ СЕМАНТИКА

Операционная семантика программы выражается в терминах преобразований состояний вычисления, выполняемого этой программы. Рассмотрим примеры.

1. Примеры вычислений, определяемых программой.

Программы для алгоритма Эвклида

Алгоритм Эвклида – это древнейший алгоритм для нахождения наибольшего общего делителя двух натуральных чисел.

Замечание. Эвклид дал формулировку этого алгоритма в геометрии в виде метода для нахождения общей меры двух отрезков.

Обозначим:

▪ N – множество натуральных чисел: 0, 1, 2, 3,…;

▪ x|y _df x – делитель у  ( u) xu=y (x, y, u N);

▪ нод(х,у) = max{z | z|x, z|y} (x, y, z N),

▪ x mod y – остаток от деления х на y (x, y N),

▪ |_z_| – ближайшее целое к вещественному числу z, т.е.

|_z_| = max{x N | x z}.

Очевидно, что

x = y |_x/y_|+ x mod y.

А. Программа для алгоритма Эвклида в языке блок-схем.

Начало

– x<y? +

(x,y) := (y,x)

1 2

(x,y) := (y, x mod y)

+ 3 у =0? –

4

return x

5

Конец

Рис.1

В этой программе входными переменными считаются х и у. Эти же переменные считаются рабочими переменными. Переменная х также считается выходной переменной.

Состояние вычисления по этой программе включает значения рабочих переменных и номер выполняемого в данный момент предложения программы. Кроме того, начальные состояния включают значения входных переменных, а заключительные состояния – значения выходной переменной. В число состояний также зачислим состояние остановки, которое обозначим восклицательным знаком «!». Таким образом множество State_Р всех возможных состояний программы Р состоит из:

▪ начальных (входных) состояний (х,у), где х,у N;

▪ промежуточных состояний (j,x,y), где j {1,2,3,4,5} x,y N;

▪ заключительных (выходных) состояний х N;

▪ состояния остановки «!».

Каждый из операторов программы Р определяет преобразование состояний Т_Р: State_P  State_P (которое будем обозначать просто Т, когда ясно о какой программе идет речь):

Т(x,y) = (1,x,y);

Τ(1,x,y) = (2,x,y), если х<y;

T(1,x,y) = (3,x,y), если x y;

Τ(2,x,y) = (3,y,x);

Τ(3,x,y) = (5,x,y), если у=0;

Т(3,х,у) = (4,x,y), если у 0;

Τ(4,x,y) = (y, x mod y);

Τ(5,x,y) = х;

Т(х) = !

Процесс вычисления можно описать как итерацию применения преобразования T = T_P. Точнее, для входного состояния (a,b) вычисление – это последовательность состояний

Comp_P(a,b): σ₀ = (a,b), σ₁=T(σ₀), σ₂=T(σ₁),…, σ_n= T(σ_n-1), T(σ_n) = c,

Заключительным состоянием является (если программа Р корректна) наибольший общий делитель чисел a и b: c = нод(a,b).

Рассмотрим пример вычисления нод(28,72) по программе Р:

(28,72),

T(28,72) = (1,28,72),

T(1,28,72) = (2,28,72),

T(2,28,72) = (3,72,28),

T(3,72,29) = (4,72,28),

T(4,72,28) = (3,28,16),

T(3,28,16) = (4,16,12),

T(4,16,12) = (3,12,4),

Τ(3,12,4) = (4,4,0),

Τ(4,4,0) = (5,4,0),

Τ(5,4,0) = 4,

Т(4) = !.

Таким образом, получаем, что нод(28,72) = 4.

Итак, имеем следующую последовательность состояний, определяющую вычисление по программе Р для входа х = 28, у =72:

(28,72) |– (1,28,72) |– (2,28,72) |– (3,72,28) |– (4,72,28) |– (3,28,16)

|– (4,16,12) |– (3,12,4) |– (4,4,0) |– (5,4,0) |– 4 |– ! (1.1)

Здесь символ |– обозначает бинарное отношение, определяемое преобразованием τ :

σ |– τ  T(σ) = τ (σ, τ State_P).

Замечание. Ясно, что отношение |– обладает свойством однозначности:

σ |– τ и σ |– τ’ τ = τ’.

Это означает детерминированность программы Р для алгоритма Эвклида. В общем случае отношение |– может быть неоднозначным, что означает недетерминированность программы.

Последовательность (1.1) дает пример вычисления по программе Р для алгоритма Эвклида. Это вычисление было выполнено для входа (28,72).

Пусть Р – произвольная программа в некотором языке и StateP

Обозначим через |–* транзитивное и рефлексивное замыкание бинарного отношения, т.е.

σ |–* τ  ( σ₁, σ₂…., σ_k State_P) σ = σ₁ |– σ₂ |– … |– σ_k = τ, σ |–* σ

для всех σ и τ.

Б. Программа для алгоритма Эвклида в языке с оператором while

Q: if x<y then (x,y) := (y,x) else skip;

while not y=0 do (x,y) := (y,x mod y) od;

return x

Обозначим:

a: (x, y) := (y, x),

b: skip,

c: (x, y) := (y, x mod y).

d: return x,

e: if x < y then (x, y) := (y, x) else skip,

f : while not y=0 do (x, y) := (y, x mod y) od,

Множеством возможных состояний программы Р является

State_Q = {(x, y) | x, y N}

{(p, u, v) | u, v N, p {a, b, c, d, e, f} } N {!}.

Программа Q определяет следующее преобразование Т состояний:

T(u, v) = (е, u, v);

T(е, u, v) = (a, u, v), если u < v;

T(e, u, v) = (b, u, v), если u v;

T(a, u, v) = (f, v, u);

T(b, u, v) = (f, u, v);

T(f, u, v) = (f, v, u mod v), если v 0;

T(f,u,v) = (d,u,v), если v=0;

T(d, u, v) = u;

T(u) = !

Рассмотрим пример вычисления по программе Р, взяв в качестве входа пару чисел (28,72). Применяя последовательно преобразование Т, получим

(28, 72),

T(28, 72) = (e, 28, 72),

T(e, 28, 72) = (a, 28, 72),

T(а, 28, 72) = (f, 72, 28),

T(f,72,28) = (f,28,16),

T(а, 28, 16) = (f, 16, 12),

T(f, 28, 16) = (f, 16, 12),

T(f, 16, 12) = (f, 12, 4),

T(f, 12, 4) = (f, 4, 0),

T(f, 4, 0) = (d, 4, 0),

T(d, 4, 0) = 4,

T(4) = !.

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

(28, 72) |– (e, 28, 72) |– (a, 28, 72) |– (f, 72, 28) |– (f, 28, 16)

|– (f,16,12) |– (f, 12, 4) |– (f, 4, 0) |– (d, 4, 0) |– 4 |– !

Таким образом Процесс вычисления можно описать как итерацию применения преобразования T = T_P. Точнее, для входного состояния (a, b) вычисление – это последовательность состояний

Comp_P(a, b): σ₀ = (a, b), σ₁= T(σ₀), σ₂= T(σ₁),…, σ_n= T(σ_n-1),

T(σ_n-1) = c, T(c)=!

Заключительным состоянием является (если программа Р корректна) наибольший общий делитель чисел a и b: c = нод(a ,b).

1. Ханойская башня

«Ханойская башня» - это игра, состоящая в следующем. Имеется три колышка и 8 дисков различного размера. В начале игры все диски надеты на первый колышек так, как это показано на рис.2. Таким образом, имеем башню, в которой диски лежат по возрастанию их размеров. Цель игры – перенести колышки так, чтобы башня оказалась на втором колышке. При этом должны соблюдать следующие правила игры:

▪ Один ход игры состоит из переноса одного верхнего диска с одного колышка на другой;

▪ Не разрешается класть диск большего размера на диск меньшего размера.

Рис.2

Оказывается, что кратчайшее (по числу шагов) решение игры составляет 2⁸–1 = 127 ходов. В общем случае, когда имеются n дисков , кратчайшее решение игры включает 2ⁿ–1. Например, в случае трех дисков игра имеет следующее решение:

1-й ход: Перенести диск с первого колышка на второй;

2-й ход: Перенести диск с первого колышка на третий;

3-й ход: Перенести диск со второго колышка на третий;

4-й ход: Перенести диск с первого колышка на второй;

5-й ход: Перенести диск с третьего на первый;

6-й ход: Перенести диск с третьего на второй;

7-й ход: Перенести диск со второго колышка на третий

s₀

1 2

s₁

1 2

s₂

2 3

s₃

1 3

s₄

3 1

s₅

3 2

s₆