SW wykład 3 - Slajd2

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

Semantyka naturalna instrukcji naszego języka TINY dziedziczy zbiór konfiguracji i zbiór konfiguracji końcowych z semantyki operacyjnej opisanej w poprzednim module tych zajęć.

Relację przejścia od konfiguracji do odpowiadających im konfiguracji końcowych (stanów) opisujemy przez szereg reguł, odpowiadających kolejno różnym postaciom zawartej w konfiguracji instrukcji i różnym warunkom dodatkowym. Te reguły czytać należy jak następuje: jeśli zachodzą warunki wymienione w poprzedniku reguły ("nad kreską") oraz warunki dodatkowe ("obok kreski"), to zachodzi też warunek w następniku tej reguły. Jak i w semantyce operacyjnej, mamy tu do czynienia ze schematami reguł, których wszystkie instancje są generowane przez wstawienie za meta-zmienne fraz składniowych odpowiednich kategorii języka (zmienne, wyrażenia arytmetyczne i logiczne, instrukcje) lub wartości z odpowiednich kategorii semantycznych (stany). Oczywiście, uwagi te odnoszą się w szczególności do "aksjomatów" semantyki (reguł bez poprzednika).

Proszę jednak zwrócić uwagę, że przez użycie tej samej meta-zmiennej w różnych warunkach danej reguły wskazujemy tu na zależności między tymi warunkami. Na przykład, przesłanki reguły dla sekwencyjnego złożenia instrukcji wymagają, by konfiguracja zawierająca pierwszą składową i stan początkowy prowadziła do pewnego stanu oraz by konfiguracja zawierająca drugą składową i ten właśnie stan wynikowy prowadziła do stanu końcowego. Jeśli warunki te są spełnione, to konfiguracja zawierająca sekwencyjne złożenie tych składowych i stanu początkowego prowadzi do wskazanego w drugim warunku stanu końcowego. Podobnie łatwo (i naturalnie) przeczytać można pozostałe reguły, a także aksjomaty, gdzie przejście od danej konfiguracji do wskazanego stanu końcowego nie wymaga spełnienia dodatkowych przesłanek.