SW wykład 4 - Slajd9

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

Wprowadzone notacje pozwalają na zwięzły i (mamy nadzieję) jasny zapis klauzul semantycznych. Zaczynamy tutaj od trywialnych klauzul dla semantyki stałych liczbowych. Dalej podajemy klauzule dla poszczególnych konstrukcji językowych budujących wyrażenia arytmetyczne i logiczne. Definiujemy tu znaczenia wyrażeń jako funkcje ze stanów w dziedziny liczb całkowitych i wartości logicznych, odpowiednio dla wyrażeń arytmetycznych i logicznych. Warto porównać te definicje z podanymi w module o semantyce operacyjnej (wykład 2, slajdy 13 i 14): zdefiniowane funkcje są tożsame, poszczególne klauzule definiują te same znaczenia dla wyrażeń, ale styl ich zapisu jest inny. Tu: znacznie bardziej zwarty i właśnie operujący wprost na funkcjach, z definiowaniem ich wyników dla poszczególnych stanów "zamkniętym" w wykorzystywanej notacji. Wyraźnie też widać, że znaczenie każdej z podanych fraz języka jest tu zależne jedynie od znaczeń jej bezpośrednich składowych.