SW wykład 4 - Slajd11
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
Ostatnia klauzula na poprzednim slajdzie może wzbudzić uzasadniony niepokój: nie podpada ona bezpośrednio pod przyjęty schemat klauzul semantycznych, gdzie znaczenie całej instrukcji ma być zadane jedynie w zależności od znaczeń jej bezpośrednich składowych. Tutaj natomiast znaczenie pętli definiowane jest w zależności od znaczeń jej bezpośrednich składowych (warunku i ciała pętli) i --- od znaczenia tejże pętli. Nie tylko więc wykracza to poza schemat definiowania zapewniający kompozycjonalność semantyki, ale wręcz sprawia wrażenie, że tak określone znaczenie pętli nie musi być dobrze zdefiniowane.
Jak więc interpretować taką "definicję"?
Mamy tu do czynienia z równaniem, gdzie wartość "niewiadomej" (znaczenie pętli) ma być równa wartości pewnego operatora (funkcji wyższego rzędu) na tejże wartości. Ten operator zadany jest pewnym wyrażeniem matematycznym, definiującym wartość w dziedzinie semantycznej dla instrukcji, gdy dana jest dowolna wartość w tej dziedzinie. Oczywistym wymaganiem jest, by wyznaczona takim równaniem wartość była punktem stałym tego operatora, tzn. by aplikacja tego operatora do wyznaczonej wartości dawała jako wynik tę wartość.
