Semantyka i weryfikacja programów/Ćwiczenia 5
Zawartość
Kontynuujemy ćwiczenie semantyki naturalnej, dodając pewne konstrukcje do języka Tiny. W szczególności rozszerzymy go o deklaracje zmiennych (bloki). Po raz pierwszy roszdzielimy informację przechowywaną w konfiguracji na środowisko określające wiązanie identyfikatorów i stan przechowujący wartości zmiennych. Będzie to przygotowanie do kolejnych zajęć.
Zadania z rozwiązaniami
Zadanie 1
Rozszerzamy język Tiny następująco:
Znaczenie instrukcji jest następujące. Obliczamy wartości wyrażeń i . Jeśli pierwsza z nich jest mniejsza lub równa od drugiej, to podstawiamy pierwszą wartość (wartość wyrażenia ) na zmienną i uruchamiamy . Jeśli w nie zostanie napotkana instrukcja , kończymy instrukcję i przyracamy wartość zmiennej sprzed tej instrukcji. Natomiast jeśli w zostanie napotkana instrukcja , podstawiamy na kolejną, o jeden większą wartość, przywracamy wartości wszystkich pozostałych zmiennych sprzed instrukcji , i ponownie wykonujemy . Powtarzamy w ten sposób aż zakończy się nie napotkawszy , albo wartość zmiennej przekroczy wartość wyrażenia obliczoną na początku. W pierwszym przypadku kończymy instrukcję i przyracamy wartość zmiennej sprzed tej instrukcji. W drugim przywracamy wartości wszystkich zmiennych sprzed instrukcji i uruchamiamy .
Przykład
Wartości zmiennych po zakończeniu programu to: .
Rozwiązanie
Będziemy posługiwać się jak zwykle tranzycjami postaci:
Zacznijmy od najprostszego przypadku, gdy nie ma wogóle potrzeby uruchamiania instrukcji wewnętrznej , ponieważ wartość wyrażenia jest większa od :
Po prostu uruchamiamy instrukcję w stanie , ignorując .
Kolejny nietrudny przypadek to sytuacja, w której a wykonanie instrukcji wewnętrznej kończy się sukcesem, tzn. nie następuje wywołanie instrukcji . Oto reguła dla tego przypadku:
Tym razem uruchamiamy instrukcję , podstawiając pod zmienną wartość . Zwróćmy uwagę, że po zakończeniu przywracamy wartość zmiennej sprzed jej wykonania.
Pozostał nam trzeci przypadek, gdy a wykonanie instrukcji zakończyło się wykonaniem instrukcji gdzieś wewnątrz . Aby poprawnie opisać takie zdarzenie, potrzebujemy dodatkowych tranzycji postaci:
Mówiąc formalnie, poszerzamy zbiór konfiguracji o jeden element . Zauważmy, że po prawej stronie tranzycji nie ma wogóle stanu. Nie potrzebujemy go dla opisania semantyki instrukcji : jeśli wystąpi , powtarzamy dla większej o wartości zmiennej , ale pozostałym zmiennym przywracamy wartość sprzed . A więc załóżmy, że
W takiej sytuacji powinniśmy przypisać na zmienną i spróbować ponownie wykonać przy wartościach wszystkich pozostałych zmiennych takich, jak na początku instrukcji . I powtarzać ten schemat aż do skutku, tzn. aż do mementu, gdy zaistnieje któraś z poprzednich dwóch (prostych) sytuacji. Oto odpowiednia reguła:
Parser nie mógł rozpoznać (nieznana funkcja „\drok”): {\displaystyle \frac{e_1, s \,\longrightarrow\, n_1 \quad \quad e_2, s \,\longrightarrow\, n_2 \quad \quad I_1, s[x \mapsto n_1] \,\longrightarrow\, \mbox{było-}\mathbf{fail} \quad \quad \mathbf{for}\, x = e_1 + 1 \,\mathbf{to}\, e_2 \,\mathbf{try}\, I_1 \,\mathbf{else}\, I_2, s \drok s'} {\mathbf{for}\, x = e_1 \,\mathbf{to}\, e_2 \,\mathbf{try}\, I_1 \,\mathbf{else}\, I_2, s \,\longrightarrow\, s'} \quad \mbox{ o ile } n_1 \leq n_2. }
Zwróćmy uwagę na pewnien niezwykle istotny szczegół: po zakończeniu wykonania instrukcji otrzymujemy stan , w którym nie przywracamy wartości zmiennej . Gdybyśmy tak zrobili, tzn. gdybyśmy zastąpili przez , nasze semantyka byłaby niepoprawna. Dlaczego? Dlatego, że nie wiemy tak naprawdę, czy powinniśmy przywracać wartość zmiennej czy nie. Jeśli ostatecznie nasza instrukcja zakończyla się przez bezbłędne zakończenie instrukcji (przypadek drugi), to powinniśmy to zrobić; ale jeśli zakończyła się wykonaniem instrukcji (przypadek pierwszy), to powinniśmy pozostawić wartość zmiennej taką, jaka jest ona po zakończeniu . A zatem w powyższej regule dla przypadku trzeciego nie przywracamy wartości zmiennej ; jeśli było to konieczne, to zostało już wykonane ,,głębiej", dzięki regule dla przypadku drugiego oraz dzięki temu, że instrukcja wykonywana jest w orginalnym stanie , a nie w stanie, w którym kończy się (tego ostatniego stanu nawet nie znamy).
Na zakończenie prezentujemy reguły niebędne do tego, aby wygenerować :
oraz aby wystąpienie umiejscowione gdzieś ,,głęboko" zostało rozpropagowane do najbliższej otaczającej instrukcji . Jeśli pojawił się , powinniśmy zaniechać dalszego wykonania instrukcji a w przypadku pętli, powinniśmy zaniechać dalszego iterowania tej pętli. Oto odpowiednie reguły:
Widać podobieństwo do analogicznych reguł dla pętli , którą zajmowaliśmy się na wcześniejszych zajęciach.
Zauważmy, że jesli zostało wykonane poza jakąkolwiek pętlą , to program ,,zakończy się" w konfiguracji . Możemy zatem tę właśnie konfigurację uznać za konfigurację końcową, informującą o porażce wykonania programu.
Zadanie 2 (bloki i deklaracje zmiennych)
Rozszerz semantykę języka Tiny o deklarację zmiennej:
Zasięgiem zmiennej jest instrukcja czyli wnętrze bloku, w którym jest zadeklarowana. Zakładamy zwykłe (statyczne) reguły widoczności, przesłaniania, itp.
Rozwiązanie 1 (tylko stan)
Oczywiście powinniśmy odróżniać zmienne zadeklarowane (i zarazem zainicjowane) od tych niezadeklarowanych. Zatem przyjmijmy, że
.
Zachowuujemy wszystkie reguły semantyczne dla języka Tiny i dodajemy jedną nową:
mówiącą, że instrukcja wewnętrzna ewaluowana jest w stanie, w którym dodatkow zaznaczono wartość zmiennej równą wartości, do której oblicza się . Oczywiście takie rozwiązanie jest niepoprawne, gdyż wartość zmiennej pozostaje w stanie nawet po wyjściu z bloku (,,wycieka" z bloku). Musimy dodać ,,dealokację" zmiennej :
I znów napotykamy podobnie trudności jak na wcześniejszych zajęciach: powyższa reguła nie obejmuje przypadku, gdy jest nieokreślone. I choć moglibyśmy naprawić ten mankament podobnie jak kiedyś (co pozostawiamy Czytelnikowi), istnieje inne, bardzo eleganckie i elastyczne rozwiązanie tego problemu, które teraz omówimy.
Rozwiązanie 2 (stan i środowisko)
Podstawowy pomysł polega na rozdzielenie informacji przechowywanej dotychczas w stanie na dwa ,,etapy". Pierwszy z nich, odwzorowuje identyfikatory zmiennych na lokacje, a drugi lokacje na wartości. Mamy więc środowiska Parser nie mógł rozpoznać (błąd składni): {\displaystyle E \in \mathbf{Env}], będące funkcjami częściowymi z <math> \mathbf{Var} } do , zbioru lokacji:
oraz stany, będące teraz funkcjami częściowymi z do :
Intuicyjnie można myśleć o lokacjach jak o lokacjach w pamięci operacyjnej maszyny. Środowisko zawiera informację o lokacji, w której przechowywana jest wartość danej zmiennej. A stan opisuje właśnie zawartość używanych lokacji.
Zakładamy przy tym, że mamy do dyspozycji nieskończony zbiór lokacji i że w każdym momencie tylko skończenie wiele spośród nich jest wykorzystywane. Formalnie mowiąc, dziedzina funkcji częściowej jest zawsze skończony. Daje nam to pewność, że zawsze jest jakaś nieużywana lokacja.
Środowisko początkowe, w którym uruchamiany będzie program, będzie z reguły puste. Ponadto obraz funkcji częściowej będzie zawsze zawarty w zbiorze aktualnie używanych lokacji, czyli zawarty w dziedzinie funkcji częściowej , oznaczanej Parser nie mógł rozpoznać (nieznana funkcja „\dom”): {\displaystyle \dom(s) } .
Pożytek z tego podziału na dwa etapy będzie taki, że będziemy umieli łatwo i elastycznie opisywać deklaracje zmiennych, przesłanianie identyfikatorów, itp. Tranzycje będą teraz postaci:
czyli instrukcja będzie modyfikować stan ale nie będzie zmieniać środowiska . Dla czytelności będziemy zapisywać nasze reguły w następujący sposób:
podkreślając w ten sposób, że środowisko nie ulega zmianie. Ale należy pamiętać, że konfiguracja, w której ,,uruchamiamy" instrukcję składa się naprawdę z pary .
Deklarując nową zmienną dodamy po prostu do parę , gdzie jest nową, nieużywaną dotychczas lokacją. Dla wygody zapisu załóżmy, że mamy do dyspozycji funkcję funkcję
która zwraca jakąś nową, nieużywaną lokację. Formalnie wymagamy, by
Parser nie mógł rozpoznać (nieznana funkcja „\dom”): {\displaystyle \mathtt{new}(s) \notin \dom(s). }
Dla ilustracji popatrzmy na przykładową regułę dla deklaracji.
Zauważmy, że stan po zakończeniu instrukcji zawiera informację o zmiennej lokalnej , tzn. jest określone. Ale lokacja jest ,,nieosiągalna" w środowisku , gdyż para została dodana tylko do środowiska, w którym ewaluuje się wnętrze bloku, a środowisko całego bloku nie jest modyfikowane.
Poniżej przedstawiamy reguły dla pozostałych instrukcji.
Przede wszystkim złożenie sekwencyjne:
Reguła ta uzmysławia nam różnicę pomiędzy środowiskiem a stanem: środowisko pozostaje to samo, gdy przechodzimy od jednej instrukcji do następn\ej, a stan oczywiście ewoluuje wraz ze zmieniającymi się wartościami zmiennych.
Reguły dla przypisania, instrukcji warunkowej i pętli nie przedstawiają żadnych nowych trudności. Musimy tylko najpierw ustalić postać reguł dla wyrażeń:
która jest zupełnie naturalna w naszym podejściu opartym o środowiska i stany. Reguły mogą wyglądać np. tak:
Reguły dla wyrażeń są oczywiste:
i tak dalej -- pomijamy pozostałe reguły.
Wariant (dealokacja)
Przypomnijmy sobie semantykę bloku
i zastanówmy się, jak ,,posprzątać" po zakończeniu wykonania bloku, tzn. zwolnić lokację , która była używana tylko w tym bloku i w związku z tym nie będzie już potrzebne. Oznaczałoby to przywrócenie lokacji do puli wolnych (nieużywanych) lokacji.
Zmodyfikowana reguła dla instrukcji bloku powinna wyglądać mniej więcej tak:
gdzie to stan ,,okrojony" do dziedziny stanu . Zatem powinniśmy po prostu przywrócić nieokreśloność stanu dla lokacji . Natomiast oczywiście nie ma potrzeby dealokownia środowiska! Oto rozwiązanie:
Zadania domowe
Zadanie 1
Napisz semantykę naturalną dla następującego rozszerzenia języka Tiny:
Parser nie mógł rozpoznać (nieznana funkcja „\ldotes”): {\displaystyle I \, ::= \,\, \ldotes \,\,|\,\, \mathbf{throw}\, x \,\,|\,\, \,\mathbf{try}\, I_1 \,\mathbf{catch}\, exc\, I_2 }
Instrukcja oznacza podniesienie wyjątku o nazwie . Instrukcja wykonuje . Jeśli podczas wykonania zostanie podniesiony wyjątej , i albo , to następuje przerwanie i sterowanie zostaje przeniesione do (następuje obsługa wyjątku). Jeśli zaś podczas wykonania zostanie podniesiony wyjątej , i i , to obsługa wyjątku przekazana jest do najbliższej instrukcji otaczającej . Umawiamy się, że otacza i wszystkie instrukcje wewnątrz , ale nie otacza .
Zadanie 2
Zaproponuj modyfikację semantyki języka Small, w której deklaracja jest wykonywana ,,równolegle\, analogicznie do przypisania równoległego. Przy takiej semantyce kolejność poszczególnych deklaracji nie powinna wpływać na wynik programu.
