SW wykład 5 - Slajd5

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

Jak i poprzednio, znacznie ciekawsza od semantyki dla wyrażeń języka TINY jest semantyka jego instrukcji.

Przyjmując, że stanom odpowiadają teraz pary złożone ze środowiska i składu, możliwa oczywista modyfikacja semantyki dla instrukcji mogłaby polegać na prostym zastąpieniu dziedziny stanów przez iloczyn kartezjański dziedzin środowisk i składów. Wówczas znaczeniami instrukcji byłyby funkcje z tej dziedziny w nią samą (z uwzględnieniem możliwości pojawienia się błędów i zapętlenia).

Jednak taka dziedzina semantyczna dla instrukcji byłaby w pewnym sensie zbyt bogata. Nieformalnie bowiem znaczenie funkcji potencjalnie mogłoby odwzorowywać dowolną parę środowisko-skład na dowolną inną (lub tę samą) taką parę. A przecież zupełnie podstawową intuicją jest, że instrukcje języka TINY nie wprowadzają nowych deklaracji, zatem nie modyfikują środowisk, a jedynie modyfikują składy. Tę ważną informację o języku możemy zawrzeć już w definicji dziedziny semantycznej dla instrukcji --- i tak właśnie postąpimy.

Zatem znaczeniami instrukcji języka TINY będą funkcje, które dowolne środowisko (środowisko zadeklarowanych zmiennych, w którym wykonywana jest dana instrukcja) odwzorowują w funkcje ze składów w składy (plus sygnał sytuacji błędnej).