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

Содержание

Слайд 2

p ∈ Program B ∈ Block D ∈ Decl C ∈ Cmd е ∈ Exp bе ∈ BExp

Синтаксические категории

Абстрактный синтаксис языка While

I ∈ Id x ∈ Var bx ∈ BVar op ∈ Op bop

p ∈ Program B ∈ Block D ∈ Decl C ∈ Cmd е
∈ BOp n ∈ Num

Слайд 3

Абстрактный синтаксис языка While

Определения

p ::= B
B ::= D ; C
D ::=

Абстрактный синтаксис языка While Определения p ::= B B ::= D ; C
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

Слайд 4

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

Отношение «вычисляет» определяется утверждениями вида:
<С,s> ⇒ s’,
где С

Естественная семантика языка While Отношение «вычисляет» определяется утверждениями вида: ⇒ s’, где С
– команда, s - состояние переменных.
Правила.
[ass] ⇒ s[x/A[e]s],
где A[e]s обозначает s├e⇒Av
[skip] < skip,s> ⇒ s.

Слайд 5

<С1,s> ⇒ s’, <С2,s’> ⇒ s” [comp] <С1;С2,s> ⇒ s”

Естественная

⇒ s’, ⇒ s” [comp] ⇒ s” Естественная семантика языка While
семантика языка While

Слайд 6

<С1,s> ⇒ s’ [ift] [B[be]s=T]

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

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

Слайд 7

<С,s> ⇒ s’ ⇒ s” [whilet]

⇒ s’ ⇒ s” [whilet] [B[be]s=T] ⇒ s” [whilef] [B[be]s=F] ⇒ s Естественная семантика языка While
[B[be]s=T] ⇒ s”
[whilef] [B[be]s=F] ⇒ s

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

Слайд 8

Реализация на Прологе 1

:-op(880,xfx,:=).
:-op(890,xfx,[then,else,do]).
:-op(900,fy,[if,while]).
:-op(910,xfy,>>).
test (y:=1 >> while x>0 do (y:= y*x

Реализация на Прологе 1 :-op(880,xfx,:=). :-op(890,xfx,[then,else,do]). :-op(900,fy,[if,while]). :-op(910,xfy,>>). test (y:=1 >> while x>0
>> x:=x-1)).

Слайд 9

АСД тестовой программы

>>

:=

while

y

1

do

x>0

>>

:=

:=

y

y*x

x

x-1

y:= 1 >> while x>0 do (y:= y*x >>

АСД тестовой программы >> := while y 1 do x>0 >> := :=
x:=x-1)

Слайд 10

Реализация на Прологе 2
store(X,V,[],[X/V]) :- !.
store(X,V,[X/_|T],[X/V|T]) :- !.
store(X,V,[X1/V1|T],[X1/V1|Tn]) :-
store(X,V,T,Tn).

Реализация на Прологе 2 store(X,V,[],[X/V]) :- !. store(X,V,[X/_|T],[X/V|T]) :- !. store(X,V,[X1/V1|T],[X1/V1|Tn]) :- store(X,V,T,Tn).

Слайд 11

Реализация на Прологе 3
eval(X:=E,S,Sn) :-
arith(S,E,V),
store(X,V,S,Sn).
eval(skip,S,S).
eval(C1 >> C2,St0,St2) :-
eval(C1,St0,St1),

Реализация на Прологе 3 eval(X:=E,S,Sn) :- arith(S,E,V), store(X,V,S,Sn). eval(skip,S,S). eval(C1 >> C2,St0,St2) :- eval(C1,St0,St1), eval(C2,St1,St2).
eval(C2,St1,St2).

Слайд 12

Реализация на Прологе 4
eval(if B then C1 else _,St0,St1) :-
beval(St0,B,tt),!,

Реализация на Прологе 4 eval(if B then C1 else _,St0,St1) :- beval(St0,B,tt),!, eval(C1,St0,St1).
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).

Слайд 13

Семантическая эквивалентность команд

Команды C1 и C2 семантически эквивалентны, если для любых

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

Слайд 14

Доказательство

Часть 1 Докажем, что если ⇒ s” (1)

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

Слайд 15

Доказательство (продолжение)

В первом случае дерево T , будет иметь форму: T1

Доказательство (продолжение) В первом случае дерево T , будет иметь форму: T1 T2
T2 ⇒ s” где T1 - дерево вывода с корнем ⇒ s’, а T2 - имеет корень ⇒ s” .
Более того B[b]s=T .

Слайд 16

Доказательство (продолжение)

Использовав T1 и T2 как посылки правила [comp] получим дерево:

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

Слайд 17

Доказательство (продолжение)

Во втором случае, когда использовалось правило [whilef] и выполнялось условие

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

Слайд 18

Доказательство (продолжение)

Часть 2 Докажем импликацию в обратном порядке: если < if be

Доказательство (продолжение) Часть 2 Докажем импликацию в обратном порядке: если ⇒ s” (2)
then (C; while be do C) else skip, s> ⇒ s” (2)
то и ⇒ s” (1) Для этого, имея дерево вывода T для (2), нужно построить дерево вывода для (1) . Для (2) дерево вывода могло быть построено только правилами [ift] или [iff].
Имя файла: Семантика-императивного-языка-While2.pptx
Количество просмотров: 91
Количество скачиваний: 0