SW wykład 3 - Slajd1

<<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 operacyjna (małych kroków) jest stosunkowo bliskim opisem rzeczywistej realizacji maszynowej programów języka. Warto jeszcze może wspomnieć, że niekiedy (często?) wykorzystuje się metody semantyki operacyjnej dla zdefiniowania pośredniej fazy kompilacji programów: definiujemy pewną "maszynę abstrakcyjną" z dobrze określonymi konfiguracjami i przejściami, a programy naszego języka tłumaczymy na język przejść tej maszyny (por. na przykład maszynę abstrakcyjną dla języka Java). Dalsza implementacja języka programowania polega już tylko na realizacji tej abstrakcyjnej maszyny na konkretne platformy systemowe i sprzętowe.

Ta bliskość semantyki operacyjnej i implementacji języka jest oczywiście zarazem jej wadą i zaletą. Jedną z jej konsekwencji (często niedogodnych) jest fakt, że końcowego wyniku obliczeń programu (czy konfiguracji ten wynik zawierającej) nie otrzymujemy tu wprost, ale tylko pośrednio, przez rozważanie (maksymalnych) obliczeń rozpoczynających się w odpowiedniej konfiguracji początkowej. Jest to po prostu niewygodne w sytuacji, gdy interesują nas tylko wyniki programu, a nie szczegóły jego działania.

Problem ten można ominąć stosując inną odmianę operacyjnej metody opisu semantyki, tzw. semantykę naturalną, zwaną też niekiedy semantyką operacyjną wielkich kroków.

Podobnie jak dla semantyki operacyjnej małych kroków, definiujemy tu zbiór konfiguracji, wskazując które z nich uznajemy za konfiguracje końcowe. Jednak zamiast obliczeń definiujemy od razu relację opisującą przejście od dowolnej konfiguracji do odpowiadającej jej konfiguracji końcowej.

Intuicyjny związek z semantyką operacyjną małych kroków opisuje warunek, że w semantyce naturalnej dana konfiguracja prowadzi do pewnej konfiguracji końcowej, gdy w semantyce operacyjnej obliczenie rozpoczynające się w tej konfiguracji kończy się w tejże konfiguracji końcowej. O ile takiego pomyślnie zakończonego obliczenia rozpoczynającego się w danej konfiguracji nie ma, nie powinna być ona w dziedzinie relacji opisanej semantyką naturalną.