Семантика императивного языка While2 презентация

∈ BVar op ∈ Op bop ∈ BOp n ∈ Num

var x | bvar bx | procedure I:C | D’; D”
C ::= skip | x := e | C’ ; C” | I
| if be then C’ else C”
| while be do C’ | begin B end
e ::= x | n | e’ op e” | if be then e’ else e”
be::= bx | T | F | Not be’| Equal (e,e’) | be’ bop be”
op ::= + | - | * | div
bop ::= and | or

– команда, s - состояние переменных.
Правила.
[ass] ⇒ s[x/A[e]s],
где A[e]s обозначает s├e⇒Av
[skip] < skip,s> ⇒ s.

семантика языка While

С2,s> ⇒ s’

<С2,s> ⇒ s’ [iff] [B[be]s=F] ⇒ s’ где B[be]s=bv обозначает s├be⇒Bbv

Естественная семантика языка While

[whilet] [B[be]s=T] ⇒ s”

[whilef] [B[be]s=F] ⇒ s

Естественная семантика языка While

>> x:=x-1)).

x:=x-1)

eval(C2,St1,St2).

eval(C1,St0,St1).
eval(if _ then _ else C2,St0,St1) :-
eval(C2,St0,St1).

eval(while B do C, St0, St1) :-
beval(St0,B,tt),!,
eval(C >> (while B do C),St0,St1).
eval(while _ do _, St, St).

двух состояний s и s’ справедливо: ⇒s’ ≡ ⇒s’
Докажем, что команды while be do C и if be then (C; while be do C) else skip семантически эквивалентны.

то и < if be then (C; while be do C) else skip, s> ⇒ s” (2)
из истинности посылки (1) следует, что для неё существует дерево вывода T. Корень этого дерева может иметь одну из двух форм, в зависимости от того, использовалось ли правило [whilet] или [whilef] .

T2 ⇒ s” где T1 - дерево вывода с корнем ⇒ s’, а T2 - имеет корень ⇒ s” .
Более того B[b]s=T .

T1 T2 ⇒ s” Учитывая, что B[be]s=T можно применив правило [ift] получим дерево: T1 T2 ⇒ s” ⇒s” В нём получился вывод заключения (2)

B[b]s=F, тогда s = s” . Дерево T будет иметь форму: ⇒ s Используя аксиому [skip] получим ⇒ s, а применив правило [iff] получим дерево вывода для (2): ⇒ s ⇒ s
В нём получился вывод заключения (2), если учесть, что s = s” .
Это завершает доказательство первой части.

then (C; while be do C) else skip, s> ⇒ s” (2)
то и ⇒ s” (1) Для этого, имея дерево вывода T для (2), нужно построить дерево вывода для (1) . Для (2) дерево вывода могло быть построено только правилами [ift] или [iff].

вершины T1 = < C; while be do C, s> ⇒ s”, которая , в свою очередь как композиция операторов могла быть получена только по правилу [comp] . Значит к T1 ведут две ветви:
T2 = < C, s> ⇒ s’, T3 = < while be do C, s’> ⇒ s”. Теперь, если T2 и T3 в качестве посылок для правила [whilet] получим дерево вывода для (1).
Во втором случае, когда выполнялось условие B[b]s=F, дерево T будет строиться по правилу [iff] и, тогда получим ветвь для ⇒ s”. На основании аксиомы [skip] получим, что s = s” . Теперь, применив аксиому [whilef] получим дерево вывода для (1).