Semantyka i weryfikacja programów/Ćwiczenia 5

From Studia Informatyczne

Spis treści

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


Semantyka naturalna pewnej instrukcji \mathbf{for}\,

Ćwiczenie 1


Rozszerzamy język TINY następująco:

I \, ::= \,\,           \ldots \,\,|\,\,           \mathbf{for}\, x = e_1 \,\mathbf{to}\, e_2 \,\mathbf{try}\, I_1 \,\mathbf{else}\, I_2 \,\,|\,\,           \mathbf{fail}

Znaczenie instrukcji \mathbf{for}\, x = e_1 \,\mathbf{to}\, e_2 \,\mathbf{try}\, I_1 \,\mathbf{else}\, I_2 jest następujące. Obliczamy wartości wyrażeń e_1 i e_2. Jeśli pierwsza z nich jest mniejsza od lub równa drugiej, podstawiamy pierwszą wartość (wartość wyrażenia e_1) na zmienną x i uruchamiamy I_1. Jeśli w I_1 nie zostanie napotkana instrukcja \mathbf{fail}, kończymy instrukcję \mathbf{for}\, i przyracamy wartość zmiennej x sprzed tej instrukcji. Natomiast jeśli w I_1 zostanie napotkana instrukcja \mathbf{fail}, podstawiamy na x kolejną, o jeden większą wartość, przywracamy wartości wszystkich pozostałych zmiennych sprzed instrukcji \mathbf{for}\, i ponownie wykonujemy I_1. Powtarzamy w ten sposób, aż I_1 zakończy się nie napotkawszy \mathbf{fail}, albo wartość zmiennej x przekroczy wartość wyrażenia e_2 obliczoną na początku. W pierwszym przypadku kończymy instrukcję \mathbf{for}\, i przyracamy wartość zmiennej x sprzed tej instrukcji. W drugim przywracamy wartości wszystkich zmiennych sprzed instrukcji \mathbf{for}\, i uruchamiamy I_2.


Przykład

Oto przykładowy program:

x := 0; y := 1;
\mathbf{for}\, x := 1 \,\mathbf{to}\, 5 \,\mathbf{try}\,
  y := y+1;
  \mathbf{if}\, x <= 4 \,\mathbf{then}\, \mathbf{fail} \,\mathbf{else}\, z:= x
\,\mathbf{else}\, \mathbf{skip}


Wartości zmiennych po zakończeniu programu to: x = 0, y = 2, z = 5.


Rozwiązanie

Będziemy posługiwać się jak zwykle tranzycjami postaci:

I, s \,\longrightarrow\, s' \quad \quad \quad e, s \,\longrightarrow\, n.

Zacznijmy od najprostszego przypadku, gdy nie ma wogóle potrzeby uruchamiania instrukcji wewnętrznej I_1, ponieważ wartość wyrażenia e_1 jest większa od e_2:

\frac{e_1, s \,\longrightarrow\, n_1       \quad \quad       e_2, s \,\longrightarrow\, n_2       \quad \quad       I_2, s \,\longrightarrow\, 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 > n_2.

Po prostu uruchamiamy instrukcję I_2 w stanie s, ignorując I_1.

Kolejny nietrudny przypadek to sytuacja, w której n_1 \leq n_2, a wykonanie instrukcji wewnętrznej I_1 kończy się sukcesem, tzn. nie następuje wywołanie instrukcji \mathbf{fail}.

Oto reguła dla tego przypadku:

\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\, s'}      {\mathbf{for}\, x = e_1 \,\mathbf{to}\, e_2 \,\mathbf{try}\, I_1 \,\mathbf{else}\, I_2, s \,\longrightarrow\, s'[x \mapsto s(x)]} \quad \mbox{ o ile } n_1 \leq n_2.

Tym razem uruchamiamy instrukcję I_1, podstawiając na zmienną x wartość n_1.

Zwróćmy uwagę, że po zakończeniu I_1 przywracamy wartość zmiennej x sprzed jej wykonania.

Pozostał nam trzeci przypadek, gdy n_1 \leq n_2, a wykonanie instrukcji I_1 zakończyło się wykonaniem instrukcji \mathbf{fail} gdzieś wewnątrz I_1.

Aby poprawnie opisać takie zdarzenie, potrzebujemy dodatkowych tranzycji postaci:

I, s \,\longrightarrow\, \mbox{było-}\mathbf{fail}.

Mówiąc formalnie, poszerzamy zbiór konfiguracji o jeden element \mbox{było-}\mathbf{fail}.

Zauważmy, że po prawej stronie tranzycji nie ma wogóle stanu. Nie potrzebujemy go dla opisania semantyki instrukcji \mathbf{for}\,: jeśli wystąpi \mathbf{fail}, powtarzamy I_1 dla większej o 1 wartości zmiennej x, ale pozostałym zmiennym przywracamy wartość sprzed I_1. A więc załóżmy, że

I_1, s[x \mapsto n_1] \,\longrightarrow\, \mbox{było-}\mathbf{fail}.

W takiej sytuacji powinniśmy przypisać n_1 + 1 na zmienną x i spróbować ponownie wykonać I_1 przy wartościach wszystkich pozostałych zmiennych, takich jak na początku instrukcji \mathbf{for}\,.

Powtarzamy ten schemat aż do skutku, tzn. aż do mementu, gdy zaistnieje któraś z poprzednich dwóch (prostych) sytuacji. Oto odpowiednia reguła:

\frac{e_1, s \,\longrightarrow\, n_1       \quad       e_2, s \,\longrightarrow\, n_2       \quad       I_1, s[x \mapsto n_1]  \,\longrightarrow\, \mbox{było-}\mathbf{fail}       \quad       \mathbf{for}\, x = e_1 + 1 \,\mathbf{to}\, e_2 \,\mathbf{try}\, I_1 \,\mathbf{else}\, I_2, s \,\longrightarrow\, 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 \mathbf{for}\, x = e_1 + 1 \,\mathbf{to}\, e_2 \,\mathbf{try}\, I_1 \,\mathbf{else}\, I_2 otrzymujemy stan s', w którym nie przywracamy wartości zmiennej x.

Gdybyśmy tak zrobili, tzn. gdybyśmy zastąpili s' przez s'[x \mapsto s(x)], nasze semantyka byłaby niepoprawna. Dlaczego? Dlatego, że nie wiemy tak naprawdę, czy powinniśmy przywracać wartość zmiennej x, czy nie. Jeśli ostatecznie nasza instrukcja \mathbf{for}\, zakończyła się przez bezbłędne zakończenie instrukcji I_1 (przypadek drugi), to powinniśmy to zrobić; ale jeśli zakończyła się wykonaniem instrukcji I_2 (przypadek pierwszy), powinniśmy pozostawić wartość zmiennej x taką, jaka jest ona po zakończeniu I_2. A zatem w powyższej regule dla przypadku trzeciego nie przywracamy wartości zmiennej x; 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 \mathbf{for}\, x = e_1 + 1 \,\mathbf{to}\, e_2 \,\mathbf{try}\, I_1 \,\mathbf{else}\, I_2 wykonywana jest w orginalnym stanie s, a nie w stanie, w którym kończy się I_1 (tego ostatniego stanu nawet nie znamy).

Jeszcze jeden drobiazg: zamiast e_1 {+} 1 w \mathbf{for}\, x = e_1 + 1 \,\mathbf{to}\, e_2 \,\mathbf{try}\, I_1 \,\mathbf{else}\, I_2, s \,\longrightarrow\, s' w regule powyżej, moglibyśmy podstawić policzoną już wartość, czyli n_1 {+} 1.

Na zakończenie prezentujemy reguły niebędne do tego, aby wygenerować \mbox{było-}\mathbf{fail}:

\mathbf{fail}, s \,\longrightarrow\, \mbox{było-}\mathbf{fail}

oraz aby wystąpienie \mathbf{fail} umiejscowione gdzieś "głęboko" zostało rozpropagowane do najbliższej otaczającej instrukcji \mathbf{for}\,.

Jeśli pojawił się \mathbf{fail}, powinniśmy zaniechać dalszego wykonania instrukcji, a w przypadku pętli, powinniśmy zaniechać dalszego iterowania tej pętli. Oto odpowiednie reguły:

\frac{I_1, s \,\longrightarrow\, \mbox{było-}\mathbf{fail}}      {I_1;\, I_2, s \,\longrightarrow\, \mbox{było-}\mathbf{fail}} \quad \quad \frac{I_1, s \,\longrightarrow\, s' \quad \quad I_2, s' \,\longrightarrow\, \mbox{było-}\mathbf{fail}}      {I_1;\, I_2, s \,\longrightarrow\, \mbox{było-}\mathbf{fail}}

\frac{b, s \,\longrightarrow\, \mathbf{true} \quad \quad I_1, s \,\longrightarrow\, \mbox{było-}\mathbf{fail}}      {\mathbf{if}\, b \,\mathbf{then}\, I_1 \,\mathbf{else}\, I_2, s \,\longrightarrow\, \mbox{było-}\mathbf{fail}} \quad \quad \mbox{ i analogicznie gdy } b, s \,\longrightarrow\, \mathbf{false}

\frac{b, s \,\longrightarrow\, \mathbf{true} \quad \quad I, s \,\longrightarrow\, \mbox{było-}\mathbf{fail}}      {\mathbf{while}\, b \,\mathbf{do}\, I, s \,\longrightarrow\, \mbox{było-}\mathbf{fail}} \quad \quad \frac{b, s \,\longrightarrow\, \mathbf{true} \quad \quad I, s \,\longrightarrow\, s' \quad \quad       \mathbf{while}\, b \,\mathbf{do}\, I, s' \,\longrightarrow\, \mbox{było-}\mathbf{fail}}      {\mathbf{while}\, b \,\mathbf{do}\, I, s \,\longrightarrow\, \mbox{było-}\mathbf{fail}}

Widać podobieństwo do analogicznych reguł dla pętli \mathbf{loop}\, I, którą zajmowaliśmy się na wcześniejszych zajęciach.

Zauważmy, że jeśli \mathbf{fail} zostało wykonane poza jakąkolwiek pętlą \mathbf{for}\,, to program "zakończy się" w konfiguracji \mbox{było-}\mathbf{fail}.

Możemy zatem tę właśnie konfigurację uznać za konfigurację końcową, informującą o porażce wykonania programu.


Semantyka naturalna bloków

Ćwiczenie 2 (bloki i deklaracje zmiennych)

Rozszerz semantykę języka TINY o deklarację zmiennej:

I \, ::= \,\,       \ldots  \,\,|\,\,      \mathbf{begin}\, \mathbf{var}\, x = e;\, I \,\mathbf{end}

Zasięgiem zmiennej x jest instrukcja I, czyli wnętrze bloku, w którym jest zadeklarowana. Zakładamy zwykłe (statyczne) reguły widoczności, przesłaniania, itp.


Rozwiązanie

Wariant 1 (tylko stan)


Oczywiście powinniśmy odróżniać zmienne zadeklarowane (i zarazem zainicjowane) od tych niezadeklarowanych.

Zatem przyjmijmy, że

\mathbf{State} = \mathbf{Var} \to_{\mathrm{fin}} \mathbf{Num}.

Zachowujemy wszystkie reguły semantyczne dla języka Tiny i dodajemy jedną nową:

\frac{e, s \,\longrightarrow\, n \quad \quad I, s[x \mapsto n] \,\longrightarrow\, s'}      {\mathbf{begin}\, \mathbf{var}\, x = e;\, I \,\mathbf{end}, s \,\longrightarrow\, s'}

mówiącą, że instrukcja wewnętrzna I ewaluowana jest w stanie, w którym dodatkowo zaznaczono wartość zmiennej x równą wartości, do której oblicza się e.

Oczywiście takie rozwiązanie jest niepoprawne, gdyż wartość zmiennej x pozostaje w stanie nawet po wyjściu z bloku ("wycieka" z bloku). Musimy dodać "dealokację" zmiennej x:

\frac{e, s \,\longrightarrow\, n \quad \quad I, s[x \mapsto n] \,\longrightarrow\, s'}      {\mathbf{begin}\, \mathbf{var}\, x = e;\, I \,\mathbf{end}, s \,\longrightarrow\, s''} \quad \mbox{ o ile } s'' = s'[x \mapsto s(x)]

I znów napotykamy podobne trudności jak na wcześniejszych zajęciach: powyższa reguła nie obejmuje przypadku, gdy s(x) 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.


Wariant 2 (stan i środowisko)

Podstawowy pomysł polega na rozdzieleniu informacji przechowywanej dotychczas w stanie, czyli odwzorowania nazw zmiennych w wartości, na dwa "etapy".

Pierwszy z nich odwzorowuje identyfikatory zmiennych w lokacje, a drugi lokacje w wartości. Mamy więc środowiska E \in \mathbf{Env}, będące funkcjami częściowymi z \mathbf{Var} do \mathbf{Loc}, zbioru lokacji:

\mathbf{Env} = \mathbf{Var} \to_{\mathrm{fin}} \mathbf{Loc}

oraz stany, będące teraz funkcjami częściowymi z \mathbf{Loc} do \mathbf{Num}:

\mathbf{Store} = \mathbf{Loc} \to_{\mathrm{fin}} \mathbf{Num}.

Dla ścisłości używamy innej nazwy (\mathbf{Store}), ale będziemy zwykle używać podobnych symboli jak dotychczas s, s', s_1, \ldots \in \mathbf{Store} itp. do nazywania stanów.

Intuicyjnie można myśleć 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 \mathbf{Loc} = \{ l_0, l_1, \ldots \} i że w każdym momencie tylko skończenie wiele spośród nich jest wykorzystywane.

Formalnie mowiąc, dziedzina funkcji częściowej s jest zawsze skończona. 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 E będzie zawsze zawarty w zbiorze aktualnie używanych lokacji, czyli zawarty w dziedzinie funkcji częściowej s, oznaczanej \mathrm{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:

I, s, E \,\longrightarrow\, s'

czyli instrukcja I będzie modyfikować stan, ale nie będzie zmieniać środowiska E. Dla czytelności będziemy zapisywać nasze reguły w następujący sposób:

E \,\vdash\, I, s \,\longrightarrow\, s'

podkreślając w ten sposób, że środowisko nie ulega zmianie.

Ale należy pamiętać, że konfiguracja, w której "uruchamiamy" instrukcję I składa się naprawdę z trójki (I, s, E).

Deklarując nową zmienną x dodamy po prostu do E parę (x, l), gdzie l jest nową, nieużywaną dotychczas lokacją.

Dla wygody zapisu załóżmy, że mamy do dyspozycji funkcję

\mathtt{newloc} : \mathbf{Store} \to \mathbf{Loc}

która zwraca jakąś nową, nieużywaną lokację. Formalnie wymagamy, by

\mathtt{newloc}(s) \notin \mathrm{dom}(s).

Dla ilustracji popatrzmy na przykładową regułę dla deklaracji.

\frac{E \,\vdash\, e, s \,\longrightarrow\, n \quad \quad       E[x \mapsto l] \,\vdash\, I, s[l \mapsto n] \,\longrightarrow\, s'}      {E \,\vdash\, \mathbf{begin}\, \mathbf{var}\, x=e;\, I \,\mathbf{end}, s \,\longrightarrow\, s'} \quad \mbox{ gdzie } l = \mathtt{newloc}(s).

Zauważmy, że stan s' po zakończeniu instrukcji \mathbf{begin}\, \mathbf{var}\, x=e;\, I \,\mathbf{end} zawiera informację o zmiennej lokalnej x, tzn. s(l) jest określone.

Ale lokacja l jest "nieosiągalna" w środowisku E, gdyż para x \mapsto l została dodana tylko do środowiska, w którym ewaluuje się wnętrze bloku, a środowisko E całego bloku nie jest modyfikowane.

Poniżej przedstawiamy reguły dla pozostałych instrukcji.

Przede wszystkim złożenie sekwencyjne:

\frac{E \,\vdash\, I_1, s \,\longrightarrow\, s'        \quad \quad        E, \,\vdash\, I_2, s' \,\longrightarrow\, s''}      {E \,\vdash\, I_1;\, I_2, s \,\longrightarrow\, s''}

Reguła ta uzmysławia nam różnicę pomiędzy środowiskiem a stanem: środowisko pozostaje to samo, gdy przechodzimy od jednej instrukcji do następnej, 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ń:

E \,\vdash\, e, s \,\longrightarrow\, n

która jest zupełnie naturalna w naszym podejściu opartym o środowiska i stany.

Reguły mogą wyglądać np. tak:

\frac{E \,\vdash\, e, s \,\longrightarrow\, n}      {E \,\vdash\, x := e, s \,\longrightarrow\, s[x \mapsto n]} \quad \quad E \,\vdash\, \mathbf{skip}, s \,\longrightarrow\, s

\frac{E \,\vdash\, b, s \,\longrightarrow\, \mathbf{true}       \quad \quad       E \,\vdash\, I_1, s \,\longrightarrow\, s'}      {E \,\vdash\, \mathbf{if}\, b \,\mathbf{then}\, I_1 \,\mathbf{else}\, I_2, s \,\longrightarrow\, s'} \quad \quad \frac{E \,\vdash\, b, s \,\longrightarrow\, \mathbf{false}       \quad \quad       E \,\vdash\, I_2, s \,\longrightarrow\, s'}      {E \,\vdash\, \mathbf{if}\, b \,\mathbf{then}\, I_1 \,\mathbf{else}\, I_2, s \,\longrightarrow\, s'}

\frac{E \,\vdash\, \mathbf{if}\, b \,\mathbf{then}\, (\mathbf{while}\, b \,\mathbf{do}\, I) \,\mathbf{else}\, \mathbf{skip}, s \,\longrightarrow\, s'}      {E \,\vdash\, \mathbf{while}\, b \,\mathbf{do}\, I, s \,\longrightarrow\, s'}

Reguły dla wyrażeń są oczywiste:

E \,\vdash\, n, s \,\longrightarrow\, n \quad \quad E \,\vdash\, x, s \,\longrightarrow\, n \quad \mbox{ o ile } E(x)=l \in \mathbf{Loc} \mbox{ i } s(l) = n

i tak dalej -- pomijamy pozostałe reguły.


Wariant 3 (dealokacja)

Przypomnijmy sobie semantykę bloku

\frac{E \,\vdash\, e, s \,\longrightarrow\, n \quad \quad       E[x \mapsto l] \,\vdash\, I, s[l \mapsto n] \,\longrightarrow\, s'}      {E \,\vdash\, \mathbf{begin}\, \mathbf{var}\, x=e;\, I \,\mathbf{end}, s \,\longrightarrow\, s'} \quad \mbox{ gdzie } l = \mathtt{newloc}(s)

i zastanówmy się, jak "posprzątać" po zakończeniu wykonania bloku, tzn. zwolnić lokację l, która była używana tylko w tym bloku i w związku z tym nie będzie już potrzebna.

Oznaczałoby to przywrócenie lokacji l do puli wolnych (nieużywanych) lokacji.

Zmodyfikowana reguła dla instrukcji bloku powinna wyglądać mniej więcej tak:

\frac{E \,\vdash\, d, s \,\longrightarrow\, (E', s')       \quad \quad      E' \,\vdash\, I, s' \,\longrightarrow\, s''}      {E \,\vdash\, \mathbf{begin}\, d;\, I \,\mathbf{end}, s \,\longrightarrow\, \bar{s}}

gdzie \bar{s} to stan s'' "okrojony" do dziedziny stanu s.

Powinniśmy po prostu przywrócić nieokreśloność stanu dla lokacji l. Natomiast oczywiście nie ma potrzeby dealokownia środowiska! Oto rozwiązanie:

\frac{E \,\vdash\, e, s \,\longrightarrow\, n \quad \quad       E[x \mapsto l] \,\vdash\, I, s[l \mapsto n] \,\longrightarrow\, s'}      {E \,\vdash\, \mathbf{begin}\, \mathbf{var}\, x=e;\, I \,\mathbf{end}, s \,\longrightarrow\, s' \setminus \{ (l, s'(l)) \}} \quad \mbox{ gdzie } l = \mathtt{newloc}(s).

Zadania domowe

Ćwiczenie 1

Napisz semantykę naturalną dla następującego rozszerzenia języka TINY:

I \, ::= \,\,       \ldotes \,\,|\,\,        \mathbf{throw}\, x \,\,|\,\,        \,\mathbf{try}\, I_1 \,\mathbf{catch}\, exc\, I_2

exc \, ::= \,\,        x \,\,|\,\,        \mathbf{any}

Instrukcja \mathbf{throw}\, x oznacza podniesienie wyjątku o nazwie x. Instrukcja I = \,\mathbf{try}\, I_1 \,\mathbf{catch}\, exc\, I_2 wykonuje I_1. Jeśli podczas wykonania I_1 zostanie podniesiony wyjątek x, i exc = x albo exc = \mathbf{any}, to następuje przerwanie I_1 i sterowanie zostaje przeniesione do I_2 (następuje obsługa wyjątku). Jeśli zaś podczas wykonania I_1 zostanie podniesiony wyjątek x oraz exc \neq x i exc \neq \mathbf{any}, to obsługa wyjątku przekazana jest do najbliższej instrukcji \,\mathbf{try}\, otaczającej I. Umawiamy się, że \,\mathbf{try}\, I_1 \,\mathbf{catch}\, exc\, I_2 otacza I_1 i wszystkie instrukcje wewnątrz I_1, ale nie otacza I_2.


Ćwiczenie 2

Zaproponuj modyfikację semantyki, w której deklaracja jest wykonywana "równolegle", analogicznie do przypisania równoległego. Przy takiej semantyce kolejność poszczególnych deklaracji powinna być nieistotna.