Лекции по СЯП (987656), страница 3

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 3)

В этом языке каждый оператор можно рассматривать как программу, т.е. на самом деле Prog = Stm.

Метапеременные:

v, v’, v₁, v₂ Var; n Num; m Int; a, a₁, a₂ Aexp; b, b₁, b₂ Bexp; S, S₁, S₂ Stm.

Грамматика:

n ::== 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 | 1n | 2n | 3n | 4n | 5n | 6n | 7n | 8n | 9n

m ::== n | -n

v ::== x | y | z | x_n | y_n | z_n

a ::== v | m | a₁+a₂ | a₁–a₂ | a_1*a₂

b ::== true | false | not b | b₁ and b₂ | b₁ or b₂

S ::== v:=a | (v₁,v₂):=(a₁,a₂) | skip | if b then S₁ else S₂ | while b do S od

| S₁ ; S₂ | return v

Семантика языка L

Пусть α – выражение языка L, т.е.

α Var Num Int Aexp Bexp Stm.

Через [α] обозначим смысл (семантику) выражения α, который будет математическим объектом – числом или функцией, заданной на состояниях.

Пусть L – конечное множество переменных, L ={x₁, x₂,…, x_p}. Состоянием для переменных L назовем произвольную функцию σ, заданную на L и принимающую значения в множестве Z целых чисел, σ: L Z. Обозначим State_L= {σ | σ: L Z}.

Замечание. Следует различать множества Z и Int: элементами первого множества служат математические (абстрактные) объекты – целые числа (нуль, положительные и отрицательные числа), а второе множество состоит из конкретных объектов – слов в алфавите {– , 0, 1, 2, 3, 4, 5, 6, 7, 8. 9}. На самом деле эти слова являются представлениями целых чисел в десятичной системе счисления.

Предположим, что выражение α имеет переменные, которые все входят в L. Тогда смыслом выражения α будет некоторая функция |[α]|, заданная на множестве State_L.

Семантика нумералов и нумералов со знаком минус:

|[0]| = 0 (слева стоит нумерал 0, справа число 0),

|[1]| = 1,

|[2]| = 2,

………

|[9]| = 9,

|[1n]| = |[n]| + 10^k (k – длина слова n),

|[2n]| = |[n]| + 2 •10^k,

………

|[9n]| = |[n]| + 9 •10^k,

|[–n] = – |[n]|,

Пример. Для нумерала 256 имеем:

|[256]| = |[56]| + 2 •10² = |[6]| + 5 •10+2 •10² = 6+5 •10+2 •10² .

Предположим, что все входящие в выражение α переменные, содержатся в L. Тогда смыслом выражения α будет некоторая функция |[α]|, заданная на множестве State_L. При этом, для любого σ State_L:

▪ если α – арифметическое выражение, то значение |[α]|(σ) принадлежит Z;

▪ если α – арифметическое выражение, то это значение является булевым;

▪ если α – оператор (программа), отличный от оператора return, то

|[α]|(σ) State_L;

▪ |[return v]|(σ) = σ(v).

Семантика арифметических выражений:

|[n]|(σ) = |[n]| = n,,

|[ – n]|(σ) =|[ – n]| = – |[n]| = – n,·

|[v]|(σ) = σ(v),

|[a₁+a₂]|(σ) = |[a₁]|(σ) + |[a₂]|(σ),

|[a₁– a₂]|(σ) = |[a₁]|(σ) – |[a₂]|(σ),

|[a_1* a₂]|(σ) = |[a₁]|(σ) · |[a₂]|(σ).

В язык L могут быть включены стандартные функции.

Пример. Возьмем арифметическое выражение x + y_* (12 – x) и L ={x, y}. Зададим состояние σ, положив σ(x) = 5, σ(у) = 2. Тогда

|[x + y*(12 – x)]|(σ) = |[x]|(σ) + |[y_* (12 – x)]|(σ)

= σ(x) + [y](σ) [12 – x](σ)

= 5 + σ(у) · ([12](σ) – [x](σ)) = 5 + 2 · (12 – σ(x))

= 5 + 2 · (12 – 5) = 19.

Семантика булевых выражений :

|[true]|(σ) = 1 (единица обозначает булево значение «истина»),

|[false]|(σ) = 0 (нуль обозначает булево значение «ложь»),

|[a₁=a₂]|(σ) = 1 |[a₁]|(σ) = |[a₂]|(σ),

т.е. |[a₁=a₂]|(σ) = ([a₁](σ) = [a₂](σ)),

|[a₁ a₂]|(σ) = 1 |[a₁]|(σ) [a₂]|(σ),

т.е. |[a₁ a₂]|(σ) = (|[a₁]|(σ) |[a₂]|(σ)),

|[a₁<a₂]|(σ) = 1 |[a₁]|(σ) < |[a₂]|(σ),

т.е. |[a₁<a₂]|(σ) = (|[a₁]|(σ) < |[a₂]|(σ)),

|[not b]|(σ) = 1 |[b]|(σ) = 0, т.е. |[not b]|(σ) = |[b]|(σ),

|[b₁ and b₂]|(σ) =1 |[b₁]|(σ) = 1 и |[b₂]|(σ) = 1,

т.е. |[b₁ and b₂]|(σ) = |[b₁](σ) [b₂]|(σ),

|[b₁ or b₂]|(σ) =1 |[b₁]|(σ) =1 или |[b₂]|(σ) =1,

т.е. |[b₁ or b₂]|(σ) = |[b₁]|(σ) |[b₂]|(σ).

Пример. Возьмем булево выражение (not x=y) and y<x и L={x,y}. Зададим состояние σ, положив σ(х) = 5, σ(у) = 2. Тогда

|[(not x=y) and y<x]|(σ) = |[(not x=y)]|(σ) |[y<x]|(σ)

= (|[x=y]|(σ)) (|[y]|(σ)<|[x]|(σ))

= (|[x]|(σ) = |[y]|(σ)) (σ(y)<σ(x))

= (σ(x)=σ(y)) (2<5) = (5=2) 1 = 1 1 = 1.

Прежде чем определять семантику операторов, введем некоторые обозначения:

▪ Пусть L={v₁, v₂,…, v_p} – множество переменных и {с₁, с₂,…, с_p} – множество целых чисел. Через {v₁:с₁, v₂:с₂,…, v_k:с_k} обозначим состояние σ для L такое, что σ(v_j) = с_j (1 j p);

▪ Через σ{v/d} обозначим состояние, получаемое из σ изменением на d значения переменной v, т.е. σ{v/d}(v) = d и σ{v /d}( v) = σ(v) = с_k для всех v’ v. Это обозначение можно распространить на случай, когда изменяются значения двух (или более) переменных: σ{v₁/d₁, v₁/d₁};

▪ Через <xy,z> обозначим форму, которая для любых данных непустых множеств C и D определяет следующую функцию выбора {0,1} C D C D :

<1y,z> = y и <0 y,z> = z.

Семантика операторов:

|[v:= a]|(σ) = σ{v/ |[a]|(σ)};

|[(v₁,v₂):= (a₁,a₂)]|(σ) = σ{v₁ / |[a₁]|(σ), v₂ / |[а₂]|(σ)};

|[skip]|(σ) = σ;

|[if b then S₁ else S₂ ]|(σ) = < [b](σ) |[S₁]|(σ),|[S₂]|(σ) > ;

|[while b do S od]|(σ) = < |[b]|(σ)  |[while b do S od]|(|[S]|(σ)), σ >;

|[return v]|(σ) = σ(v);

|[S₁ ; S₂]|(σ) = |[S₂ ]|(|[S₁]|(σ)).

Пример. Возьмем программу для алгоритма Эвклида

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

и найдем значение |[Q]|(σ), где σ = {x:28, у:72}.

Обозначим:

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

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

S₃ : return x.

Тогда имеем

|[Q]|(σ) = |[S₁ ; S₂ ; S₃]|(σ) = |[S₃]|( |[S₂]|( |[S₁]|(σ)))

Замечание. В дальнейшем, чтобы сократить число круглых скобок, вместо выражений вида |[S]|(σ) будем писать |[S]|σ, а также будем пользоваться ассоциативностью операции применения функций. В частности, мы пишем |[S₃]| |[S₂]| |[S₁]| σ вместо |[S₃]| (|[S₂]| (|[S₁]|(σ))).

Имеем:

|[S₁]| σ = |[if x<y then (x,y):= (y,x) else skip]| σ

= < |[x<y]| σ  |[(x,y):= (y,x)]| σ, |[skip]| σ >

= < |[x]| σ < |[y]| σ  |[(x,y):= (y,x)]| σ, |[skip]| σ >

= < σ(x) < σ(y)  σ{x/σ(y),y/σ(x)}, σ >

= < 28 < 72  σ{x/72,y/28}, σ >

= < 1  σ{x/72,y/28}, σ >

= σ{x/72,y/28}

= {x:72, y:28}.

Полученное состояние обозначим σ₁ . Таким образом,

|[S₁]| σ = σ₁ = {x:72, y:28}.

Вычисляя σ₁, мы на каждом шаге применяли все правила семантики, которые на этом шаге применимы. Другими словами, мы здесь использовали тактику полной подстановки (переписывания). Но можно за один шаг применять лишь часть возможных подстановок.

При вычислении |[S₂]| σ₁, чтобы несколько сократить записи, будем использовать обозначение

S₀ : (x, y) := (y, x mod y).

Вычисляя |[S₂]| σ₁ , получим:

|[S₂]| σ₁ = |[while not y=0 do S₀ od]| σ₁

= < |[not y =0]| σ₁ |[while not y=0 do S₀ od]| |[S₀]| σ₁, σ₁ >

= < |[y =0]| σ₁ |[while not y=0 do S₀ od]| |[S₀]| σ₁, σ₁ >

= < |[y]| σ₁ |[0]|σ₁ |[while not y=0 do S₀ od]| |[S₀]| σ₁, σ₁ >

= < σ₁(y) |[0]| σ₁ |[while not y=0 do S₀ od]| |[S₀]|σ₁, σ₁ >

= < 28 0 |[while not y=0 do S₀ od]| |[S₀]| σ₁, σ₁ >

= |[while not y=0 do S₀ od]| |[S₀]| σ₁

= |[while not y=0 do S₀ od]| σ₂,

где σ₂ = |[S₀]| σ₁ = |[(х,у):= (y,x mod y)]| σ₁

= σ₁{x / |[y]| σ₁, y / |[x mod y]| σ₁}

= σ₁{x/ 28, y/ 16} = {x: 28, у: 16}.

Далее получаем:

|[while not y=0 do S₀ od]| σ₂ =

= < |[not y]| σ₂ |[while not y=0 do S₀ od]| |[S₀]| σ₂, σ₁ >

= < |[y]| σ₂ |[0]| σ₂ |[while not y=0 do S₀ od]| |[S₀]| σ₂, σ₁ >

= < 16 0  |[while not y=0 do S₀ od]| |[S₀]| σ₂, σ₁ >

= |[while not y=0 do S₀ od]| |[S₀]| σ₂

= |[while not y=0 do S₀ od]| σ₃ ,

где σ₃ = |[S₀]| σ₂ = |[(х,у):= (y,x mod y)]| σ₂ = {x: 16, y: 12}.

Аналогично получаем:

|[while not y=0 do S₀ od]| σ₃ = |[while not y=0 do S₀ od]| σ₄ ,

где σ₄ = |[S₀]| σ₃ = {x: 12, y: 4};

|[while not y=0 do S₀ od]| σ₄ =|[while not y=0 do S₀ od]| σ₅ ,

где σ₅ = |[S₀]| = {x: 4, y: 0};

Теперь имеем:

|[while not y=0 do S₀ od]| σ₅ =

= < |[not y]| σ₅ |[while not y=0 do S₀ od]| |[S₀]| σ₅, σ₅>

= < 0 0  |[while not y=0 do S₀ od]| |[S₀]| σ₅, σ₅ >

= σ₅ = {x: 4, y: 0}.

Наконец получаем:

|[Q]|(σ) = |[|S₃]| σ₅ = 4.

1.6. Эквивалентность программ

Две программы P и Q называются эквивалентными, если

|[P]| = |[Q]|, т.е. |[P]| σ = |[Q]| σ для всех L-состояний, где L = L_P L_Q.

Примеры. 1) Программы

P: while b do S od,

Q: if b then S; while b do S od else skip

эквивалентны. В самом деле, имеем для всякого L-состояния σ (где L == L_P L_Q )

|[if b then S; while b do S od else skip]| σ

Характеристики

Список файлов лекций