SW wykład 5 - Slajd6
Bloki i deklaracje Lokacje Funkcje semantyczne Konwencje notacyjne Instrukcje Klauzule semantyczne Klauzule semantyczne, c.d. Deklaracje Deklaracje, c.d. Semantyka bloków Procedury Wiązania zmiennych Semantyka Tiny++ Semantyka Tiny++ Rekurencja Semantyka procedur rek. Semantyka procedur rek.
Klauzule semantyczne dla poszczególnych konstrukcji językowych definiujących instrukcje języka TINY są teraz dość oczywiste.
Semantyką instrukcji przypisania jest funkcja, która dowolnemu środowisku oraz dowolnemu składowi przypisuje skład końcowy będący modyfikacją składu początkowego przez przypisanie lokacji, którą środowisko podaje dla danej zmiennej, wartości wyliczonej w tym środowisku i składzie początkowym przez semantykę wyrażenia po prawej stronie instrukcji przypisania. Oczywiście, zgodnie z wcześniej wprowadzoną konwencją, propagowane są wszelkie błędy, które tu mogą się pojawić w dwóch sytuacjach. Po pierwsze, błąd się pojawi, gdy zmienna, na którą przypisujemy, nie oznacza w danym środowisku lokacji (a więc, nie została wcześniej zadeklarowana). A po drugie, błąd pojawi się także, gdy wyrażenie po prawej stronie instrukcji przypisania nie definiuje w danym środowisku i składzie wartości liczbowej. Ten ostatni problem może się pojawić na przykład przy wykorzystywaniu w wyrażeniu zmiennych, którym uprzednio nie przypisano wartości (a wiec lokacja przypisana takiej zmiennej w środowisku, w danym składzie nie będzie miała przypisanej wartości liczbowej).
Semantyki instrukcji pustej nie warto niemal omawiać: w każdym środowisku określa ona funkcję identycznościową ze składów w składy.
Semantyka instrukcji złożonej w danym środowisku określa funkcję, która dla danego składu najpierw wyznacza skład pośredni, będący wynikiem semantyki pierwszej składowej instrukcji w tymże środowisku dla tego składu początkowego, a następnie podaje jako wynik skład otrzymany jako wynik semantyki drugiej instrukcji składowej w tym samym środowisku dla tak otrzymanego składu. Oczywiście, zgodnie z naszą konwencją, gdyby wynik pierwszej składowej nie był składem (a błędem abstrakcyjnym), to wynikiem jest błąd abstrakcyjny. Warto tu zwrócić uwagę na sposób przekazywania środowiska, w którym odbywa się modyfikacja składów określona przez instrukcje składowe.
Semantyka instrukcji warunkowej powinna też być oczywista (przy zupełnie naturalnym rozumieniu notacji wprowadzającej pomocniczą wartość wyrażenia warunkowego w danym środowisku i składzie początkowym oraz notacji warunkowego określenia wartości). Znów ważne jest przekazywanie tego samego środowiska bez zmian "w dół", do instrukcji składowych w obu gałęziach instrukcji warunkowej (a wcześniej do wyliczenia wartości wyrażenia logicznego).
I w końcu instrukcja pętli, której opis semantyczny łączy w gruncie rzeczy techniki wykorzystane w poprzednich klauzulach (w szczególności semantykę instrukcji warunkowej, pustej i złożonej) z definicją stałopunktową --- zupełnie podobną do tej podanej w poprzedniej wersji semantyki denotacyjnej języka TINY, wykorzystującej składy. Nie będziemy się jeszcze jakiś czas zajmować pełną analizą definicji stałopunktowych; intuicje przedstawione w poprzednim module i tu powinny być wystarczające. Tam: definiowaliśmy funkcje ze stanów stany, przez iterowanie odpowiedniego operatora wyższego rzędu na takich funkcjach. Tu podobnie definiujemy funkcje ze składów w składy, stopniowo rozszerzając zakres ich określoności po kolejnych iteracjach operatora opisującego jeden krok pętli.
