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

Wersja z 08:34, 8 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

Ćwiczenie 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

{{{3}}}

Rozwiązanie

{{{3}}}

Ćwiczenie 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

{{{3}}}

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$ oraz $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, w której deklaracja jest wykonywana ,,równolegle", analogicznie do przypisania równoległego. Przy takiej semantyce kolejność poszczególnych deklaracji powinna być nieistotna.

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

Wersja z 08:34, 8 sie 2006

Spis treści

Zawartość

Zadania z rozwiązaniami

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ść ==
@@ Linia 14: / Linia 15: @@
-==== Zadanie 1 ====
+{{cwiczenie|1|cw1|
@@ Linia 26: / Linia 27: @@
 </math>
-Znaczenie instrukcji <math> \mathbf{for}\, x = e_1 \,\mathbf{to}\, e_2 \,\mathbf{try}\, I_1 \,\mathbf{else}\, I_2 </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
+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>.
+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>,
+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>
+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>,
+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ść,
+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
+pozostałych zmiennych sprzed instrukcji <math>\mathbf{for}\,</math>, i ponownie
-wykonujemy <math> I_1 </math>.
+wykonujemy <math>I_1</math>.
-Powtarzamy w ten sposób aż <math> I_1 </math> zakończy się nie napotkawszy <math> \mathbf{fail} </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>
+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>
+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>.
+<math>\mathbf{for}\,</math> i uruchamiamy <math>I_2</math>.
+}}
-===== Przykład =====
+{{przyklad|||
+ x := 0; y := 1;
+ <math>\mathbf{for}\,</math> x := 1 \,\mathbf{to}\, 5 <math>\,\mathbf{try}\,</math>
+   y := y+1;
+   <math>\mathbf{if}\,</math> x \leq 4 <math>\,\mathbf{then}\, \mathbf{fail} \,\mathbf{else}\,</math> z:= x
+ <math>\,\mathbf{else}\, \mathbf{skip}</math>
-<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:
+Wartości zmiennych po zakończeniu programu to: <math>x = 0, y = 2, z = 5</math>.
-<math> x = 0, y = 2, z = 5 </math>.
+}}
-==== Rozwiązanie ====
+{{rozwiazanie||roz1|
+<div class="mw-collapsible mw-made=collapsible mw-collapsed"><div class="mw-collapsible-content" style="display:none">
 Będziemy posługiwać się jak zwykle tranzycjami postaci:
@@ Linia 73: / Linia 76: @@
 Zacznijmy od najprostszego przypadku, gdy nie ma wogóle potrzeby
-uruchamiania instrukcji wewnętrznej <math> I_1 </math>, ponieważ
+uruchamiania instrukcji wewnętrznej <math>I_1</math>, ponieważ
-wartość wyrażenia <math> e_1 </math> jest większa od <math> e_2 </math>:
+wartość wyrażenia <math>e_1</math> jest większa od <math>e_2</math>:
 <math>
@@ Linia 86: / Linia 89: @@
 </math>
-Po prostu uruchamiamy instrukcję <math> I_2 </math> w stanie <math> s </math>, ignorując
+Po prostu uruchamiamy instrukcję <math>I_2</math> w stanie <math>s</math>, ignorując
-<math> I_1 </math>.
+<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>
+<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>\mathbf{fail}</math>. Oto reguła dla tego przypadku:
 <math>
@@ Linia 104: / Linia 107: @@
 </math>
-Tym razem uruchamiamy instrukcję <math> I_1 </math>, podstawiając
+Tym razem uruchamiamy instrukcję <math>I_1</math>, podstawiając
-pod zmienną <math> x </math> wartość <math> n_1 </math>.
+pod zmienną <math>x</math> wartość <math>n_1</math>.
-Zwróćmy uwagę, że po zakończeniu <math> I_1 </math> przywracamy
+Zwróćmy uwagę, że po zakończeniu <math>I_1</math> przywracamy
-wartość zmiennej <math> x </math> sprzed jej wykonania.
+wartość zmiennej <math>x</math> sprzed jej wykonania.
-Pozostał nam trzeci przypadek, gdy <math> n_1 \leq n_2 </math>
+Pozostał nam trzeci przypadek, gdy <math>n_1 \leq n_2</math>
-a wykonanie instrukcji <math> I_1 </math> zakończyło się
+a wykonanie instrukcji <math>I_1</math> zakończyło się
-wykonaniem instrukcji <math> \mathbf{fail} </math> gdzieś wewnątrz <math> I_1 </math>.
+wykonaniem instrukcji <math>\mathbf{fail}</math> gdzieś wewnątrz <math>I_1</math>.
 Aby poprawnie opisać takie zdarzenie, potrzebujemy dodatkowych
 tranzycji postaci:
@@ Linia 120: / Linia 123: @@
 Mówiąc formalnie, poszerzamy zbiór konfiguracji o jeden element
-<math> \mbox{było-}\mathbf{fail} </math>.
+<math>\mbox{było-}\mathbf{fail}</math>.
-Zauważmy, że po prawej stronie tranzycji <math> dkrok </math> nie ma wogóle
+Zauważmy, że po prawej stronie tranzycji nie ma wogóle stanu.
-stanu.
+Nie potrzebujemy go dla opisania semantyki instrukcji <math>\mathbf{for}\,</math>:
-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
-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''
-zmiennej <math> x </math>, ale pozostałym zmiennym przywracamy wartość ''sprzed''
+<math>I_1</math>.
-<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>
+<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>
+W takiej sytuacji powinniśmy przypisać <math>n_1 + 1</math>
-na zmienną <math> x </math> i spróbować ponownie wykonać
+na zmienną <math>x</math> i spróbować ponownie wykonać
-<math> I_1 </math> przy wartościach wszystkich pozostałych
+<math>I_1</math> przy wartościach wszystkich pozostałych
-zmiennych takich, jak na początku instrukcji <math> \mathbf{for}\, </math>.
+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.
@@ Linia 141: / Linia 143: @@
 <math>
 \frac{e_1, s \,\longrightarrow\, n_1
-       \quad \quad
+       \quad
        e_2, s \,\longrightarrow\, n_2
-       \quad \quad
+       \quad
        I_1, s[x \mapsto n_1]  \,\longrightarrow\, \mbox{było-}\mathbf{fail}
-       \quad \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 + 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.
@@ Linia 152: / Linia 154: @@
 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>
+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
+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'
+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
+</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.
+czy powinniśmy przywracać wartość zmiennej <math>x</math> czy nie.
-Jeśli ostatecznie nasza instrukcja <math> \mathbf{for}\, </math> zakończyla
+Jeśli ostatecznie nasza instrukcja <math>\mathbf{for}\,</math> zakończyla
-się przez bezbłędne zakończenie instrukcji <math> I_1 </math>
+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>
+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ą,
+to powinniśmy pozostawić wartość zmiennej <math>x</math> taką,
-jaka jest ona po zakończeniu <math> I_2 </math>.
+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
+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>
+ż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>,
+wykonywana jest w orginalnym stanie <math>s</math>,
-a nie w stanie, w którym kończy się <math> I_1 </math>
+a nie w stanie, w którym kończy się <math>I_1</math>
 (tego ostatniego stanu nawet nie znamy).
+Jeszcze jeden drobiazg: zamiast <math>e_1 {+} 1</math> w
+<math>\mathbf{for}\, x = e_1 + 1 \,\mathbf{to}\, e_2 \,\mathbf{try}\, I_1 \,\mathbf{else}\, I_2, s \,\longrightarrow\, s'</math>
+w regule powyżej, moglibyśmy podstawić policzoną już
+wartość, czyli <math>n_1 {+} 1</math>.
 Na zakończenie prezentujemy reguły niebędne do tego,
-aby wygenerować <math> \mbox{było-}\mathbf{fail} </math>:
+aby wygenerować <math>\mbox{było-}\mathbf{fail}</math>:
 <math>
@@ Linia 181: / Linia 188: @@
 </math>
-oraz aby wystąpienie <math> \mathbf{fail} </math> umiejscowione gdzieś ,,głęboko"
+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>.
+instrukcji <math>\mathbf{for}\,</math>.
-Jeśli pojawił się <math> \mathbf{fail} </math>, powinniśmy zaniechać dalszego
+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.
@@ Linia 190: / Linia 197: @@
 <math>
-\frac{I_1, s \,\longrightarrow\, s', \mbox{było-}\mathbf{fail}}
+\frac{I_1, s \,\longrightarrow\, \mbox{było-}\mathbf{fail}}
-      {I_1;\, I_2, s \,\longrightarrow\, s', \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\, s'', \mbox{było-}\mathbf{fail}}
+\frac{I_1, s \,\longrightarrow\, s' \quad \quad I_2, s' \,\longrightarrow\, \mbox{było-}\mathbf{fail}}
-      {I_1;\, I_2, s \,\longrightarrow\, s'', \mbox{było-}\mathbf{fail}}
+      {I_1;\, I_2, s \,\longrightarrow\, \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}}
+\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\, s', \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{true}
+\mbox{ i analogicznie gdy } b, s \,\longrightarrow\, \mathbf{false}
 </math>
 <math>
-\frac{b, s \,\longrightarrow\, \mathbf{true} \quad \quad I, s \,\longrightarrow\, s', \mbox{było-}\mathbf{fail}}
+\frac{b, s \,\longrightarrow\, \mathbf{true} \quad \quad I, s \,\longrightarrow\, \mbox{było-}\mathbf{fail}}
-      {\mathbf{while}\, b \,\mathbf{do}\, I, s \,\longrightarrow\, s', \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\, s'', \mbox{było-}\mathbf{fail}}
+       \mathbf{while}\, b \,\mathbf{do}\, I, s' \,\longrightarrow\, \mbox{było-}\mathbf{fail}}
-      {\mathbf{while}\, b \,\mathbf{do}\, I, s \,\longrightarrow\, s', \mbox{było-}\mathbf{fail}}
+      {\mathbf{while}\, b \,\mathbf{do}\, I, s \,\longrightarrow\, \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
+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
+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
+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ę
+<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.
+</div></div>
+}}
-==== Zadanie 2 (bloki i deklaracje zmiennych) ====
+{{cwiczenie|2 (bloki i deklaracje zmiennych)|cw2|
 Rozszerz semantykę języka Tiny o deklarację zmiennej:
@@ Linia 234: / Linia 244: @@
 </math>
-Zasięgiem zmiennej <math> x </math>  jest instrukcja <math> I </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.
+}}
+{{rozwiazanie||roz2|
-==== Rozwiązanie 1 (tylko stan) ====
+<div class="mw-collapsible mw-made=collapsible mw-collapsed"><div class="mw-collapsible-content" style="display:none">
+'''Rozwiązanie 1 (tylko stan)'''
+<br>
 Oczywiście powinniśmy odróżniać zmienne zadeklarowane (i zarazem
@@ Linia 246: / Linia 261: @@
 Zatem przyjmijmy, że
-<math> \mathbf{State} = \mathbf{Var} \to_{\mathrm{fin}} \mathbf{Num} </math>.
+<math>\mathbf{State} = \mathbf{Var} \to_{\mathrm{fin}} \mathbf{Num}</math>.
-Zachowuujemy wszystkie reguły semantyczne dla języka Tiny
+Zachowujemy wszystkie reguły semantyczne dla języka Tiny
 i dodajemy jedną nową:
@@ Linia 256: / Linia 271: @@
 </math>
-mówiącą, że instrukcja wewnętrzna <math> I </math> ewaluowana jest
+mówiącą, że instrukcja wewnętrzna <math>I</math> ewaluowana jest
-w stanie, w którym dodatkow zaznaczono wartość zmiennej <math> x </math>
+w stanie, w którym dodatkowo zaznaczono wartość zmiennej <math>x</math>
-równą wartości, do której oblicza się <math> e </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
+zmiennej <math>x</math>  pozostaje w stanie nawet po wyjściu z bloku
 (,,wycieka" z bloku).
-Musimy dodać ,,dealokację" zmiennej <math> x </math>:
+Musimy dodać ,,dealokację" zmiennej <math>x</math>:
 <math>
@@ Linia 271: / Linia 286: @@
 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
+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ś
@@ Linia 278: / Linia 293: @@
-==== Rozwiązanie 2 (stan i środowisko) ====
+<br>
+'''Rozwiązanie 2 (stan i środowisko)'''
+<br>
 Podstawowy pomysł polega na rozdzielenie informacji przechowywanej
@@ Linia 284: / Linia 301: @@
 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>
+Mamy więc ''środowiska'' <math>E \in \mathbf{Env}</math>, będące funkcjami częściowymi z <math>\mathbf{Var}</math>
-do <math> \mathbf{Loc} </math>, zbioru lokacji:
+do <math>\mathbf{Loc}</math>, zbioru lokacji:
 <math>
@@ Linia 291: / Linia 308: @@
 </math>
-oraz stany, będące teraz funkcjami częściowymi z <math> \mathbf{Loc} </math> do <math> \mathbf{Num} </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}.
+\mathbf{Store} = \mathbf{Loc} \to_{\mathrm{fin}} \mathbf{Num}.
 </math>
-Intuicyjnie można myśleć o lokacjach jak o lokacjach w pamięci
+Dla jednoznaczności używamy innej nazwy (<math>\mathbf{Store}</math>) ale będziemy
+zwykle używać symbolu <math>s, s', s_1, \ldots \in \mathbf{Store}</math> 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.
+przechowywana jest wartość danej zmiennej
-A stan opisuje właśnie zawartość używanych lokacji.
+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
+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.
+Formalnie mowiąc, dziedzina funkcji częściowej <math>s</math> 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 <math> E </math>
+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
+czyli zawarty w dziedzinie funkcji częściowej <math>s</math>, oznaczanej
-<math> \dom(s) </math>.
+<math>\mathrm{dom}(s)</math>.
 Pożytek z tego podziału na dwa etapy będzie taki, że
@@ Linia 325: / Linia 344: @@
 </math>
-czyli instrukcja <math> I </math> będzie modyfikować stan ale nie będzie
+czyli instrukcja <math>I</math> będzie modyfikować stan ale nie będzie
-zmieniać środowiska <math> E </math>. Dla czytelności będziemy zapisywać
+zmieniać środowiska <math>E</math>. Dla czytelności będziemy zapisywać
 nasze reguły w następujący sposób:
@@ Linia 335: / Linia 354: @@
 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>.
+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ę
+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ą.
+<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}
+\mathtt{newloc} : \mathbf{Store} \to \mathbf{Loc}
 </math>
@@ Linia 349: / Linia 368: @@
 <math>
-\mathtt{new}(s) \notin \dom(s).
+\mathtt{newloc}(s) \notin \mathrm{dom}(s).
 </math>
@@ Linia 358: / Linia 377: @@
        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)
+\quad \mbox{ gdzie } l = \mathtt{newloc}(s).
 </math>
-Zauważmy, że stan <math> s' </math> po zakończeniu instrukcji
+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
+<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.
+lokalnej <math>x</math>, tzn. <math>s(l)</math> jest określone.
-Ale lokacja <math> l </math> jest ,,nieosiągalna" w środowisku
+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
+<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.
+<math>E</math> całego bloku nie jest modyfikowane.
 Poniżej przedstawiamy reguły dla pozostałych instrukcji.
@@ Linia 382: / Linia 400: @@
 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ę
+następnej, a stan oczywiście ewoluuje wraz ze zmieniającymi się
 wartościami zmiennych.
@@ Linia 410: / Linia 428: @@
       {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}
+\frac{E \,\vdash\, b, s \,\longrightarrow\, \mathbf{false}
        \quad \quad
        E \,\vdash\, I_2, s \,\longrightarrow\, s'}
@@ Linia 417: / Linia 435: @@
 <math>
-{E \,\vdash\, \mathbf{if}\, b \,\mathbf{then}\, (\mathbf{while}\, b \,\mathbf{do}\, I) \,\mathbf{else}\, \mathbf{skip}, 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'}
+     {E \,\vdash\, \mathbf{while}\, b \,\mathbf{do}\, I, s \,\longrightarrow\, s'}
 </math>
@@ Linia 433: / Linia 451: @@
+<br>
-===== Wariant (dealokacja) =====
+'''Wariant (dealokacja)'''
+<br>
 Przypomnijmy sobie semantykę bloku
@@ Linia 442: / Linia 461: @@
        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)
+\quad \mbox{ gdzie } l = \mathtt{newloc}(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
+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
+Oznaczałoby to przywrócenie lokacji <math>l</math> do puli wolnych
 (nieużywanych) lokacji.
@@ Linia 460: / Linia 479: @@
 </math>
-gdzie <math> \bar{s} </math> to stan <math> s'' </math> ,,okrojony" do dziedziny stanu <math> 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
+Powinniśmy po prostu przywrócić nieokreśloność stanu dla lokacji
-<math> l </math>.
+<math>l</math>.
 Natomiast oczywiście nie ma potrzeby dealokownia środowiska!
 Oto rozwiązanie:
@@ Linia 470: / Linia 489: @@
        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)
+\quad \mbox{ gdzie } l = \mathtt{newloc}(s)
 </math>
+</div></div>
+}}
 == Zadania domowe ==
@@ Linia 495: / Linia 516: @@
 </math>
-Instrukcja <math> \mathbf{throw}\, x </math> oznacza podniesienie wyjątku o nazwie <math> x </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>.
+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
+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>
+</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>
+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
+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
+</math> oraz <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
+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>
+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>,
+i wszystkie instrukcje wewnątrz <math>I_1</math>,
-ale ''nie'' otacza <math> I_2 </math>.
+ale ''nie'' otacza <math>I_2</math>.
 ==== Zadanie 2 ====
-Zaproponuj modyfikację semantyki języka Small, w której deklaracja
+Zaproponuj modyfikację semantyki, w której deklaracja
-jest wykonywana ,,równolegle\'', analogicznie do przypisania
+jest wykonywana ,,równolegle", analogicznie do przypisania
 równoległego. Przy takiej semantyce kolejność poszczególnych
-deklaracji nie powinna wpływać na wynik programu.
+deklaracji powinna być nieistotna.