SW wykład 3 - Slajd9: Różnice pomiędzy wersjami

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
Mengel (dyskusja | edycje)
Nie podano opisu zmian
 
Dorota (dyskusja | edycje)
Nie podano opisu zmian
 
(Nie pokazano 3 wersji utworzonych przez 2 użytkowników)
Linia 1: Linia 1:
{{Semantyka i weryfikacja programów/Wykład 3}}
[[Grafika:sw0308.png|center|frame]]
[[Grafika:sw0308.png|center|frame]]
Ważną klasę stwierdzeń o właśnie wprowadzonej naturalnej równoważności
stanowią fakty mówiące, że konstrukcje językowe zachowują tę
równoważność. Dla każdej konstrukcji językowej budującej instrukcje z
ich bezpośrednich składowych, jeśli bezpośrednie składowe są wzajemnie
równoważne, całe instrukcje z nich zbudowane są wzajemnie
równoważne (dowody pomijamy, ale zachęcamy do ich systematycznego
przeprowadzenia).
Jak wspominaliśmy wyżej, semantyka wyznacza też równoważność dla innych
kategorii składniowych języka TINY. Na przykład, dwa wyrażenia
(arytmetyczne, logiczne) są równoważne, gdy mają tę samą semantykę.
Pozwala to na sformułowanie nieco bardziej ogólnych stwierdzeń o
własnościach kongruencji dla równoważności instrukcji, które
uwzględniają także możliwość zastąpienia wyrażeń logicznych w
instrukcjach warunkowych i pętlach przez wyrażenia im równoważne ---
dokładne sformułowanie i dowody tych własności pozostawiamy Państwu.

Aktualna wersja na dzień 11:12, 29 wrz 2006

<<powrót do strony wykładu

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ść

Ważną klasę stwierdzeń o właśnie wprowadzonej naturalnej równoważności stanowią fakty mówiące, że konstrukcje językowe zachowują tę równoważność. Dla każdej konstrukcji językowej budującej instrukcje z ich bezpośrednich składowych, jeśli bezpośrednie składowe są wzajemnie równoważne, całe instrukcje z nich zbudowane są wzajemnie równoważne (dowody pomijamy, ale zachęcamy do ich systematycznego przeprowadzenia).

Jak wspominaliśmy wyżej, semantyka wyznacza też równoważność dla innych kategorii składniowych języka TINY. Na przykład, dwa wyrażenia (arytmetyczne, logiczne) są równoważne, gdy mają tę samą semantykę. Pozwala to na sformułowanie nieco bardziej ogólnych stwierdzeń o własnościach kongruencji dla równoważności instrukcji, które uwzględniają także możliwość zastąpienia wyrażeń logicznych w instrukcjach warunkowych i pętlach przez wyrażenia im równoważne --- dokładne sformułowanie i dowody tych własności pozostawiamy Państwu.