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

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
Arturas (dyskusja | edycje)
Nie podano opisu zmian
Dorota (dyskusja | edycje)
Nie podano opisu zmian
 
(Nie pokazano 1 wersji utworzonej przez jednego użytkownika)
Linia 1: Linia 1:
{{Semantyka i weryfikacja programów/Wykład 5}}
{{Semantyka i weryfikacja programów/Wykład 5}}
[[Grafika:sw0516.png|center|frame]]
[[Grafika:sw0516.png|center|frame]]
Podajemy tu klauzule semantyczne dla instrukcji i deklaracji procedur
rozszerzonego języka TINY w wersji dla wiązania statycznego. Istotnie
nowe i inne niż dla wersji z wiązaniem dynamicznym są tylko klauzule
dla deklaracji procedur i dla ich wywołań (inna formalnie jest też
klauzula dla bloków, która dodatkowo musi przekazać środowisko
zmiennych do semantyki deklaracji procedur).
Najistotniejsza jest tu klauzula dla deklaracji procedury: wyraźnie
wskazujemy, jaki zasięg ma możliwe rekurencyjne uwikłanie semantyki
procedury przez stałopunktową definicję znaczenia procedury jako
funkcji zadanej przez znaczenie jej ciała w danym środowisku zmiennych
i środowisku procedur zmodyfikowanym wyraźnie przez przypisanie
rekurencyjnie definiowanej funkcji ze składów w składy jako znaczenia
deklarowanej procedury. Reszta to już tylko techniczne szczegóły
przekazania odpowiednio zmodyfikowanego środowiska procedur do ciągu
pozostałych deklaracji.
Klauzula dla wywołań procedury nie zawiera już żadnych (ani jawnych,
ani niejawnych) komplikacji: znaczeniem wywołania procedury w danym
środowisku zmiennych i procedur jest funkcja ze składów w składy,
która jest przypisana wywoływanej procedurze w odpowiednim
środowisku. Zauważmy, że środowisko zmiennych i pozostałe wartości
przechowywane w środowisku procedur nie mają wpływu na sposób
przekształcania składu przez wywołanie procedury.

Aktualna wersja na dzień 14:31, 29 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 tu klauzule semantyczne dla instrukcji i deklaracji procedur rozszerzonego języka TINY w wersji dla wiązania statycznego. Istotnie nowe i inne niż dla wersji z wiązaniem dynamicznym są tylko klauzule dla deklaracji procedur i dla ich wywołań (inna formalnie jest też klauzula dla bloków, która dodatkowo musi przekazać środowisko zmiennych do semantyki deklaracji procedur).

Najistotniejsza jest tu klauzula dla deklaracji procedury: wyraźnie wskazujemy, jaki zasięg ma możliwe rekurencyjne uwikłanie semantyki procedury przez stałopunktową definicję znaczenia procedury jako funkcji zadanej przez znaczenie jej ciała w danym środowisku zmiennych i środowisku procedur zmodyfikowanym wyraźnie przez przypisanie rekurencyjnie definiowanej funkcji ze składów w składy jako znaczenia deklarowanej procedury. Reszta to już tylko techniczne szczegóły przekazania odpowiednio zmodyfikowanego środowiska procedur do ciągu pozostałych deklaracji.

Klauzula dla wywołań procedury nie zawiera już żadnych (ani jawnych, ani niejawnych) komplikacji: znaczeniem wywołania procedury w danym środowisku zmiennych i procedur jest funkcja ze składów w składy, która jest przypisana wywoływanej procedurze w odpowiednim środowisku. Zauważmy, że środowisko zmiennych i pozostałe wartości przechowywane w środowisku procedur nie mają wpływu na sposób przekształcania składu przez wywołanie procedury.