Лекции по СЯП (Лекции по СЯП)

Посмотреть архив целиком







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





























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

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

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

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

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

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










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, zN),

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

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

|_z_| = max{xN | xz}.

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

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,yN;

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

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

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

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

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

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

Τ(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 = TP. Точнее, для входного состояния (a,b) вычисление – это последовательность состояний

CompP(a,b): σ0 = (a,b), σ1=T(σ0), σ2=T(σ1),…, σ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(σ) = τ (σ, τ StateP).

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

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

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

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

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

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

σ |–* τ (σ1, σ2…., σk StateP) σ = σ1 |– σ2 |– … |– σk = τ, σ |–* σ

для всех σ и τ.

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

Q: if xthen (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,

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

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

{(p, u, v) | u, vN, 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 = TP. Точнее, для входного состояния (a, b) вычисление – это последовательность состояний

CompP(a, b): σ0 = (a, b), σ1= T(σ0), σ2= T(σ1),…, σn= T(σn-1),

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

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


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


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

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

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


Рис.2


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

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

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

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

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

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

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

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



s0

12


s1

12


s2

23


s3




13

s4


31


s5



32



s6




12



s7




Рис.3



На рис.3 показана последовательность ситуаций, определяющей кратчайшее решение игры. Каждую из ситуаций можно представить тройкой. Например, начальную ситуацию s0 можно представить тройкой (123,ε,ε), а ситуации s5 и s6 – тройками (1,3,2) и (1,23,ε). (Здесь ε обозначает пустое слово.)

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

(i1i2ip, j1j2jq, k1k2kr),

где i1, i2,…, ip – номера дисков, находящихся на первом колышке, j1, j2,…, jp номера дисков, находящихся на втором колышке, k1, k2,…,kp – номера дисков, находящиеся на третьем колышке. Мы здесь предполагаем, что диски пронумерованы в порядке их размера и i1<i2<…< ip, j1< j2<…< jp, k1<k2<…<kp. (Заметим, что {i1, i2,…, ip}{j1, j2,…, jp}{k1, k2,…,kp} и эти множества попарно не пересекаются.)

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

(123,ε,ε) <12> (23,1,ε) <13> (3,1,2) <23> (3,ε,12) <12>

(ε,3,12) <31> (1,3,2) <32> (1,23,ε) <12> (ε,123,ε)


(1,ε,ε)



(ε,ε,1) (ε,1,ε)








(12,ε,ε)

13

(2,1,ε) (2,ε,1)


12

(ε,1,2) (ε,2,1)

32

(ε,ε,12) (ε,12,ε)

(1,ε,2) (1,2,ε)


(123,ε,ε)

12

(23,1,ε)


13

(3,1,2)

23

(3,ε,12)

12

(ε,3,12)

31

(1,3,2)

31

(1,23,ε)

12

(ε,123,)

Рис.4


Обозначим через h(n,i,j) решение задачи, т.е. кратчайшую последовательность шагов от состояния (12…n, ε, ε) к состоянию (ε, ε ,12…n). Каждый ход представляется парой вида <ij>, которая указывает, что нужно перенести диск с колышка номер i на колышек номер j. Таким образом, последовательность шагов представляется словом в алфавите

{<12>, <13>, <21>, <23>, <31>, <32>}.

Решение задачи для трех дисков представляется словом

h(3,1,2) = <12> <13> <23> <12> <31> <31> <12>

Ясно, что

h(n,1,2) = h(n1,1,3) <12> h(n1,3,2).

Вообще, для произвольных i, j (ij)

h(n,i,j) = h(n–1, i, t(i,j)) <i j> h(n–1, t(i,j) ,j)

Таким образом, имеем следующую рекурсивную программу:


R: h(n,1,2) <= h(n–1,1,3) <12> h(n–1,3,2)

h(n,1,3) <= h(n–1,1,2) <13> h(n–1,2,3)

h(n,2,1) <= h(n–1,2,3) <21> h(n–1,3,1)

h(n,2,3) <= h(n–1,2,1) <23> h(n–1,1,3)

h(n,3,1) <= h(n–1,3,2) <31> h(n–1,2,1)

h(n,3,2) <= h(n–1,3,1) <32> h(n–1,1,2)

h(1,1,2) <= 12

h(1,1,3) <= 13

h(1,2,1) <= 21

h(0,2,3) <= 23

h(0,3,1) <= 31

h(0,3,2) <= 32


Пример. Применим эту программу для того, чтобы решить задачу «Ханойская башня» для трех дисков.


h(3,1,2) (1)

h(31,1,3)<12>h(31,3,2) (2)

h(2,1,3)<12>h(2,3,2) (3)

h(21,1,2)<13>h(21,2,3)<12>h(21,2,1)<23>h(21,1,3) (4)

h(1,1,2)<13>h(1,2,3)<12>h(1,2,1)<23>h(1,1,3) (5)

<12><13><23><12><21><23><13> (6)


Оценка вычислительной сложности программы R.

Операции программы: <= (подстановка), –1 (вычитание единицы).

Функция tR((n,1,2)) – число операций, выполненной программой R при ее применении к ситуации (n,1,2). Рассматривая протокол вычисления программы R для указанного примера, мы замечаем, что выполняются:

1 операция «<= » при переходе от (1) к (2);

2 операции «–1» при переходе от (2) к (3);

2 операции «<= » при переходе от (3) к (4);

4 операции «–1» при переходе от (4) к (5);

4 операции «<= » при переходе от (5) к (6).

Таким образом,

tR((3,1,2)) = 1+2+2+4+4 = 9.

Рассмотрим теперь протокол вычисления для входа (4,1,2).

h(4,1,2) (1)

h(41,1,3)<12>h(41,3,2) (2)

h(3,1,3)<12>h(3,3,2) (3)

h(31,1,2)<13>h(31,2,3)<12>h(31,2,1)<23>h(31,1,3) (4)

h(2,1,2)<13>h(2,2,3)<12>h(2,2,1)<23>h(2,1,3) (5)

h(21,1,3)<12>h(21,3,2)<13>h(21,2,1)<23>h(21,1,3)

<12>h(21,2,3)<21>h(21,3,1)<23>h(21,1,2)

<13> h(21,2,3) (6)

h(1,1,3) <12>h(1,3,2)<13>h(1,2,1)<23>h(1,1,3)

<12>h(1,2,3)<21>h(1,3,1)<23>h(1,1,2)

<1