SW wykład 5 - Slajd8: Różnice pomiędzy wersjami

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
Arturas (dyskusja | edycje)
Nie podano opisu zmian
Tarlecki (dyskusja | edycje)
Nie podano opisu zmian
Linia 1: Linia 1:
{{Semantyka i weryfikacja programów/Wykład 5}}
{{Semantyka i weryfikacja programów/Wykład 5}}
[[Grafika:sw0507.png|center|frame]]
[[Grafika:sw0507.png|center|frame]]
Dla podania klauzuli określającej semantykę instrukcji bloku niezbędna
jest jednak semantyka deklaracji zmiennych.  Inaczej niż w przypadku
instrukcji, deklaracje mogą zmieniać środowisko (to jest przecież
właśnie ich głównym zadaniem: wprowadzenie do środowiska nowych
zmiennych), a przy tym mogą też modyfikować skład (choćby po to, by
zarejestrować deklarację nowej zmiennej, czy zainicjalizować
przypisaną jej lokację --- choć akurat tego drugiego zabiegu tu nie
będziemy przeprowadzać). Zatem znaczeniami deklaracji będą funkcje,
które kolejno przyjmą jaka swoje argumenty środowisko i skład, a w
wyniku podadzą parę: (zmodyfikowane) środowisko i skład. Oczywiście,
nadal dopuszczamy tu pojawienie się błędu (choć akurat w dotychczas
wprowadzonych deklaracjach nie będą się one pojawiać).
Klauzula semantyczna dla pustego ciągu deklaracji jest oczywista:
wynikiem deklaracji dla danego środowiska i składu jest para złożona z
tegoż środowiska i składu.
Elaborując deklarację zmiennej w danym środowisku i składzie, najpierw
wyznaczamy nową (dotychczas niewykorzystywaną) lokację, modyfikujemy
środowisko, przypisując tę lokację deklarowanej zmiennej, i
modyfikujemy skład, przypisując tej lokacji "błąd" (wartość zmiennej
nie zostaje określona). Tak zmodyfikowane środowisko i ten nowy skład
przekazujemy dalej, do semantyki ciągu pozostałych deklaracji.
Jedyny tu kłopot to pojawienie się nowej funkcji, wybierającej
niewykorzystywaną dotychczas lokację. Nie da się jej zdefiniować bez
wniknięcia głębiej w naturę lokacji i składów.

Wersja z 21:00, 25 wrz 2006

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

Dla podania klauzuli określającej semantykę instrukcji bloku niezbędna jest jednak semantyka deklaracji zmiennych. Inaczej niż w przypadku instrukcji, deklaracje mogą zmieniać środowisko (to jest przecież właśnie ich głównym zadaniem: wprowadzenie do środowiska nowych zmiennych), a przy tym mogą też modyfikować skład (choćby po to, by zarejestrować deklarację nowej zmiennej, czy zainicjalizować przypisaną jej lokację --- choć akurat tego drugiego zabiegu tu nie będziemy przeprowadzać). Zatem znaczeniami deklaracji będą funkcje, które kolejno przyjmą jaka swoje argumenty środowisko i skład, a w wyniku podadzą parę: (zmodyfikowane) środowisko i skład. Oczywiście, nadal dopuszczamy tu pojawienie się błędu (choć akurat w dotychczas wprowadzonych deklaracjach nie będą się one pojawiać).

Klauzula semantyczna dla pustego ciągu deklaracji jest oczywista: wynikiem deklaracji dla danego środowiska i składu jest para złożona z tegoż środowiska i składu.

Elaborując deklarację zmiennej w danym środowisku i składzie, najpierw wyznaczamy nową (dotychczas niewykorzystywaną) lokację, modyfikujemy środowisko, przypisując tę lokację deklarowanej zmiennej, i modyfikujemy skład, przypisując tej lokacji "błąd" (wartość zmiennej nie zostaje określona). Tak zmodyfikowane środowisko i ten nowy skład przekazujemy dalej, do semantyki ciągu pozostałych deklaracji.

Jedyny tu kłopot to pojawienie się nowej funkcji, wybierającej niewykorzystywaną dotychczas lokację. Nie da się jej zdefiniować bez wniknięcia głębiej w naturę lokacji i składów.