Semantyka i weryfikacja programów/Ćwiczenia 5: Różnice pomiędzy wersjami

Wersja z 08:51, 7 sie 2006

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:

$I : : = \dots | 𝐟 𝐨 𝐫 x = e_{1} 𝐭 𝐨 e_{2} 𝐭 𝐫 𝐲 I_{1} 𝐞 𝐥 𝐬 𝐞 I_{2} | 𝐟 𝐚 𝐢 𝐥$

Znaczenie instrukcji $𝐟 𝐨 𝐫 x = e_{1} 𝐭 𝐨 e_{2} 𝐭 𝐫 𝐲 I_{1} 𝐞 𝐥 𝐬 𝐞 I_{2}$ jest następujące. Obliczamy wartości wyrażeń $e_{1}$ i $e_{2}$ . Jeśli pierwsza z nich jest mniejsza lub równa od drugiej, to podstawiamy pierwszą wartość (wartość wyrażenia $e_{1}$ ) na zmienną $x$ i uruchamiamy $I_{1}$ . Jeśli w $I_{1}$ nie zostanie napotkana instrukcja $𝐟 𝐚 𝐢 𝐥$ , kończymy instrukcję $𝐟 𝐨 𝐫$ i przyracamy wartość zmiennej $x$ sprzed tej instrukcji. Natomiast jeśli w $I_{1}$ zostanie napotkana instrukcja $𝐟 𝐚 𝐢 𝐥$ , podstawiamy na $x$ kolejną, o jeden większą wartość, przywracamy wartości wszystkich pozostałych zmiennych sprzed instrukcji $𝐟 𝐨 𝐫$ , i ponownie wykonujemy $I_{1}$ . Powtarzamy w ten sposób aż $I_{1}$ zakończy się nie napotkawszy $𝐟 𝐚 𝐢 𝐥$ , albo wartość zmiennej $x$ przekroczy wartość wyrażenia $e_{2}$ obliczoną na początku. W pierwszym przypadku kończymy instrukcję $𝐟 𝐨 𝐫$ i przyracamy wartość zmiennej $x$ sprzed tej instrukcji. W drugim przywracamy wartości wszystkich zmiennych sprzed instrukcji $𝐟 𝐨 𝐫$ i uruchamiamy $I_{2}$ .

Przykład

$x : = 0; y : = 1; 𝐟 𝐨 𝐫 x : = 1 𝐭 𝐨 5 𝐭 𝐫 𝐲 y : = y + 1; 𝐢 𝐟 x \leq 4 𝐭 𝐡 𝐞 𝐧 𝐟 𝐚 𝐢 𝐥 𝐞 𝐥 𝐬 𝐞 z : = x 𝐞 𝐥 𝐬 𝐞 𝐬 𝐤 𝐢 𝐩$

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 ⟶ s^{'} e, s ⟶ 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 ⟶ n_{1} e_{2}, s ⟶ n_{2} I_{2}, s ⟶ s^{'}}{𝐟 𝐨 𝐫 x = e_{1} 𝐭 𝐨 e_{2} 𝐭 𝐫 𝐲 I_{1} 𝐞 𝐥 𝐬 𝐞 I_{2}, s ⟶ s^{'}} 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 $𝐟 𝐚 𝐢 𝐥$ . Oto reguła dla tego przypadku:

$\frac{e_{1}, s ⟶ n_{1} e_{2}, s ⟶ n_{2} I_{1}, s [x \mapsto n_{1}] ⟶ s^{'}}{𝐟 𝐨 𝐫 x = e_{1} 𝐭 𝐨 e_{2} 𝐭 𝐫 𝐲 I_{1} 𝐞 𝐥 𝐬 𝐞 I_{2}, s ⟶ s^{'} [x \mapsto s (x)]} o ile n_{1} \leq n_{2} .$

Tym razem uruchamiamy instrukcję $I_{1}$ , podstawiając pod 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 $𝐟 𝐚 𝐢 𝐥$ gdzieś wewnątrz $I_{1}$ . Aby poprawnie opisać takie zdarzenie, potrzebujemy dodatkowych tranzycji postaci:

$I, s ⟶ było- 𝐟 𝐚 𝐢 𝐥 .$

Mówiąc formalnie, poszerzamy zbiór konfiguracji o jeden element $było- 𝐟 𝐚 𝐢 𝐥$ . Zauważmy, że po prawej stronie tranzycji $d k r o k$ nie ma wogóle stanu. Nie potrzebujemy go dla opisania semantyki instrukcji $𝐟 𝐨 𝐫$ : jeśli wystąpi $𝐟 𝐚 𝐢 𝐥$ , 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}] ⟶ było- 𝐟 𝐚 𝐢 𝐥 .$

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 $𝐟 𝐨 𝐫$ . 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 $𝐟 𝐨 𝐫 x = e_{1} + 1 𝐭 𝐨 e_{2} 𝐭 𝐫 𝐲 I_{1} 𝐞 𝐥 𝐬 𝐞 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 $𝐟 𝐨 𝐫$ zakończyla 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), to 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 $𝐟 𝐨 𝐫 x = e_{1} + 1 𝐭 𝐨 e_{2} 𝐭 𝐫 𝐲 I_{1} 𝐞 𝐥 𝐬 𝐞 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).

Na zakończenie prezentujemy reguły niebędne do tego, aby wygenerować $było- 𝐟 𝐚 𝐢 𝐥$ :

$𝐟 𝐚 𝐢 𝐥, s ⟶ było- 𝐟 𝐚 𝐢 𝐥$

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:

$\frac{I_{1}, s ⟶ s^{'}, było- 𝐟 𝐚 𝐢 𝐥}{I_{1}; I_{2}, s ⟶ s^{'}, było- 𝐟 𝐚 𝐢 𝐥} \frac{I_{1}, s ⟶ s^{'} I_{2}, s^{'} ⟶ s^{″}, było- 𝐟 𝐚 𝐢 𝐥}{I_{1}; I_{2}, s ⟶ s^{″}, było- 𝐟 𝐚 𝐢 𝐥}$

$\frac{b, s ⟶ 𝐭 𝐫 𝐮 𝐞 I_{1}, s ⟶ s^{'}, było- 𝐟 𝐚 𝐢 𝐥}{𝐢 𝐟 b 𝐭 𝐡 𝐞 𝐧 I_{1} 𝐞 𝐥 𝐬 𝐞 I_{2}, s ⟶ s^{'}, było- 𝐟 𝐚 𝐢 𝐥} i analogicznie gdy b, s ⟶ 𝐭 𝐫 𝐮 𝐞$

$\frac{b, s ⟶ 𝐭 𝐫 𝐮 𝐞 I, s ⟶ s^{'}, było- 𝐟 𝐚 𝐢 𝐥}{𝐰 𝐡 𝐢 𝐥 𝐞 b 𝐝 𝐨 I, s ⟶ s^{'}, było- 𝐟 𝐚 𝐢 𝐥} \frac{b, s ⟶ 𝐭 𝐫 𝐮 𝐞 I, s ⟶ s^{'} 𝐰 𝐡 𝐢 𝐥 𝐞 b 𝐝 𝐨 I, s^{'} ⟶ s^{″}, było- 𝐟 𝐚 𝐢 𝐥}{𝐰 𝐡 𝐢 𝐥 𝐞 b 𝐝 𝐨 I, s ⟶ s^{'}, było- 𝐟 𝐚 𝐢 𝐥}$

Widać podobieństwo do analogicznych reguł dla pętli $𝐥 𝐨 𝐨 𝐩 I$ , 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 $było- 𝐟 𝐚 𝐢 𝐥$ . 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:

$I : : = \dots | 𝐛 𝐞 𝐠 𝐢 𝐧 𝐯 𝐚 𝐫 x = e; I 𝐞 𝐧 𝐝$

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 1 (tylko stan)

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

$𝐒 𝐭 𝐚 𝐭 𝐞 = 𝐕 𝐚 𝐫 \to_{f i n} 𝐍 𝐮 𝐦$ .

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

$\frac{e, s ⟶ n I, s [x \mapsto n] ⟶ s^{'}}{𝐛 𝐞 𝐠 𝐢 𝐧 𝐯 𝐚 𝐫 x = e; I 𝐞 𝐧 𝐝, s ⟶ s^{'}}$

mówiącą, że instrukcja wewnętrzna $I$ ewaluowana jest w stanie, w którym dodatkow 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 ⟶ n I, s [x \mapsto n] ⟶ s^{'}}{𝐛 𝐞 𝐠 𝐢 𝐧 𝐯 𝐚 𝐫 x = e; I 𝐞 𝐧 𝐝, s ⟶ s^{″}} o ile s^{″} = s^{'} [x \mapsto s (x)]$

I znów napotykamy podobnie 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.

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:

$𝐄 𝐧 𝐯 = 𝐕 𝐚 𝐫 \to_{f i n} 𝐋 𝐨 𝐜$

oraz stany, będące teraz funkcjami częściowymi z $𝐋 𝐨 𝐜$ do $𝐍 𝐮 𝐦$ :

$𝐒 𝐭 𝐚 𝐭 𝐞 = 𝐋 𝐨 𝐜 \to_{f i n} 𝐍 𝐮 𝐦 .$

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 $𝐋 𝐨 𝐜 = {l_{0}, l_{1}, \dots}$ 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ń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 $E$ będzie zawsze zawarty w zbiorze aktualnie używanych lokacji, czyli zawarty w dziedzinie funkcji częściowej $s$ , 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:

$I, s, E ⟶ 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 ⊢ I, s ⟶ 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 pary $(E, s)$ .

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ę funkcję

$n e w : 𝐒 𝐭 𝐚 𝐭 𝐞 \to 𝐋 𝐨 𝐜$

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.

$\frac{E ⊢ e, s ⟶ n E [x \mapsto l] ⊢ I, s [l \mapsto n] ⟶ s^{'}}{E ⊢ 𝐛 𝐞 𝐠 𝐢 𝐧 𝐯 𝐚 𝐫 x = e; I 𝐞 𝐧 𝐝, s ⟶ s^{'}} gdzie l = n e w (s)$

Zauważmy, że stan $s^{'}$ po zakończeniu instrukcji $𝐛 𝐞 𝐠 𝐢 𝐧 𝐯 𝐚 𝐫 x = e; I 𝐞 𝐧 𝐝$ 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 ⊢ I_{1}, s ⟶ s^{'} E, ⊢ I_{2}, s^{'} ⟶ s^{″}}{E ⊢ I_{1}; I_{2}, s ⟶ 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ę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ń:

$E ⊢ e, s ⟶ 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 ⊢ e, s ⟶ n}{E ⊢ x : = e, s ⟶ s [x \mapsto n]} E ⊢ 𝐬 𝐤 𝐢 𝐩, s ⟶ s$

$\frac{E ⊢ b, s ⟶ 𝐭 𝐫 𝐮 𝐞 E ⊢ I_{1}, s ⟶ s^{'}}{E ⊢ 𝐢 𝐟 b 𝐭 𝐡 𝐞 𝐧 I_{1} 𝐞 𝐥 𝐬 𝐞 I_{2}, s ⟶ s^{'}} \frac{E ⊢ b, s ⟶ 𝐭 𝐫 𝐮 𝐞 E ⊢ I_{2}, s ⟶ s^{'}}{E ⊢ 𝐢 𝐟 b 𝐭 𝐡 𝐞 𝐧 I_{1} 𝐞 𝐥 𝐬 𝐞 I_{2}, s ⟶ s^{'}}$

$E ⊢ 𝐢 𝐟 b 𝐭 𝐡 𝐞 𝐧 (𝐰 𝐡 𝐢 𝐥 𝐞 b 𝐝 𝐨 I) 𝐞 𝐥 𝐬 𝐞 𝐬 𝐤 𝐢 𝐩, s ⟶ s^{'} E ⊢ 𝐰 𝐡 𝐢 𝐥 𝐞 b 𝐝 𝐨 I, s ⟶ s^{'}$

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

$E ⊢ n, s ⟶ n E ⊢ x, s ⟶ n o ile E (x) = l \in 𝐋 𝐨 𝐜 i s (l) = n$

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

Wariant (dealokacja)

Przypomnijmy sobie semantykę bloku

$\frac{E ⊢ e, s ⟶ n E [x \mapsto l] ⊢ I, s [l \mapsto n] ⟶ s^{'}}{E ⊢ 𝐛 𝐞 𝐠 𝐢 𝐧 𝐯 𝐚 𝐫 x = e; I 𝐞 𝐧 𝐝, s ⟶ s^{'}} gdzie l = n e w (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ż potrzebne. 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 ⊢ d, s ⟶ (E^{'}, s^{'}) E^{'} ⊢ I, s^{'} ⟶ s^{″}}{E ⊢ 𝐛 𝐞 𝐠 𝐢 𝐧 d; I 𝐞 𝐧 𝐝, s ⟶ \bar{s}}$

gdzie $\bar{s}$ to stan $s^{″}$ ,,okrojony" do dziedziny stanu $s$ . Zatem 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 ⊢ e, s ⟶ n E [x \mapsto l] ⊢ I, s [l \mapsto n] ⟶ s^{'}}{E ⊢ 𝐛 𝐞 𝐠 𝐢 𝐧 𝐯 𝐚 𝐫 x = e; I 𝐞 𝐧 𝐝, s ⟶ s^{'} ∖ {(l, s^{'} (l))}} gdzie l = n e w (s)$

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 }

$e x c : : = x | 𝐚 𝐧 𝐲$

Instrukcja $𝐭 𝐡 𝐫 𝐨 𝐰 x$ oznacza podniesienie wyjątku o nazwie $x$ . Instrukcja $I = 𝐭 𝐫 𝐲 I_{1} 𝐜 𝐚 𝐭 𝐜 𝐡 e x c I_{2}$ wykonuje $I_{1}$ . Jeśli podczas wykonania $I_{1}$ zostanie podniesiony wyjątej $x$ , i $e x c = x$ albo $e x c = 𝐚 𝐧 𝐲$ , 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ątej $x$ , i $e x c \neq x$ i $e x c \neq 𝐚 𝐧 𝐲$ , to obsługa wyjątku przekazana jest do najbliższej instrukcji $𝐭 𝐫 𝐲$ otaczającej $I$ . Umawiamy się, że $𝐭 𝐫 𝐲 I_{1} 𝐜 𝐚 𝐭 𝐜 𝐡 e x c I_{2}$ otacza $I_{1}$ i wszystkie instrukcje wewnątrz $I_{1}$ , ale nie otacza $I_{2}$ .

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.

Semantyka i weryfikacja programów/Ćwiczenia 5: Różnice pomiędzy wersjami

Wersja z 08:51, 7 sie 2006

Spis treści

Zawartość

Zadania z rozwiązaniami

Zadanie 1

Przykład

Rozwiązanie

Zadanie 2 (bloki i deklaracje zmiennych)

Rozwiązanie 1 (tylko stan)

Rozwiązanie 2 (stan i środowisko)

Wariant (dealokacja)

Zadania domowe

Zadanie 1

Zadanie 2

Menu nawigacyjne

Działania na stronie

Opcje strony

Narzędzia osobiste

Nawigacja

Szukaj

Narzędzia

@@ Linia 1: / Linia 1: @@
+== 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:
+<math>
+I \, ::= \,\,
+          \ldots \,\,|\,\,
+          \mathbf{for}\, x = e_1 \,\mathbf{to}\, e_2 \,\mathbf{try}\, I_1 \,\mathbf{else}\, I_2 \,\,|\,\,
+          \mathbf{fail}
+</math>
+Znaczenie instrukcji <math> \mathbf{for}\, x = e_1 \,\mathbf{to}\, e_2 \,\mathbf{try}\, I_1 \,\mathbf{else}\, I_2 </math>
+jest następujące.
+Obliczamy wartości wyrażeń <math> e_1 </math> i <math> e_2 </math>. Jeśli pierwsza
+z nich jest mniejsza lub równa od drugiej, to podstawiamy pierwszą
+wartość (wartość wyrażenia <math> e_1 </math>) na zmienną <math> x </math> i uruchamiamy <math> I_1 </math>.
+Jeśli w <math> I_1 </math> nie zostanie napotkana instrukcja <math> \mathbf{fail} </math>,
+kończymy instrukcję <math> \mathbf{for}\, </math> i przyracamy wartość zmiennej <math> x </math>
+sprzed tej instrukcji.
+Natomiast jeśli w <math> I_1 </math> zostanie napotkana instrukcja <math> \mathbf{fail} </math>,
+podstawiamy na <math> x </math> kolejną, o jeden większą wartość,
+przywracamy wartości wszystkich
+pozostałych zmiennych sprzed instrukcji <math> \mathbf{for}\, </math>, i ponownie
+wykonujemy <math> I_1 </math>.
+Powtarzamy w ten sposób aż <math> I_1 </math> zakończy się nie napotkawszy <math> \mathbf{fail} </math>,
+albo wartość zmiennej <math> x </math> przekroczy wartość wyrażenia <math> e_2 </math>
+obliczoną na początku.
+W pierwszym przypadku
+kończymy instrukcję <math> \mathbf{for}\, </math> i przyracamy wartość zmiennej <math> x </math>
+sprzed tej instrukcji.
+W drugim przywracamy wartości wszystkich zmiennych sprzed instrukcji
+<math> \mathbf{for}\, </math> i uruchamiamy <math> I_2 </math>.
+===== Przykład =====
+<math>
+x := 0; y := 1;
+\mathbf{for}\, x := 1 \,\mathbf{to}\, 5 \,\mathbf{try}\,
+\quad y := y+1;
+\quad \mathbf{if}\, x \leq 4 \,\mathbf{then}\, \mathbf{fail} \,\mathbf{else}\, z:= x
+\,\mathbf{else}\, \mathbf{skip}
+</math>
+Wartości zmiennych po zakończeniu programu to:
+<math> x = 0, y = 2, z = 5 </math>.
+==== Rozwiązanie ====
+Będziemy posługiwać się jak zwykle tranzycjami postaci:
+<math>
+I, s \,\longrightarrow\, s' \quad \quad \quad e, s \,\longrightarrow\, n.
+</math>
+Zacznijmy od najprostszego przypadku, gdy nie ma wogóle potrzeby
+uruchamiania instrukcji wewnętrznej <math> I_1 </math>, ponieważ
+wartość wyrażenia <math> e_1 </math> jest większa od <math> e_2 </math>:
+<math>
+\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.
+</math>
+Po prostu uruchamiamy instrukcję <math> I_2 </math> w stanie <math> s </math>, ignorując
+<math> I_1 </math>.
+Kolejny nietrudny przypadek to sytuacja, w której
+<math> n_1 \leq n_2 </math> a wykonanie instrukcji wewnętrznej <math> I_1 </math>
+kończy się sukcesem, tzn. nie następuje wywołanie instrukcji
+<math> \mathbf{fail} </math>. Oto reguła dla tego przypadku:
+<math>
+\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.
+</math>
+Tym razem uruchamiamy instrukcję <math> I_1 </math>, podstawiając
+pod zmienną <math> x </math> wartość <math> n_1 </math>.
+Zwróćmy uwagę, że po zakończeniu <math> I_1 </math> przywracamy
+wartość zmiennej <math> x </math> sprzed jej wykonania.
+Pozostał nam trzeci przypadek, gdy <math> n_1 \leq n_2 </math>
+a wykonanie instrukcji <math> I_1 </math> zakończyło się
+wykonaniem instrukcji <math> \mathbf{fail} </math> gdzieś wewnątrz <math> I_1 </math>.
+Aby poprawnie opisać takie zdarzenie, potrzebujemy dodatkowych
+tranzycji postaci:
+<math>
+I, s \,\longrightarrow\, \mbox{było-}\mathbf{fail}.
+</math>
+Mówiąc formalnie, poszerzamy zbiór konfiguracji o jeden element
+<math> \mbox{było-}\mathbf{fail} </math>.
+Zauważmy, że po prawej stronie tranzycji <math> dkrok </math> nie ma wogóle
+stanu.
+Nie potrzebujemy go dla opisania semantyki instrukcji <math> \mathbf{for}\, </math>:
+jeśli wystąpi <math> \mathbf{fail} </math>, powtarzamy <math> I_1 </math> dla większej o <math> 1 </math> wartości
+zmiennej <math> x </math>, ale pozostałym zmiennym przywracamy wartość ''sprzed''
+<math> I_1 </math>.
+A więc załóżmy, że
+<math> I_1, s[x \mapsto n_1] \,\longrightarrow\, \mbox{było-}\mathbf{fail}. </math>
+W takiej sytuacji powinniśmy przypisać <math> n_1 + 1 </math>
+na zmienną <math> x </math> i spróbować ponownie wykonać
+<math> I_1 </math> przy wartościach wszystkich pozostałych
+zmiennych takich, jak na początku instrukcji <math> \mathbf{for}\, </math>.
+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:
+<math>
+\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.
+</math>
+Zwróćmy uwagę na pewnien niezwykle istotny szczegół: po zakończeniu
+wykonania instrukcji <math> \mathbf{for}\, x = e_1 + 1 \,\mathbf{to}\, e_2 \,\mathbf{try}\, I_1 \,\mathbf{else}\, I_2 </math>
+otrzymujemy stan <math> s' </math>, w którym '''nie przywracamy''' wartości
+zmiennej <math> x </math>. Gdybyśmy tak zrobili, tzn. gdybyśmy zastąpili <math> s'
+</math> przez <math> s'[x \mapsto s(x)] </math>, nasze semantyka byłaby
+niepoprawna. Dlaczego? Dlatego, że nie wiemy tak naprawdę,
+czy powinniśmy przywracać wartość zmiennej <math> x </math> czy nie.
+Jeśli ostatecznie nasza instrukcja <math> \mathbf{for}\, </math> zakończyla
+się przez bezbłędne zakończenie instrukcji <math> I_1 </math>
+(przypadek drugi), to powinniśmy to zrobić;
+ale jeśli zakończyła się wykonaniem instrukcji <math> I_2 </math>
+(przypadek pierwszy),
+to powinniśmy pozostawić wartość zmiennej <math> x </math> taką,
+jaka jest ona po zakończeniu <math> I_2 </math>.
+A zatem w powyższej regule dla przypadku trzeciego
+nie przywracamy wartości zmiennej <math> x </math>; 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 <math> \mathbf{for}\, x = e_1 + 1 \,\mathbf{to}\, e_2 \,\mathbf{try}\, I_1 \,\mathbf{else}\, I_2 </math>
+wykonywana jest w orginalnym stanie <math> s </math>,
+a nie w stanie, w którym kończy się <math> I_1 </math>
+(tego ostatniego stanu nawet nie znamy).
+Na zakończenie prezentujemy reguły niebędne do tego,
+aby wygenerować <math> \mbox{było-}\mathbf{fail} </math>:
+<math>
+\mathbf{fail}, s \,\longrightarrow\, \mbox{było-}\mathbf{fail}
+</math>
+oraz aby wystąpienie <math> \mathbf{fail} </math> umiejscowione gdzieś ,,głęboko"
+zostało rozpropagowane do najbliższej otaczającej
+instrukcji <math> \mathbf{for}\, </math>.
+Jeśli pojawił się <math> \mathbf{fail} </math>, powinniśmy zaniechać dalszego
+wykonania instrukcji a w przypadku pętli, powinniśmy
+zaniechać dalszego iterowania tej pętli.
+Oto odpowiednie reguły:
+<math>
+\frac{I_1, s \,\longrightarrow\, s', \mbox{było-}\mathbf{fail}}
+     {I_1;\, I_2, s \,\longrightarrow\, s', \mbox{było-}\mathbf{fail}}
+\quad \quad
+\frac{I_1, s \,\longrightarrow\, s' \quad \quad I_2, s' \,\longrightarrow\, s'', \mbox{było-}\mathbf{fail}}
+     {I_1;\, I_2, s \,\longrightarrow\, s'', \mbox{było-}\mathbf{fail}}
+</math>
+<math>
+\frac{b, s \,\longrightarrow\, \mathbf{true} \quad \quad I_1, s \,\longrightarrow\, s', \mbox{było-}\mathbf{fail}}
+     {\mathbf{if}\, b \,\mathbf{then}\, I_1 \,\mathbf{else}\, I_2, s \,\longrightarrow\, s', \mbox{było-}\mathbf{fail}}
+\quad \quad
+\mbox{ i analogicznie gdy } b, s \,\longrightarrow\, \mathbf{true}
+</math>
+<math>
+\frac{b, s \,\longrightarrow\, \mathbf{true} \quad \quad I, s \,\longrightarrow\, s', \mbox{było-}\mathbf{fail}}
+     {\mathbf{while}\, b \,\mathbf{do}\, I, s \,\longrightarrow\, s', \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\, s'', \mbox{było-}\mathbf{fail}}
+     {\mathbf{while}\, b \,\mathbf{do}\, I, s \,\longrightarrow\, s', \mbox{było-}\mathbf{fail}}
+</math>
+Widać podobieństwo do analogicznych reguł dla
+pętli <math> \mathbf{loop}\, I </math>, którą zajmowaliśmy się na wcześniejszych
+zajęciach.
+Zauważmy, że jesli <math> \mathbf{fail} </math> zostało wykonane poza jakąkolwiek
+pętlą <math> \mathbf{for}\, </math>, to program ,,zakończy się" w konfiguracji
+<math> \mbox{było-}\mathbf{fail} </math>. 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:
+<math>
+I \, ::= \,\,
+      \ldots  \,\,|\,\,
+     \mathbf{begin}\, \mathbf{var}\, x = e;\, I \,\mathbf{end}
+</math>
+Zasięgiem zmiennej <math> x </math>  jest instrukcja <math> I </math>
+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
+<math> \mathbf{State} = \mathbf{Var} \to_{\mathrm{fin}} \mathbf{Num} </math>.
+Zachowuujemy wszystkie reguły semantyczne dla języka Tiny
+i dodajemy jedną nową:
+<math>
+\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'}
+</math>
+mówiącą, że instrukcja wewnętrzna <math> I </math> ewaluowana jest
+w stanie, w którym dodatkow zaznaczono wartość zmiennej <math> x </math>
+równą wartości, do której oblicza się <math> e </math>.
+Oczywiście takie rozwiązanie jest niepoprawne, gdyż wartość
+zmiennej <math> x </math>  pozostaje w stanie nawet po wyjściu z bloku
+(,,wycieka" z bloku).
+Musimy dodać ,,dealokację" zmiennej <math> x </math>:
+<math>
+\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)]
+</math>
+I znów napotykamy podobnie trudności jak na wcześniejszych zajęciach:
+powyższa reguła nie obejmuje przypadku, gdy <math> s(x) </math> 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'' <math> E \in \mathbf{Env}], będące funkcjami częściowymi z <math> \mathbf{Var} </math>
+do <math> \mathbf{Loc} </math>, zbioru lokacji:
+<math>
+\mathbf{Env} = \mathbf{Var} \to_{\mathrm{fin}} \mathbf{Loc}
+</math>
+oraz stany, będące teraz funkcjami częściowymi z <math> \mathbf{Loc} </math> do <math> \mathbf{Num} </math>:
+<math>
+\mathbf{State} = \mathbf{Loc} \to_{\mathrm{fin}} \mathbf{Num}.
+</math>
+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 <math> \mathbf{Loc} = \{ l_0, l_1, \ldots \} </math> i że
+w każdym momencie tylko skończenie wiele spośród nich jest
+wykorzystywane.
+Formalnie mowiąc, dziedzina funkcji częściowej <math> s </math> 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 <math> E </math>
+będzie zawsze zawarty w zbiorze aktualnie używanych lokacji,
+czyli zawarty w dziedzinie funkcji częściowej <math> s </math>, oznaczanej
+<math> \dom(s) </math>.
+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:
+<math>
+I, s, E \,\longrightarrow\, s'
+</math>
+czyli instrukcja <math> I </math> będzie modyfikować stan ale nie będzie
+zmieniać środowiska <math> E </math>. Dla czytelności będziemy zapisywać
+nasze reguły w następujący sposób:
+<math>
+E \,\vdash\, I, s \,\longrightarrow\, s'
+</math>
+podkreślając w ten sposób, że środowisko nie ulega zmianie.
+Ale należy pamiętać, że konfiguracja, w której ,,uruchamiamy"
+instrukcję <math> I </math> składa się naprawdę z pary <math> (E, s) </math>.
+Deklarując nową zmienną <math> x </math> dodamy po prostu do <math> E </math> parę
+<math> (x, l) </math>, gdzie <math> l </math> jest nową, nieużywaną dotychczas lokacją.
+Dla wygody zapisu załóżmy, że mamy do dyspozycji funkcję
+funkcję
+<math>
+\mathtt{new} : \mathbf{State} \to \mathbf{Loc}
+</math>
+która zwraca jakąś nową, nieużywaną lokację. Formalnie wymagamy, by
+<math>
+\mathtt{new}(s) \notin \dom(s).
+</math>
+Dla ilustracji popatrzmy na przykładową regułę dla deklaracji.
+<math>
+\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{new}(s)
+</math>
+Zauważmy, że stan <math> s' </math> po zakończeniu instrukcji
+<math> \mathbf{begin}\, \mathbf{var}\, x=e;\, I \,\mathbf{end} </math> zawiera informację o zmiennej
+lokalnej <math> x </math>, tzn. <math> s(l) </math> jest określone.
+Ale lokacja <math> l </math> jest ,,nieosiągalna" w środowisku
+<math> E </math>, gdyż para <math> x \mapsto l </math> została dodana tylko do
+środowiska, w którym ewaluuje się wnętrze bloku, a środowisko
+<math> E </math> całego bloku nie jest modyfikowane.
+Poniżej przedstawiamy reguły dla pozostałych instrukcji.
+Przede wszystkim złożenie sekwencyjne:
+<math>
+\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''}
+</math>
+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ń:
+<math>
+E \,\vdash\, e, s \,\longrightarrow\, n
+</math>
+która jest zupełnie naturalna w naszym podejściu opartym o środowiska
+i stany.
+Reguły mogą wyglądać np. tak:
+<math>
+\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
+</math>
+<math>
+\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{true}
+      \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'}
+</math>
+<math>
+{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'}
+</math>
+Reguły dla wyrażeń są oczywiste:
+<math>
+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
+</math>
+i tak dalej -- pomijamy pozostałe reguły.
+===== Wariant (dealokacja) =====
+Przypomnijmy sobie semantykę bloku
+<math>
+\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{new}(s)
+</math>
+i zastanówmy się, jak ,,posprzątać" po zakończeniu wykonania bloku,
+tzn. zwolnić lokację <math> l </math>, 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 <math> l </math> do puli wolnych
+(nieużywanych) lokacji.
+Zmodyfikowana reguła dla instrukcji bloku powinna wyglądać mniej więcej tak:
+<math>
+\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}}
+</math>
+gdzie <math> \bar{s} </math> to stan <math> s'' </math> ,,okrojony" do dziedziny stanu <math> s </math>.
+Zatem powinniśmy po prostu przywrócić nieokreśloność stanu dla lokacji
+<math> l </math>.
+Natomiast oczywiście nie ma potrzeby dealokownia środowiska!
+Oto rozwiązanie:
+<math>
+\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{new}(s)
+</math>
+== Zadania domowe ==
+==== Zadanie 1 ====
+Napisz semantykę naturalną dla następującego
+rozszerzenia języka Tiny:
+<math>
+I \, ::= \,\,
+      \ldotes \,\,|\,\,
+       \mathbf{throw}\, x \,\,|\,\,
+       \,\mathbf{try}\, I_1 \,\mathbf{catch}\, exc\, I_2
+</math>
+<math>
+exc \, ::= \,\,
+       x \,\,|\,\,
+       \mathbf{any}
+</math>
+Instrukcja <math> \mathbf{throw}\, x </math> oznacza podniesienie wyjątku o nazwie <math> x </math>.
+Instrukcja <math> I = \,\mathbf{try}\, I_1 \,\mathbf{catch}\, exc\, I_2 </math> wykonuje <math> I_1 </math>.
+Jeśli podczas wykonania <math> I_1 </math> zostanie podniesiony wyjątej <math> x
+</math>, i <math> exc = x </math> albo <math> exc = \mathbf{any} </math>, to następuje przerwanie <math>
+I_1 </math> i sterowanie zostaje przeniesione do <math> I_2 </math>
+(następuje ''obsługa wyjątku'').
+Jeśli zaś podczas wykonania <math> I_1 </math> zostanie podniesiony wyjątej <math> x
+</math>, i <math> exc \neq x </math> i <math> exc \neq \mathbf{any} </math>, to obsługa wyjątku
+przekazana jest do najbliższej instrukcji <math> \,\mathbf{try}\, </math> otaczającej <math> I
+</math>.
+Umawiamy się, że <math> \,\mathbf{try}\, I_1 \,\mathbf{catch}\, exc\, I_2 </math> ''otacza'' <math> I_1 </math>
+i wszystkie instrukcje wewnątrz <math> I_1 </math>,
+ale ''nie'' otacza <math> I_2 </math>.
+==== 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.