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

Категория: Устройства и комплектующие
Нажмите для полного просмотра!
Семантика императивного языка While2, слайд №1Семантика императивного языка While2, слайд №2Семантика императивного языка While2, слайд №3Семантика императивного языка While2, слайд №4Семантика императивного языка While2, слайд №5Семантика императивного языка While2, слайд №6Семантика императивного языка While2, слайд №7Семантика императивного языка While2, слайд №8Семантика императивного языка While2, слайд №9Семантика императивного языка While2, слайд №10Семантика императивного языка While2, слайд №11Семантика императивного языка While2, слайд №12Семантика императивного языка While2, слайд №13Семантика императивного языка While2, слайд №14Семантика императивного языка While2, слайд №15Семантика императивного языка While2, слайд №16Семантика императивного языка While2, слайд №17Семантика императивного языка While2, слайд №18Семантика императивного языка While2, слайд №19
Скачать
Вы можете ознакомиться и скачать презентацию на тему Семантика императивного языка While2. Доклад-сообщение содержит 19 слайдов. Презентации для любого класса можно скачать бесплатно. Если материал и наш сайт презентаций Mypresentation Вам понравились – поделитесь им с друзьями с помощью социальных кнопок и добавьте в закладки в своем браузере.

Слайды и текст этой презентации

Слайд 1


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

Слайд 2


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

Слайд 3


Абстрактный синтаксис языка While
Описание слайда:
Абстрактный синтаксис языка While

Слайд 4


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

Слайд 5


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

Слайд 6


Естественная семантика языка 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 <С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

Слайд 7


Естественная семантика языка 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
Описание слайда:
Естественная семантика языка 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

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

Слайд 9


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

Слайд 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), eval(C2,St1,St2).
Описание слайда:
Реализация на Прологе 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 _ 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).
Описание слайда:
Реализация на Прологе 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).

Слайд 13


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

Слайд 14


Доказательство Часть 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] .
Описание слайда:
Доказательство Часть 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] .

Слайд 15


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

Слайд 16


Доказательство (продолжение) Использовав 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)
Описание слайда:
Доказательство (продолжение) Использовав 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)

Слайд 17


Доказательство (продолжение) Во втором случае, когда использовалось правило [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” . Это завершает доказательство первой части.
Описание слайда:
Доказательство (продолжение) Во втором случае, когда использовалось правило [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” . Это завершает доказательство первой части.

Слайд 18


Доказательство (продолжение) Часть 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].
Описание слайда:
Доказательство (продолжение) Часть 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].

Слайд 19


Доказательство (продолжение) В первом случае, когда 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).
Описание слайда:
Доказательство (продолжение) В первом случае, когда 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).

Скачать

Похожие презентации
Mypresentation.ru
Загрузить презентацию