SW wykład 3 - Slajd8

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

Zadana semantyka naturalna (jak zresztą każda semantyka, przypisująca mniej lub bardziej pośrednio programom języka ich znaczenia) wyznacza pewną naturalną równoważność programów --- tu instrukcji języka TINY. Mianowicie, dwie instrukcje są równoważne względem semantyki naturalnej, gdy dla wszystkich par konfiguracji zawierających odpowiednio każdą z tych instrukcji i ten sam stan, konfiguracje te prowadzą do dokładnie tych samych stanów końcowych.

Podkreślmy: jest to precyzyjna, jednoznaczna definicja równoważności instrukcji, której niezbędnym warunkiem było podanie formalnej semantyki języka TINY.

Możemy też już teraz pokazać szereg (tu: dość prostych) równoważności między instrukcjami. Ich dowody przez indukcję po strukturze wyprowadzenia pomijamy. I znów: te i bardziej skomplikowane równoważności możemy teraz pokazywać w pełni wiarygodnie dzięki odpowiednim podstawom formalnym (definicja semantyki, definicja równoważności, dobrze uzasadniona, poprawna technika dowodzenia).