Содержание
- 2. p ∈ Program B ∈ Block D ∈ Decl C ∈ Cmd е ∈ Exp bе
- 3. Абстрактный синтаксис языка While Определения p ::= B B ::= D ; C D ::= var
- 4. Естественная семантика языка While Отношение «вычисляет» определяется утверждениями вида: ⇒ s’, где С – команда, s
- 5. ⇒ s’, ⇒ s” [comp] ⇒ s” Естественная семантика языка While
- 6. ⇒ s’ [ift] [B[be]s=T] ⇒ s’ ⇒ s’ [iff] [B[be]s=F] ⇒ s’ где B[be]s=bv обозначает s├be⇒Bbv
- 7. ⇒ s’ ⇒ s” [whilet] [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
- 9. АСД тестовой программы >> := while y 1 do x>0 >> := := y y*x x
- 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).
- 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), eval(C2,St1,St2).
- 12. Реализация на Прологе 4 eval(if B then C1 else _,St0,St1) :- beval(St0,B,tt),!, eval(C1,St0,St1). eval(if _ then
- 13. Семантическая эквивалентность команд Команды C1 и C2 семантически эквивалентны, если для любых двух состояний s и
- 14. Доказательство Часть 1 Докажем, что если ⇒ s” (1) то и ⇒ s” (2) из истинности
- 15. Доказательство (продолжение) В первом случае дерево T , будет иметь форму: T1 T2 ⇒ s” где
- 16. Доказательство (продолжение) Использовав T1 и T2 как посылки правила [comp] получим дерево: T1 T2 ⇒ s”
- 17. Доказательство (продолжение) Во втором случае, когда использовалось правило [whilef] и выполнялось условие B[b]s=F, тогда s =
- 18. Доказательство (продолжение) Часть 2 Докажем импликацию в обратном порядке: если ⇒ s” (2) то и ⇒
- 20. Скачать презентацию