SW wykład 3 - Slajd16: 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:sw0315.png|center|frame]] | [[Grafika:sw0315.png|center|frame]] | ||
Rozszerzmy teraz instrukcje języka TINY przez dodanie dwóch | |||
dodatkowych konstrukcji językowych: instrukcji powodującej | |||
zakleszczenie obliczeń, oraz konstrukcji niedeterministycznego | |||
wyboru. Odpowiednie rozszerzenia semantyki operacyjnej (definicji | |||
relacji przejścia) i semantyki naturalnej przedstawione są powyżej na | |||
slajdzie. W obu przypadkach podajemy jedynie warunki definicyjne | |||
określające przejścia związane z niedeterministycznym | |||
wyborem. Instrukcja zakleszczenia w tych definicjach nie pojawia sie; | |||
powód jest oczywisty: zgodnie z intuicją, oznacza to brak przejść dla | |||
konfiguracji tę instrukcję zawierających. | |||
Wersja z 20:37, 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ść
Rozszerzmy teraz instrukcje języka TINY przez dodanie dwóch dodatkowych konstrukcji językowych: instrukcji powodującej zakleszczenie obliczeń, oraz konstrukcji niedeterministycznego wyboru. Odpowiednie rozszerzenia semantyki operacyjnej (definicji relacji przejścia) i semantyki naturalnej przedstawione są powyżej na slajdzie. W obu przypadkach podajemy jedynie warunki definicyjne określające przejścia związane z niedeterministycznym wyborem. Instrukcja zakleszczenia w tych definicjach nie pojawia sie; powód jest oczywisty: zgodnie z intuicją, oznacza to brak przejść dla konfiguracji tę instrukcję zawierających.
