SW wykład 5 - Slajd6

<<powrót do strony wykładu

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 i dalej, 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.