SW wykład 5 - Slajd14: 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:sw0513.png|center|frame]]
[[Grafika:sw0513.png|center|frame]]
Podajemy nowe klauzule semantyczne dla instrukcji i deklaracji
procedur (klauzule dla pozostałych kategorii języka nie ulegają
zmianie).
Większość klauzul dla instrukcji zmienia się tylko bardzo formalnie:
przekazują one dodane do semantyki środowisko procedur do swoich
instrukcji składowych, poza tym działając tak, jak poprzednio.
Wyjątkiem są tu oczywiście klauzule dla bloków i dla nowej postaci
instrukcji, wywołania procedury. Nowe są też klauzule dla (dodanej)
semantyki deklaracji procedur.
Zacznijmy od tych ostatnich, wyjątkowo tu prostych: klauzula dla
pustego ciągu deklaracji procedur nie wymaga komentarza. Klauzula dla
deklaracji procedury określa po prostu znaczenie jej ciała jako
instrukcji (które to znaczenie, przypomnijmy, jest funkcją pobierającą
kolejno środowisko zmiennych, środowisko procedur, itd.), modyfikuje
środowisko procedur przez przypisanie tego znaczenia identyfikatorowi
właśnie deklarowanej procedury, a w końcu przekazuje tak zmodyfikowane
środowisko procedur do dalszego ciągu deklaracji procedur.
Semantyka bloków z deklaracjami procedur też jest dość
oczywista. Rożni się ona od semantyki bloków w dotychczasowej postaci
(bez deklaracji procedur) tylko przez wprowadzenie dodatkowego
środowiska procedur, jego modyfikacji przez deklaracje procedur i
przekazanie zmodyfikowanego środowiska do ciała bloku.
W końcu, semantyka wywołania procedury w danym środowisku zmiennych i
środowisku procedur, jest funkcją przekształcająca składy dokładnie
tak, jak funkcja wyznaczona przez zawarte w tym drugim środowisku
znaczenie wywoływanej procedury dla tego samego samych środowiska
zmiennych i tego samego środowiska procedur.
Klauzule te są jednak proste tylko z pozoru. Występują w nich ukryte
współzależności, które sprawiają, że w istocie mamy tu do czynienia z
dość skomplikowanym układem równań stałopunktowych. Deklaracje
procedur przypisują ich identyfikatorom semantykę instrukcji, która z
kolei wykorzystuje semantykę instrukcji wywołania procedury, która z
kolei wykorzystuje znaczenia instrukcji przypisane deklarowanym
procedurom przez ich deklaracje. Mamy nadzieję, że "operacyjne"
czytanie tych klauzul jest intuicyjnie jasne; bez wnikania w
systematyczne rozwiązywanie takich układów równań, wskażmy tylko, że
nie różni się to bardzo istotnie od przypadku instrukcji pętli. Co
najważniejsze, zachowana jest zgodność pomiędzy najmniejszymi
rozwiązaniami pojawiających się tu układów równań a intuicyjnie jasną
semantyką operacyjną.

Wersja z 21:03, 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.

Podajemy nowe klauzule semantyczne dla instrukcji i deklaracji procedur (klauzule dla pozostałych kategorii języka nie ulegają zmianie).

Większość klauzul dla instrukcji zmienia się tylko bardzo formalnie: przekazują one dodane do semantyki środowisko procedur do swoich instrukcji składowych, poza tym działając tak, jak poprzednio. Wyjątkiem są tu oczywiście klauzule dla bloków i dla nowej postaci instrukcji, wywołania procedury. Nowe są też klauzule dla (dodanej) semantyki deklaracji procedur.

Zacznijmy od tych ostatnich, wyjątkowo tu prostych: klauzula dla pustego ciągu deklaracji procedur nie wymaga komentarza. Klauzula dla deklaracji procedury określa po prostu znaczenie jej ciała jako instrukcji (które to znaczenie, przypomnijmy, jest funkcją pobierającą kolejno środowisko zmiennych, środowisko procedur, itd.), modyfikuje środowisko procedur przez przypisanie tego znaczenia identyfikatorowi właśnie deklarowanej procedury, a w końcu przekazuje tak zmodyfikowane środowisko procedur do dalszego ciągu deklaracji procedur.

Semantyka bloków z deklaracjami procedur też jest dość oczywista. Rożni się ona od semantyki bloków w dotychczasowej postaci (bez deklaracji procedur) tylko przez wprowadzenie dodatkowego środowiska procedur, jego modyfikacji przez deklaracje procedur i przekazanie zmodyfikowanego środowiska do ciała bloku.

W końcu, semantyka wywołania procedury w danym środowisku zmiennych i środowisku procedur, jest funkcją przekształcająca składy dokładnie tak, jak funkcja wyznaczona przez zawarte w tym drugim środowisku znaczenie wywoływanej procedury dla tego samego samych środowiska zmiennych i tego samego środowiska procedur.

Klauzule te są jednak proste tylko z pozoru. Występują w nich ukryte współzależności, które sprawiają, że w istocie mamy tu do czynienia z dość skomplikowanym układem równań stałopunktowych. Deklaracje procedur przypisują ich identyfikatorom semantykę instrukcji, która z kolei wykorzystuje semantykę instrukcji wywołania procedury, która z kolei wykorzystuje znaczenia instrukcji przypisane deklarowanym procedurom przez ich deklaracje. Mamy nadzieję, że "operacyjne" czytanie tych klauzul jest intuicyjnie jasne; bez wnikania w systematyczne rozwiązywanie takich układów równań, wskażmy tylko, że nie różni się to bardzo istotnie od przypadku instrukcji pętli. Co najważniejsze, zachowana jest zgodność pomiędzy najmniejszymi rozwiązaniami pojawiających się tu układów równań a intuicyjnie jasną semantyką operacyjną.