SW wykład 3 - Slajd14: Różnice pomiędzy wersjami
Nie podano opisu zmian |
Nie podano opisu zmian |
||
| Linia 1: | Linia 1: | ||
{{Semantyka i weryfikacja programów/Wykład 3}} | {{Semantyka i weryfikacja programów/Wykład 3}} | ||
[[Grafika:sw0313.png|center|frame]] | [[Grafika:sw0313.png|center|frame]] | ||
Powyżej pokazaliśmy, w jakim sensie podane semantyki (operacyjną i | |||
naturalną) dla instrukcji języka TINY można uznać za równoważne. Z | |||
drugiej jednak strony, są one oczywiście różne. Najkrócej jak można: | |||
semantyka naturalna pomija wiele szczegółowych informacji o procesie | |||
obliczenia instrukcji, które podaje semantyka operacyjna małych | |||
kroków. W szczególności, semantyka naturalna nie uwzględnia własności | |||
zakleszczania i pętlenia się obliczeń. Te właśnie różnice chcemy teraz | |||
podkreślić. | |||
Wersja z 20:36, 22 sie 2006
Semantyka naturalna Semantyka naturalna Tiny Sens definicji Sens definicji, c.d. Dowody Indukcja po strukturze Własności Równoważność semantyczna Kongruencje Semantyka operacyjna a naturalna Semantyka operacyjna a naturalna, c.d. Semantyka operacyjna a naturalna, c.d. Semantyka "denotacyjna" Semantyka operacyjna a naturalna, c.d. Równoważność operacyjna Niedeterminizm Kilka równoważności Równoległość
Powyżej pokazaliśmy, w jakim sensie podane semantyki (operacyjną i naturalną) dla instrukcji języka TINY można uznać za równoważne. Z drugiej jednak strony, są one oczywiście różne. Najkrócej jak można: semantyka naturalna pomija wiele szczegółowych informacji o procesie obliczenia instrukcji, które podaje semantyka operacyjna małych kroków. W szczególności, semantyka naturalna nie uwzględnia własności zakleszczania i pętlenia się obliczeń. Te właśnie różnice chcemy teraz podkreślić.
