SW wykład 3 - Slajd16
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.
