SW wykład 4 - Slajd13

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

Wróćmy do przykładu, który motywuje nasze rozważania definicji stałopunktowych. Klauzula semantyczna dla instrukcji pętli określa jej znaczenie jako punkt stały pewnego operatora (funkcji wyższego rzędu) na dziedzinie semantycznej dla instrukcji. Operator ten, zdefiniowany w zwarty sposób powyżej, jest więc funkcją, która funkcjom częściowym na stanach przypisuje funkcje częściowe na stanach.

Poszukujemy metody określania pewnego punktu stałego dla takich (być może spełniających pewne dodatkowe warunki) operatorów.

Najważniejszym kryterium stwierdzenia, czy wskazana metoda będzie adekwatna dla zastosowań w semantyce denotacyjnej, jest zapewnienie, że właśnie dla instrukcji pętli znaczenia definiowane jako wybrany punkt stały odpowiadających tym pętlom operatorów będą zgodne z naszymi operacyjnymi intuicjami dotyczącymi realizacji obliczeń pętli. Intuicje te zostały już wcześniej sprecyzowane przez semantykę operacyjną i do niej właśnie najprościej się tu odwołać, formułując precyzyjnie nasze oczekiwania wobec wyboru punktu stałego rozważanych operatorów jak w ostatniej ramce na slajdzie.