SW wykład 3 - Slajd11: Różnice pomiędzy wersjami
Nie podano opisu zmian |
Nie podano opisu zmian |
||
| (Nie pokazano 1 wersji utworzonej przez jednego użytkownika) | |||
| Linia 1: | Linia 1: | ||
{{Semantyka i weryfikacja programów/Wykład 3}} | {{Semantyka i weryfikacja programów/Wykład 3}} | ||
[[Grafika:sw0310.png|center|frame]] | [[Grafika:sw0310.png|center|frame]] | ||
Zacznijmy od implikacji mówiącej, że jeśli w semantyce naturalnej dana | |||
konfiguracja prowadzi do pewnego stanu końcowego, to w semantyce | |||
operacyjnej obliczenie, rozpoczynające się w tej konfiguracji, kończy | |||
się w tymże stanie końcowym. Dowód przebiega przez indukcję po | |||
wyprowadzeniu założenia implikacji. Dowody dla poszczególnych | |||
przypadków (aksjomatów i reguł) szkicujemy powyżej na slajdzie. | |||
Aktualna wersja na dzień 11:16, 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ść
Zacznijmy od implikacji mówiącej, że jeśli w semantyce naturalnej dana konfiguracja prowadzi do pewnego stanu końcowego, to w semantyce operacyjnej obliczenie, rozpoczynające się w tej konfiguracji, kończy się w tymże stanie końcowym. Dowód przebiega przez indukcję po wyprowadzeniu założenia implikacji. Dowody dla poszczególnych przypadków (aksjomatów i reguł) szkicujemy powyżej na slajdzie.
