SW wykład 5 - Slajd2
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.
Okazuje się, że opis semantyki bloków z deklaracjami lokalnych zmiennych w terminach dziedzin semantycznych dla najprostszej wersji języka TINY w poprzednim module, choć zapewne możliwy, byłby kłopotliwy i raczej niezgrabny. Co więcej, dalsze jego uogólnianie na kolejne konstrukcje językowe szybko okazałoby się niezmiernie trudne, jeśli w ogóle możliwe. Podstawowym kłopotem jest tu podwójna rola, którą pełnią w programach zmienne przy dotychczasowej definicji stanu. Otóż, gdy przyporządkowanie zmiennym odpowiadających im wartości odbywa się bezpośrednio, zmienne są nie tylko identyfikatorami występującymi w programach, ale odgrywają też rolę komórek (czy adresów) pamięci, przechowujących ostatnio przypisane im wartości. Gdy ten sam identyfikator może być zadeklarowany więcej niż jeden raz (w kolejno zagnieżdżonych blokach), co sprawia, że niejako "jednocześnie" może mu odpowiadać więcej niż jedna wartość, nie bardzo wiadomo, jak prosto modelować to zjawisko w semantyce z "bezpośrednimi" stanami. Sytuacja skomplikuje się jeszcze bardziej, gdy wprowadzenie procedur z parametrami doprowadzi do możliwości jednoczesnej modyfikacji tych wielu "wcieleń" danego identyfikatora, czy też wówczas, gdy opisywać będziemy chcieli wskaźniki, gdzie modyfikacja wartości jednej zmiennej niejawnie może oznaczać także modyfikację wartości innych zmiennych.
Piękne rozwiązanie (można je śmiało przypisać Christopherowi Stracheyowi, jak wiele innych idei w dziedzinie denotacyjnego opisu języków programowania) dla tych wszystkich problemów pojawiło się w semantyce denotacyjnej przez rozdzielenie roli zmiennej jako identyfikatora od roli "komórki pamięci". Formalnie oznacza to, że przypisanie wartości zmiennym modelowane jest teraz w dwóch krokach: przez zadane środowiskami przypisanie identyfikatorom zmiennych ich lokacji, a dalej przez zadane składami przypisanie lokacjom wartości. Wprowadzamy więc nową dziedzinę lokacji (na razie nie definiując jej dokładniej); lokacje modelują nieformalne pojęcie adresu komórki pamięci przechowującej wartości. Wprowadzamy też dwie kolejne nowe dziedziny semantyczne: środowiska, przypisujące zmiennym lokacje, i składy, przypisujące lokacjom wartości liczbowe. Przy okazji, wprowadzamy możliwość wyraźnego oznaczenia sytuacji, gdy zmienna nie została jeszcze zadeklarowana w danym środowisku (przez przypisanie tej zmiennej specjalnego symbolu "abstrakcyjnego błędu", czy "nieokreślenia"), oraz gdy zawartość lokacji w danym stanie nie została jeszcze podana (przez przypisanie tej lokacji w składzie specjalnego symbolu "abstrakcyjnego błędu", czy "nieokreślenia"). Pomijając kłopoty z nieokreślonością, można myśleć, że każdą parę środowisko i skład można "złożyć", otrzymując reprezentowany przez tę parę stan.
