SW wykład 4 - Slajd19

<<powrót do strony wykładu

Semantyka denotacyjna Dziedziny składniowe i semantyczne Funkcje semantyczne Kompozycjonalność Tiny. Semantyka denotacyjna Tiny. Semantyka denotacyjna, c.d. Pojęcia pomocnicze Pojęcia pomocnicze, c.d. |Tiny. Semantyka denotacyjna, c.d. Tiny. Semantyka denotacyjna, c.d. Problem z while Konstrukcje stałopunktowe Konstrukcje stałopunktowe, c.d. Konstrukcje stałopunktowe, c.d. Przykład Przykład, c.d. Dowód Dowód Zgodność semantyki denotacyjnej

Wskazana wyżej własność znaczeń pętli określonych semantyką denotacyjną, wiążąca te znaczenia z podaną wcześniej semantyką operacyjną, to kluczowy krok dowodu faktu stwierdzającego adekwatność semantyki denotacyjnej względem naszych intuicji obliczeniowych, sformalizowanych przez semantykę operacyjną języka TINY.

Własność ta sformułowana jest ściśle na slajdzie (ramka).

Dowód pierwszej z implikacji przebiega przez indukcję strukturalną po strukturze rozważanej instrukcji. Wszystkie przypadki są łatwe, poza przypadkiem pętli, który pokazaliśmy powyżej.

Dowód implikacji przeciwnej przebiega przez indukcję względem długości obliczenia instrukcji w danym stanie początkowym. Dla obliczeń niepustych (a tylko takie są tu interesujące), dowód przebiega przez przypadki po pierwszym kroku obliczenia (a więc przypadki określone są przez postać instrukcji i spełnienie wykorzystywanych w definicji relacji przejścia w semantyce operacyjnej warunków).

Szczegóły dowodów pomijamy, ale zachęcamy Państwa do ich formalnego przeprowadzenia.