Семантика императивного языка 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

Слайд 2

Описание слайда:

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

Слайд 3

Описание слайда:

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

Слайд 4

Описание слайда:

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

Слайд 5

Описание слайда:

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

Слайд 6

Описание слайда:

Естественная семантика языка While  s’ [ift] [B[be]s=T]  s’  s’ [iff] [B[be]s=F]  s’ где B[be]s=bv обозначает s├beBbv

Слайд 7

Описание слайда:

Естественная семантика языка While  s’  s” [whilet] [B[be]s=T]  s” [whilef] [B[be]s=F]  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)).

Слайд 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).

Слайд 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 _ 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’ справедливо: s’  s’ Докажем, что команды while be do C и if be then (C; while be do C) else skip семантически эквивалентны.

Слайд 14

Описание слайда:

Доказательство Часть 1 Докажем, что если  s” (1) то и  s” (2) из истинности посылки (1) следует, что для неё существует дерево вывода T. Корень этого дерева может иметь одну из двух форм, в зависимости от того, использовалось ли правило [whilet] или [whilef] .

Слайд 15

Описание слайда:

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

Слайд 16

Описание слайда:

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

Слайд 17

Описание слайда:

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

Слайд 18

Описание слайда:

Доказательство (продолжение) Часть 2 Докажем импликацию в обратном порядке: если < if be then (C; while be do C) else skip, s>  s” (2) то и  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] и, тогда получим ветвь для  s”. На основании аксиомы [skip] получим, что s = s” . Теперь, применив аксиому [whilef] получим дерево вывода для (1).