SW wykład 3 - Slajd16: Różnice pomiędzy wersjami
Nie podano opisu zmian |
Nie podano opisu zmian |
||
| Linia 4: | Linia 4: | ||
Rozszerzmy teraz instrukcje języka TINY przez dodanie dwóch | Rozszerzmy teraz instrukcje języka TINY przez dodanie dwóch | ||
dodatkowych konstrukcji językowych: instrukcji powodującej | dodatkowych konstrukcji językowych: instrukcji powodującej | ||
zakleszczenie obliczeń | zakleszczenie obliczeń oraz konstrukcji niedeterministycznego | ||
wyboru. Odpowiednie rozszerzenia semantyki operacyjnej (definicji | wyboru. Odpowiednie rozszerzenia semantyki operacyjnej (definicji | ||
relacji przejścia) i semantyki naturalnej przedstawione są powyżej na | relacji przejścia) i semantyki naturalnej przedstawione są powyżej na | ||
slajdzie. W obu przypadkach podajemy jedynie warunki definicyjne | slajdzie. W obu przypadkach podajemy jedynie warunki definicyjne, | ||
określające przejścia związane z niedeterministycznym | określające przejścia związane z niedeterministycznym | ||
wyborem. Instrukcja zakleszczenia w tych definicjach nie pojawia | wyborem. Instrukcja zakleszczenia w tych definicjach nie pojawia się; | ||
powód jest oczywisty: zgodnie z intuicją, oznacza to brak przejść dla | powód jest oczywisty: zgodnie z intuicją, oznacza to brak przejść dla | ||
konfiguracji tę instrukcję zawierających. | konfiguracji tę instrukcję zawierających. | ||
Aktualna wersja na dzień 11:21, 29 wrz 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 się; powód jest oczywisty: zgodnie z intuicją, oznacza to brak przejść dla konfiguracji tę instrukcję zawierających.
