SW wykład 3 - Slajd10: Różnice pomiędzy wersjami
Nie podano opisu zmian |
Nie podano opisu zmian |
||
| Linia 4: | Linia 4: | ||
Spróbujmy teraz porównać dwie wprowadzone semantyki dla instrukcji | Spróbujmy teraz porównać dwie wprowadzone semantyki dla instrukcji | ||
języka TINY: semantykę operacyjną (małych kroków) i semantykę | języka TINY: semantykę operacyjną (małych kroków) i semantykę | ||
naturalną (wielkich kroków). | |||
Zgodnie z nieformalną sugestią przy wprowadzaniu semantyki naturalnej | Zgodnie z nieformalną sugestią przy wprowadzaniu semantyki naturalnej | ||
Aktualna wersja na dzień 11:15, 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ść
Spróbujmy teraz porównać dwie wprowadzone semantyki dla instrukcji języka TINY: semantykę operacyjną (małych kroków) i semantykę naturalną (wielkich kroków).
Zgodnie z nieformalną sugestią przy wprowadzaniu semantyki naturalnej powyżej, w pewnym sensie są one w istocie takie same: w semantyce naturalnej dana konfiguracja prowadzi do pewnej konfiguracji końcowej wtedy i tylko wtedy, gdy w semantyce operacyjnej obliczenie rozpoczynające się w tej konfiguracji kończy się w tejże konfiguracji końcowej.
Uwaga: nie jest to już teraz tylko intuicja; jest to w pełni ścisłe stwierdzenie, dla którego poniżej przeprowadzimy formalny dowód.
