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

Содержание слайда: Семантика императивного языка While

Содержание слайда: Абстрактный синтаксис языка While Синтаксические категории

Содержание слайда: Абстрактный синтаксис языка While

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

Содержание слайда: Естественная семантика языка While <С1,s>  s’, <С2,s’>  s” [comp] <С1;С2,s>  s”

Содержание слайда: Естественная семантика языка While <С1,s>  s’ [ift] [B[be]s=T] <if be then С1 else С2,s>  s’ <С2,s>  s’ [iff] [B[be]s=F] <if be then С1 else С2,s>  s’ где B[be]s=bv обозначает s├beBbv

Содержание слайда: Естественная семантика языка While <С,s>  s’ <while be do С,s’>  s” [whilet] [B[be]s=T] <while be do С,s>  s” [whilef] [B[be]s=F] <while be do С,s>  s

Содержание слайда: Реализация на Прологе 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 >> x:=x-1)).

Содержание слайда: АСД тестовой программы

Содержание слайда: Реализация на Прологе 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).

Содержание слайда: Реализация на Прологе 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).

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

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

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

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

Содержание слайда: Доказательство (продолжение) Использовав T1 и T2 как посылки правила [comp] получим дерево: T1 T2 <C; while be do C, s>  s” Учитывая, что B[be]s=T можно применив правило [ift] получим дерево: T1 T2 <C; while be do C, s>  s” <if be then (C; while be do C) else skip, s> s” В нём получился вывод заключения (2)

Содержание слайда: Доказательство (продолжение) Во втором случае, когда использовалось правило [whilef] и выполнялось условие B[b]s=F, тогда s = s” . Дерево T будет иметь форму: <while be do C, s>  s Используя аксиому [skip] получим <skip,s>  s, а применив правило [iff] получим дерево вывода для (2): <skip, s>  s <if be then (C; while be do C) else skip, s>  s В нём получился вывод заключения (2), если учесть, что s = s” . Это завершает доказательство первой части.

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

Содержание слайда: Доказательство (продолжение) В первом случае, когда B[be]s=T, вершина (2) получена из вершины 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] и, тогда получим ветвь для <skip, s>  s”. На основании аксиомы [skip] получим, что s = s” . Теперь, применив аксиому [whilef] получим дерево вывода для (1).