SW wykład 5 - Slajd8: Różnice pomiędzy wersjami
Nie podano opisu zmian |
Nie podano opisu zmian |
||
(Nie pokazano 2 wersji utworzonych przez 2 użytkowników) | |||
Linia 1: | Linia 1: | ||
{{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 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. |
Aktualna wersja na dzień 14:10, 29 wrz 2006
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 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.