SW wykład 4 - Slajd10
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
I wreszcie doszliśmy do najciekawszych definicji dla instrukcji języka TINY. Podajemy na powyższym slajdzie klauzule semantyczne dla poszczególnych konstrukcji językowych budujących instrukcje. Przypomnijmy: znaczeniami instrukcji są funkcje (częściowe) ze stanów w stany. Zauważmy i tu, że stany pojawiają się jednak bezpośrednio jedynie w klauzuli dla instrukcji przypisania: tu już nie może być inaczej, musimy bezpośrednio podać sposób modyfikacji stanu przez instrukcję przypisania. Modyfikacja ta jest oczywista: zmieniamy wartość stanu dla zmiennej, na którą wykonywane jest przypisanie, na określoną w danym stanie wartość przypisywanego wyrażenia.
Klauzula dla instrukcji pustej jest oczywista: jej znaczeniem jest funkcja identycznościowa (stan pozostaje bez zmian).
Klauzula dla złożenia sekwencyjnego instrukcji określa jego znaczenie jako złożenie znaczeń jego składowych (przypomnijmy raz jeszcze: znaczeń jako funkcji częściowych na stanach).
Klauzula dla instrukcji warunkowej definiuje znaczenie tej instrukcji jako funkcję na stanach określoną przez wybór modyfikacji stanu zadanej przez odpowiednią gałąź instrukcji, wybraną w zależności od wartości warunku (wyrażenia logicznego) w poszczególnych stanach.
W końcu klauzula dla pętli zadaje jej znaczenie nieco podobnie, przez wybór pomiędzy przekształceniem identycznościowym (gdy wartością wyrażenia logicznego w danym stanie jest prawda) a złożeniem przekształcenia, będącego znaczeniem ciała funkcji oraz przekształcenia będącego znaczeniem całej pętli.
