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

← poprzednia edycja następna edycja →

WizualnieWikikod

Wersja z 14:55, 26 lip 2006

Ćwiczenia 1: semantyka operacyjna wyrażeń (małe kroki)

Zadanie 1 (przygotowawcze)

Rozważmy prosty język wyrażeń, którego składnia opisana jest następującą gramatyką:

$n : : = 0 | 1 | \dots$

$x : : = \dots (i d e n t y f i k a t o r y) \dots$

$e : : = n | x | e_{1} + e_{2} | 𝐢 𝐟 e_{1} 𝐭 𝐡 𝐞 𝐧 e_{2} 𝐞 𝐥 𝐬 𝐞 e_{3}$

Wynikiem wyrażenienia warunkowego $𝐢 𝐟 e_{1} 𝐭 𝐡 𝐞 𝐧 e_{2} 𝐞 𝐥 𝐬 𝐞 e_{3}$ jest wartość wyrażenia $e_{2}$ , o ile wyrażenie $e_{1}$ oblicza się do wartości różnej od zera; w przeciwnym przypadku wynikiem jest wartość wyrażenia $e_{3}$ .

Zaproponuj semantykę operacyjną (małe kroki) dla tego języka.

Rozwiązanie

Zacznijmy od ustalenia notacji i dziedzin syntaktycznych. Niech $𝐍 𝐮 𝐦$ oznacza zbiór stałych liczbowych, $n \in 𝐍 𝐮 𝐦 = {0, 1, \dots}$ . Podobnie, niech $𝐕 𝐚 𝐫$ oznacza zbiór identyfikatorów, które mogą być nazwami zmiennych; $x \in 𝐕 𝐚 𝐫$ . Wreszcie, niech $𝐄 𝐱 𝐩$ oznacza zbiór wyrażeń; $e \in 𝐄 𝐱 𝐩$ . Dla ułatwienia zapisywania reguł zakładamy, ze stałe liczbowe sa wyrażeniami, czyli $𝐍 𝐮 𝐦 \subseteq 𝐄 𝐱 𝐩$ .

Będziemy potrzebować zbioru stanów, opisujących wartości przypisane zmiennym. Najprostszym rozwiązaniem jest przyjąc, że stan to funkcja z $𝐕 𝐚 𝐫$ do $𝐍 𝐮 𝐦$ . Oznaczmy przez $𝐒 𝐭 𝐚 𝐭 𝐞$ zbiór wszystkich takich funkcji; stany oznaczac będziemy przez $s, s_{1}, s^{'}, \dots \in 𝐒 𝐭 𝐚 𝐭 𝐞$ .

W naszej semantyce będziemy potrzebowac tranzycji dwóch postaci. Po pierwsze, tranzycja

$e, s ⟹ e^{'}, s$

oznaczająca mały krok w trakcie obliczania wyrażenia $e$ w stanie $s$ , w wyniku którego $e$ wyewoluowało do $e^{'}$ . Stan nie ulega zmiania podczas obliczania wyrażenia, więc to samo $s$ figuruje po lewej i prawej stronie strzałki.

Po drugie, tranzycja $e, s ⟹ n$

będzie oznaczaczać, że wyrażenie $e$ jest już policzone, a jego wartością jest $n$ .

Zatem przyjmijmy, że zbiór konfiguracji to

$(𝐄 𝐱 𝐩 \times 𝐒 𝐭 𝐚 𝐭 𝐞) \cup 𝐍 𝐮 𝐦$

a konfiguracje końcowe to $𝐍 𝐮 𝐦$ .

Uwaga: tranzycje pierwszej postaci mogłyby również wyglądać następująco: $e, s ⟹ e^{'};$ wtedy zbiorem konfiguracji byłby zbiór $(𝐄 𝐱 𝐩 \times 𝐒 𝐭 𝐚 𝐭 𝐞) \cup 𝐄 𝐱 𝐩$ a konfiguracje końcowe pozostałyby bez zmian (koniec uwagi).

Najprostsze są tranzycje prowadzące do konfiguracji końcowej:

$n, s ⟹ n$

Zmienna oblicza się do swojej wartości w bieżącym stanie: $x, s ⟹ n, s o ile s (x) = n$

Teraz zajmiemy się dodawaniem $e_{1} + e_{2}$ . Ponieważ semantyka jest w stylu małych kroków, musimy zdecydować się czy najpierw obliczyć pierwszy (lewy) składnik Parser nie mógł rozpoznać (błąd składni): {\displaystyle e_1 ] czy drugi? Jeśli wybierzemy lewy, otrzymamy regułę: <math> \frac{e_1, s \,\Longrightarrow\, e'_1, s} {e_1 + e_2, s \,\Longrightarrow\, e'_1 + e_2}. }

Czyli mały krok w $e_{1}$ stanowi też mały krok w $e_{1} + e_{2}$ . Po zakończeniu obliczania $e_{1}$ przechodzimy do $e_{2}$ :

$\frac{e_{2}, s ⟹ e'_{2}, s}{n + e_{2}, s ⟹ n + e'_{2}, s} .$

A na końcu dodajemy:

$n_{1} + n_{2}, s ⟹ n, s o ile n = n_{1} + n_{2} .$

Zauważmy tutaj pewną subtelność, dotyczącą dwóch wystąpień symbolu +: pierwsze wystąpienie oznacza jedną z konstrukcji składniowych języka, a drugie oznacza operację dodawania w zbiorze $𝐍 𝐮 𝐦$ . Pozwalamy sobie na taką kolizję oznaczeń, gdyż nie powinna ona prowadzić do niejednoznaczności. Pamiętajmy, że składnia języka jest składnią abstrajkcyjną, więc zamiast $e_{1} + e_{2}$ moglibyśmy równie dobrze pisać np. $a d d (e_{1}, e_{2})$ .

Inna możliwą strategią obliczania $e_{1} + e_{2}$ jest strategia prawostronna, którą otrzymujemy zastępując pierwsze dwie z trzech powyższych reguł przez:

$\frac{e_{2}, s ⟹ e'_{2}, s}{e_{1} + e_{2}, s ⟹ e_{1} + e'_{2}} \frac{e_{1}, s ⟹ e'_{1}, s}{e_{1} + n, s ⟹ e'_{1} + n, s} .$

Ponadto, jeśli przyjmiemy wszystkie pięc reguł, otrzymamy strategię równoległą, polegającą na obliczaniu jednocześnie $e_{1}$ i $e_{2}$ . Bardziej precyzyjnie mówiąc, małe kroki obliczające obydwa podwyrażenia przeplatają się, i to w dowolny sposób. Ta dowolność prowadzi do niedeterminizmu, czyli do sytuacji, gdy kolejna (następna) konfiguracja nie jest wyznaczona jednoznacznie. Jest tak, gdyż jednocześnie możemy mieć dwie tranzycje

$e_{1} + e_{2}, s ⟹ e'_{1} + e_{2}, s e_{1} + e_{2}, s ⟹ e_{1} + e'_{2}, s .$

Zauważmy natomiast, że kolejność przeplatania się małych kroków obliczających $e_{1}$ i $e_{2}$ nie wpływa w tym przypadku na końcową wartość całego wyrażenia.

Na koniec reguły dla wyrażenia warunkowego.

$\frac{e_{1}, s ⟹ e'_{1}, s}{𝐢 𝐟 e_{1} 𝐭 𝐡 𝐞 𝐧 e_{2} 𝐞 𝐥 𝐬 𝐞 e_{3}, s ⟹ 𝐢 𝐟 e'_{1} 𝐭 𝐡 𝐞 𝐧 e_{2} 𝐞 𝐥 𝐬 𝐞 e_{3}, s}$

$𝐢 𝐟 n 𝐭 𝐡 𝐞 𝐧 e_{2} 𝐞 𝐥 𝐬 𝐞 e_{3}, s ⟹ e_{2}, s o ile n \neq 0$

$𝐢 𝐟 n 𝐭 𝐡 𝐞 𝐧 e_{2} 𝐞 𝐥 𝐬 𝐞 e_{3}, s ⟹ e_{3}, s o ile n = 0$

Zadanie 2

Rozszerzmy język wyrażeń z poprzedniego zadania o jedną konstrukcję $e : : = \dots | 𝐥 𝐞 𝐭 x = e_{1} 𝐢 𝐧 e_{2}$

Wyrażenie $𝐥 𝐞 𝐭 x = e_{1} 𝐢 𝐧 e_{2}$ zawiera w sobie deklarację $x = e_{1}$ , która stanowi jedyny mechannizm wiązania identyfikatorów w naszym języku. Wartość wyrażenia $𝐥 𝐞 𝐭 x = e_{1} 𝐢 𝐧 e_{2}$ obliczamy następująco: najpierw oblicza się wartość $e_{1}$ , podstawia ją na zmienna $x$ , a następnie oblicza wyrażenie $e_{2}$ . Zakresem zmiennej $x$ jest wyrażenie $e_{2}$ , ale jeśli w $e_{2}$ występuje podwyrażenie $𝐥 𝐞 𝐭 x = \dots 𝐢 𝐧 e$ to odwołania do $x$ wewnątrz $e$ odnoszą się do najbliższej (najbardziej zagnieżdzonej) deklaracji zmiennej $x$ . Taki mechanizm wiązania identyfikatorów nazywamy wiązaniem statycznym.

Zakładamy, że na początku wartości wszystkich zmiennych są nieokreślone, czyli zmienne są niezainicjowane, a odwołanie do niezainicjowanej zmiennej jest uważane za niepoprawne.

Przykłady

$𝐥 𝐞 𝐭 x = z + z 𝐢 𝐧 𝐥 𝐞 𝐭 y = 7 𝐢 𝐧 𝐥 𝐞 𝐭 x = y + 3 𝐢 𝐧 x + x + y wynik = 24$ $𝐥 𝐞 𝐭 y = 5 𝐢 𝐧 𝐥 𝐞 𝐭 x = (𝐥 𝐞 𝐭 y = 3 𝐢 𝐧 y + y) 𝐢 𝐧 x + y wynik = 11$ Parser nie mógł rozpoznać (błąd składni): {\displaystyle \mathbf{let}\, z = 5 \,\mathbf{in}\, x+z \quad \quad \mbox{brak wyniku; odwołanie do niezainicjowanej zmiennej}\, x } $𝐥 𝐞 𝐭 x = 1 𝐢 𝐧 𝐥 𝐞 𝐭 x = x + x 𝐢 𝐧 x wynik = 2$

Rozwiązanie

Podobnie jak poprzednio, stan powinien opisywać wartości przypisane zmiennym, ale powinniśmy też uwzględnić niezainicjowane zmienne, czyli zmienne bez żadnej wartości. Przyjmijmy zatem, że stan to skończona funkcja częściowa z $𝐕 𝐚 𝐫$ do $𝐍 𝐮 𝐦$ . Oznaczmy przez $𝐒 𝐭 𝐚 𝐭 𝐞$ zbiór wszystkich takich funkcji. Naturalnym stanem początkowym jest stan pusty, tzn. pusta funkcja częściowa, który będziemy oznaczać $\emptyset$ . A wartość wyrażenia $e$ w stanie początkowym wynosi $n$ o ile zachodzi:

$e, \emptyset ⟹^{*} n .$

Będziemy potrzebowac tranzycji dwóch postaci, podobnie jak poprzednio, ale pierwsza postać będzie trochę ogólniejsza:

$e, s ⟹ e^{'}, s^{'} .$

Tranzycja ta oznacza mały krok w trankcie obliczania wyrażenia $e$ w stanie $s$ , w wyniku którego $e$ wyewoluowało do $e^{'}$ a nowym stanem jest $s^{'}$ . Stan może się teraz zmienić na skutek deklaracji zmiennych.

Ponieważ stan jest funkcją częściową, musimy zmienić niektóre reguły, np.

$x, s ⟹ n, s o ile s (x) jest określone i s (x) = n$

Zadanie 3

Zmodyfikuj semantykę z poprzedniego zadania tak, aby uzyskać leniwą ewaluację wyrażeń, zgodnie z dyrektywą: nie obliczaj wyrażenia o ile jego wynik nie jest potrzebny (albo: obliczaj wartość wyrażenia dopiero wtedy, gdy jego wynik jest naprawdę potrzebny). Spojrzmy na przykład:

$𝐥 𝐞 𝐭 x = 7 𝐢 𝐧 𝐥 𝐞 𝐭 y = y + y 𝐢 𝐧 x + x$

Według semantyki z poprzedniego zadania wyrażnie to nie ma wartości, bo w deklaracji $y = y + y$ jest odwołanie do niezainicjowanej zmiennej. Natomiast w semantyce leniwej wyrażenie to obliczy się do wartości $14$ , ponieważ wyrażenie $y + y$ nie będzie wogóle obliczane. Będzie tak dlatego, że w wyrażeniu $x + x$ nie ma odwołań do zmiennej $y$ .

Rozwiązanie

Zadanie 4

Dotychczas wystąpienie błędu podczas obliczania wyrażenia, np. odwołanie do niezainicjowanej zmiennej, powodowało, że wyrażenie nie posiadało wartości (nie było ciągu tranzycji prowadzących do konfiguracji końcowej). Zmodyfikuj którąś z semantyk z poprzednich zadań tak, aby błąd był komunikowany jako jedna z konfiguracji końcowych. To znaczy: jeśli obliczenie wyrażenia $e$ w stanie $s$ jest niemożliwe bo wystąpił błąd, to

$e, s ⟹^{*} B l a d$

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

Wersja z 14:55, 26 lip 2006

Spis treści

Ćwiczenia 1: semantyka operacyjna wyrażeń (małe kroki)

Zadanie 1 (przygotowawcze)

Rozwiązanie

Zadanie 2

Przykłady

Rozwiązanie

Zadanie 3

Rozwiązanie

Zadanie 4

Menu nawigacyjne

Działania na stronie

Opcje strony

Narzędzia osobiste

Nawigacja

Szukaj

Narzędzia

@@ Linia 1: / Linia 1: @@
-== Ćwiczenia 1: Semantyka operacyjna wyrażeń ==
+== Ćwiczenia 1: semantyka operacyjna wyrażeń (małe kroki) ==
+==== Zadanie 1 (przygotowawcze) ====
+Rozważmy prosty język wyrażeń, którego składnia opisana jest
+następującą gramatyką:
-==== Zadanie 1 ====
-Semantyka języka Tiny z wykładu używała funkcji semantycznych
 <math>
-B, E : State \to State
+n \, ::= \,\, 0 \,\,|\,\, 1 \,\,|\,\, \ldots
 </math>
-dla określenie znaczenia wyrażeń boolowskich i arytmetycznych.
-Zdefiniuj znaczenie wyrażeń za pomocą semantyki operacyjnej,
-w stylu dużych kroków (semantyka naturalna) i małych kroków.
-==== Rozwiązanie ====
-Przypomnijmy składnię wyrażeń boolowskich i arytmetycznych:
 <math>
-b \, ::= \,\,
+x \, ::= \,\, \ldots \, (identyfikatory) \, \ldots
-        true   \,\,|\,\,
-        false  \,\,|\,\,
-        e_1 \leq e_2  \,\,|\,\,
-        \neg b  \,\,|\,\,
-        b_1  \land  b_2   \,\,|\,\,
-        b_1  \lor  b_2
 </math>
 <math>
-e \,  ::= \,\,
+e \,  ::=  \,\,
-   \,\,|\,\,   1     \,\,|\,\,   \ldots   \,\,|\,\,
+         n   \,\,|\,\,
-         x  \,\,|\,\,
+         x   \,\,|\,\,
-         e_1 + e_2  \,\,|\,\,
+         e_1 + e_2   \,\,|\,\,
-         e_1 * e_2  \,\,|\,\,
+         \mathbf{if}\, e_1 \,\mathbf{then}\, e_2 \,\mathbf{else}\, e_3
-        e_1 - e_2  \,\,|\,\,   \ldots
 </math>
+Wynikiem wyrażenienia warunkowego <math> \mathbf{if}\, e_1 \,\mathbf{then}\, e_2 \,\mathbf{else}\, e_3 </math>
+jest wartość wyrażenia <math> e_2 </math>, o ile wyrażenie
+<math> e_1 </math> oblicza się do wartości różnej od zera; w przeciwnym
+przypadku wynikiem jest wartość wyrażenia <math> e_3 </math>.
-Zacznijmy od dużych kroków.
+Zaproponuj semantykę operacyjną (małe kroki) dla tego języka.
-===== Semantyka naturalna =====
-Chcemy, aby tranzycje wyrażen wyglądały następująco:
+==== Rozwiązanie ====
-<math>
+Zacznijmy od ustalenia notacji i dziedzin syntaktycznych.
-e, s \longrightarrow n
+Niech <math> \mathbf{Num} </math> oznacza zbiór stałych liczbowych,
-\quad \quad \quad
+<math> n \in \mathbf{Num} = \{ 0, 1, \ldots \} </math>.
-b, s \longrightarrow l,
+Podobnie, niech <math> \mathbf{Var} </math> oznacza zbiór identyfikatorów, które
-</math>
+mogą być nazwami zmiennych; <math> x \in \mathbf{Var} </math>.
+Wreszcie, niech <math> \mathbf{Exp} </math> oznacza zbiór wyrażeń;
+<math> e \in \mathbf{Exp} </math>.
+Dla ułatwienia zapisywania reguł zakładamy, ze stałe
+liczbowe sa wyrażeniami, czyli <math> \mathbf{Num} \subseteq \mathbf{Exp} </math>.
-gdzie
+Będziemy potrzebować zbioru ''stanów'', opisujących wartości
-<math>s \in State</math>, <math>n</math> jest liczbą całkowitą,
+przypisane zmiennym.
-<math>n \in Int</math>, a <math>l \in Bool = \{ true, false \}</math>.
+Najprostszym rozwiązaniem jest przyjąc, że stan to funkcja
-Tranzycja taka oznacza, że wyrażenie <math>e</math> w stanie <math>s</math> wylicza się do
+z <math> \mathbf{Var} </math> do <math> \mathbf{Num} </math>.
-wartości <math>n</math>, oraz że wyrażenie logiczne <math>b</math> w
+Oznaczmy przez <math> \mathbf{State} </math> zbiór wszystkich takich funkcji;
-stanie <math>s</math> wylicza się do <math>l</math>.
+stany oznaczac będziemy przez <math> s, s_1, s', \ldots \in \mathbf{State} </math>.
-Zauważmy, że zakładamy tu, iż obliczenie wyrażenia nie zmienia
-stanu (nie ma efektów ubocznych).
-W tym celu rozszerzamy zbiór konfiguracji <math>\Gamma</math> następująco:
+W naszej semantyce będziemy potrzebowac tranzycji dwóch postaci.
+Po pierwsze, tranzycja
 <math>
-\Gamma = (Instr \times State) \cup (Expr \times State) \cup (BExpr \times State) \cup State \cup Int \cup Bool
+e, s \,\Longrightarrow\, e', s
 </math>
-gdzie Instr oznacza zbiór instrukcji (jedna z kategorii syntaktycznych
+oznaczająca mały krok w trakcie obliczania wyrażenia <math> e </math>
-języka Tiny), Expr zbiór wyrażeń arytmetycznych a BExpr
+w stanie <math> s </math>, w wyniku którego <math> e </math> wyewoluowało do
-zbiór wyrażeń boolowskich.
+<math> e' </math>. Stan nie ulega zmiania podczas obliczania wyrażenia,
-<math>State = Var \to Int</math>.
+więc to samo <math> s </math> figuruje po lewej i prawej stronie strzałki.
-Konfiguracje końcowe pozostają bez zmian (State).
-Tranzycje dla instrukcji pozostają zasadniczo bez zmian, z tym,
-że odwołania do funkcji semantycznych dla wyrazżen zastępujemy
-przez odpowiednie tranzycje.
-Np. dla instrukcji pętli będziemy mieć następujące reguły:
+Po drugie, tranzycja
 <math>
-\frac{b, s \longrightarrow true  \quad \quad
+e, s \,\Longrightarrow\, n
-      I; \mathbf{while}\, b \mathbf{do}\, I, s \longrightarrow s'}
-{\mathbf{while}\, b\, \mathbf{do}\, I, s \longrightarrow s'}
 </math>
+będzie oznaczaczać, że wyrażenie <math> e </math> jest już policzone,
+a jego wartością jest <math> n </math>.
+Zatem przyjmijmy, że zbiór konfiguracji to
 <math>
-\frac{b, s \longrightarrow false}
+( \mathbf{Exp} \times \mathbf{State} ) \, \cup \, \mathbf{Num}
-{\mathbf{while}\, b\, \mathbf{do}\, I, s \longrightarrow s}
 </math>
-Podobnie dla instrukcji warunkowej.
+a konfiguracje końcowe to <math> \mathbf{Num} </math>.
-Teraz zajmiemy się tranzycjami dla wyrażeń.
-Zacznijmy od stalych arytmetycznych:
+'''Uwaga:''' tranzycje pierwszej postaci mogłyby również wyglądać
+następująco:
 <math>
-n, s \longrightarrow n, \quad \quad   \mbox{dla } n \in Int
+e, s \,\Longrightarrow\, e';
 </math>
+wtedy zbiorem konfiguracji byłby zbiór
-Zauważmy, iż celowo nie odróżniamy liczby <math>n \in Int</math> od
-stałej reprezentującej tę liczbę, która może pojawić się
-w wyrażeniach zgodnie z przyjętą przez nas składnią.
-Czyli zakładamy, że Int jest podzbiorem zbioru wyrażeń.
-W powyższej tranzycji, <math>n</math> po lewej stronie to stała reprezentująca
-liczbę, która widnieje po prawej stronie.
-Analogiczne tranzycje dla stałych boolowskich to:
 <math>
-true, s \longrightarrow true
+( \mathbf{Exp} \times \mathbf{State} ) \, \cup \, \mathbf{Exp}
-\quad \quad \quad
-false, s \longrightarrow false
 </math>
+a konfiguracje końcowe pozostałyby bez zmian
+'''(koniec uwagi)'''.
-Analogicznie, czynimy tu założenie, że Bool jest podbiorem
-wyrażen boolowskich.
-Operatory arytmetyczne definiujemy następująco:
+Najprostsze są tranzycje prowadzące do konfiguracji końcowej:
 <math>
-\frac{e_1, s \longrightarrow n_1   \quad \quad
+n, s \,\Longrightarrow\, n
-        e_2, s \longrightarrow n_2 \quad \quad
-        n = n_1 + n_2    }
-{e_1 + e_2,s \longrightarrow n}
 </math>
-Czyli aby obliczyć sumę <math>e_1 + e_2</math> w stanie
+Zmienna oblicza się do swojej wartości w bieżącym stanie:
-<math>s</math>, trzeba najpierw obliczyć <math>e_1</math> i
-<math>e_2</math> w stanie <math>s</math>, a następnie dodać obliczone wartości.
-Zauważmy, że nie specyfikujemy kolejności, w jakiej mają się
-obliczać <math>e_1</math> i <math>e_2</math>.
-I choć tutaj nie ma to żadnego znaczenia, w przyszłości
-będzie inaczej, gdy jezyk będzie umożliwiał efekty uboczne
-podzas obliczania wyrażeń.
-Podobne reguły można napisać dla pozostałych operacji
-arytmnetycznych, oraz dla spójników logicznych:
 <math>
-\frac{b_1, s \longrightarrow l_1  \quad \quad
+x, s \,\Longrightarrow\, n, s \quad \mbox{ o ile } s(x) = n
-      b_2, s \longrightarrow l_2  \quad \quad  l = l_1 \land l_2}
-{b_1  \land  b_2, s \longrightarrow l}
 </math>
-Oczywiście jeśli <math>b_1</math> oblicza się do false, wartość
+Teraz zajmiemy się dodawaniem <math> e_1 + e_2 </math>. Ponieważ semantyka jest w stylu małych
-całego wyrażenia jest false niezależnie od wartości wyrażenia
+kroków, musimy zdecydować się czy najpierw obliczyć pierwszy (lewy) składnik
-<math>b_2</math>.
+<math> e_1 ] czy drugi?
-Czyli jeśli zaczniemy od obliczenia <math>b_1</math> i wynikiem będzie
+Jeśli wybierzemy lewy, otrzymamy regułę:
-false, to nie ma wogóle potrzeby obliczania <math>b_2</math>.
-Oto odpowiednie reguły (nazwijmy je regułami lewo-stronnymi, ponieważ
-rozpoczynamy od ''lewego'' koniunktu):
 <math>
-\frac{b_1, s \longrightarrow false}
+\frac{e_1, s \,\Longrightarrow\, e'_1, s}
-{b_1 \land b_2, s \longrightarrow false}
+     {e_1 + e_2, s \,\Longrightarrow\, e'_1 + e_2}.
-\frac{b_1, s \longrightarrow true  \quad \quad
-        b_2, s \longrightarrow l}
-{b_1 \land b_2,s \longrightarrow l}
 </math>
-Wybraliśmy następującą kolejność obliczania wyrażeń:
+Czyli mały krok w <math> e_1 </math> stanowi też mały krok w <math> e_1 + e_2 </math>.
-najpierw b_1, potem b_2.
+Po zakończeniu obliczania <math> e_1 </math> przechodzimy do <math> e_2 </math>:
-Pozostawiamy Czytelnikowi napisanie analogicznych reguł dla
-kolejności odwrotnej (reguły prawo-stronne).
-Rozważmy też następującą kombinację obydwu semantyk
-(reguły ''równoległe''):
 <math>
-\frac{b_1, s \longrightarrow false}
+\frac{e_2, s \,\Longrightarrow\, e'_2, s}
-{b_1 \land b_2,s \longrightarrow false}
+     {n + e_2, s \,\Longrightarrow\, n + e'_2, s}.
-\quad \quad \quad
-\frac{b_2, s \longrightarrow false}
-{b_1 \land b_2,s \longrightarrow false}
 </math>
-Czyli jeśli którekolwiek z podwyrażeń daje wynik false,
+A na końcu dodajemy:
-to taki wynik zyskuje całe wyrażenie.
-Dodatkowo potrzebujemy jeszcze reguły:
 <math>
-\frac{b_1, s \longrightarrow true  \quad \quad
+n_1 + n_2, s \,\Longrightarrow\, n, s \quad \mbox{ o ile } n = n_1 + n_2.
-b_2, s \longrightarrow true}
-{b_1 \land b_2,s \longrightarrow true}
 </math>
-Zauważmy, że powyższych reguł nie da sie zaimplementować
+Zauważmy tutaj pewną subtelność, dotyczącą dwóch wystąpień
-sekwencyjnie: nie wiadomo czy najpierw obliczać
+symbolu ''+'': pierwsze wystąpienie oznacza jedną z konstrukcji składniowych
-<math>b_1</math> czy <math>b_2</math>.
+języka, a drugie oznacza operację dodawania w zbiorze <math> \mathbf{Num} </math>.
-Reguły te odpowiadają raczej strategii ,,równoległej'':
+Pozwalamy sobie na taką kolizję oznaczeń, gdyż nie powinna ona
-obliczaj ,,jednocześnie'' b_1 i b_2 do momentu, gdy
+prowadzić do niejednoznaczności. Pamiętajmy, że składnia języka jest
-jedno z nich obliczy się do wynikiem false, albo aż obydwa się zakończą
+składnią abstrajkcyjną, więc zamiast <math> e_1 + e_2 </math> moglibyśmy równie
-z wynikiem true.
+dobrze pisać np. <math> {\mathrm{add}}(e_1, e_2) </math>.
-W naszym prostym języku wszystkie cztery warianty
+Inna możliwą strategią obliczania <math> e_1 + e_2 </math> jest strategia
-są równoważne. Różnice pomiędzy nimi zobaczymy jednak już w
+''prawostronna'', którą otrzymujemy zastępując pierwsze dwie z trzech
-następnym zadaniu, w którym pojawi się prosta
+powyższych reguł przez:
-odmiana efektów ubocznych (błąd wykonania).
-Reguły dla pozostałych spójników logicznych oraz dla
-negacji pozostawiamy jako ćwiczenie.
-A teraz małe kroki.
-===== Strukturalna semantyka operacyjna (małe kroki)  =====
-Chcemy, aby tranzycje dla wyrażeń były postaci:
 <math>
-e, s \longrightarrow e', s
+\frac{e_2, s \,\Longrightarrow\, e'_2, s}
-</math>
+     {e_1 + e_2, s \,\Longrightarrow\, e_1 + e'_2}
-i podobnie dla wyrażeń boolowskich:
+\quad \quad \quad
-<math>
+\frac{e_1, s \,\Longrightarrow\, e'_1, s}
-b, s \longrightarrow b', s
+     {e_1 + n, s \,\Longrightarrow\, e'_1 + n, s}.
 </math>
-gdzie <math>s \in State</math>.
-Przyjmijmy na razie takie same konfiguracje i konfiguracje końcowe
-jak dla semantyki naturalnej.
-Zacznijmy od wyrażeń boolowskich.
+Ponadto, jeśli przyjmiemy wszystkie pięc reguł, otrzymamy strategię
+''równoległą'', polegającą na obliczaniu jednocześnie <math> e_1 </math> i
+<math> e_2 </math>. Bardziej precyzyjnie mówiąc, małe kroki obliczające
+obydwa podwyrażenia przeplatają się, i to w dowolny sposób.
+Ta dowolność prowadzi do ''niedeterminizmu'', czyli do sytuacji, gdy
+kolejna (następna) konfiguracja nie jest wyznaczona jednoznacznie.
+Jest tak, gdyż jednocześnie możemy mieć dwie tranzycje
 <math>
-true, s \Longrightarrow true
+e_1 + e_2, s \,\Longrightarrow\, e'_1 + e_2, s
-\quad \quad
+\quad \quad \quad
-false, s \Longrightarrow false
+e_1 + e_2, s \,\Longrightarrow\, e_1 + e'_2, s.
 </math>
-Przejdźmy do spójników logicznych, powiedzmy <math>b_1 \land b_2</math>.
+Zauważmy natomiast, że kolejność przeplatania się małych kroków obliczających
-Ponieważ opisujemy teraz pojedyncze (małe) kroki składające się na
+<math> e_1 </math> i <math> e_2 </math> nie wpływa w tym przypadku na końcową wartość
-wykonanie programu, musimy podać w jakiej kolejności będą się
+całego wyrażenia.
-obliczać <math>b_1</math> i <math>b_2</math>. Zacznijmy od strategii lewostronnej:
+Na koniec reguły dla wyrażenia warunkowego.
 <math>
-\frac{b_1, s \Longrightarrow b'_1, s}
+\frac{e_1, s \,\Longrightarrow\, e'_1, s}
-{b_1 \land b_2, s \Longrightarrow b'_1 \land b_2, s}
+     {\mathbf{if}\, e_1 \,\mathbf{then}\, e_2 \,\mathbf{else}\, e_3, s \,\Longrightarrow\, \mathbf{if}\, e'_1 \,\mathbf{then}\, e_2 \,\mathbf{else}\, e_3, s}
-\quad \quad
-\frac{b_2, s \Longrightarrow b'_2, s}
-{l_1 \land b_2, s \Longrightarrow l_1 \land b_2, s}
-\quad \quad
-l_1 \land l_2 \Longrightarrow l,
-\mbox{ o ile } l = l_1 \land l_2
 </math>
-Podobnie jak poprzednio, możemy zaniechać obliczania
-<math>b_2</math> jeśli <math>b_1</math> oblicza się do false.
-Oto odpowiednio zmodyfikowane reguły:
 <math>
-\frac{b_1, s \Longrightarrow b'_1, s}
+\mathbf{if}\, n \,\mathbf{then}\, e_2 \,\mathbf{else}\, e_3, s \,\Longrightarrow\, e_2, s \quad \mbox{ o ile } n \neq 0
-{b_1 \land b_2, s \Longrightarrow b'_1 \land b_2, s}
-\quad \quad
-false \land b_2, s \Longrightarrow false
-\quad \quad
-true  \land b_2, s \Longrightarrow b_2, s
 </math>
-Analogicznie reguły prawostronne to:
 <math>
-\frac{b_2, s \Longrightarrow b'_2, s}
+\mathbf{if}\, n \,\mathbf{then}\, e_2 \,\mathbf{else}\, e_3, s \,\Longrightarrow\, e_3, s \quad \mbox{ o ile } n = 0
-{b_1 \land b_2, s \Longrightarrow b_1 \land b'_2, s}
-\quad \quad
-b_1 \land false, s \Longrightarrow false
-\quad \quad
-b_1 \land true, s \Longrightarrow b_1, s
 </math>
-Reguły ''równoległe'' otrzymujemy jako sumę reguł lewo- i
-prawostronnych (w sumie 6 reguł). Zauważmy, że obliczanie
-wyrażeń <math>b_1</math> i <math>b_2</math> odbywa się teraz
-w twz. ''przeplocie'': Pojedynczy krok polega na wykonaniu
-jednego kroku obliczenia <math>b_1</math> albo jednego kroku
-obliczenia <math>b_2</math>.
-Zwróćmy też uwagę, że po raz pierwszy nasze tranzycje nie posiadają
-własności ''determinizmu'': wyrażenie <math>b_1 \land b_2</math>
-może wyewoluować w pojedyńczym kroku albo do
-<math>b'_1 \land b_2</math> albo do <math>b_1 \land b'_2</math>.
-Na szczęście, końcowy wynik, do jakiego oblicza się wyrażenie
-jest zawsze taki sam, niezależnie od przeplotu.
-Oto reguła dla negacji:
+==== Zadanie 2 ====
+Rozszerzmy język wyrażeń z poprzedniego zadania o jedną konstrukcję
 <math>
-\neg true, s \Longrightarrow false, s
+e \,  ::=  \,\,
-\quad \quad \quad
+        \ldots   \,\,|\,\,
-\neg false, s \Longrightarrow true, s
+        \mathbf{let}\, x = e_1 \,\mathbf{in}\, e_2
-\quad \quad \quad
-\frac{b, s \Longrightarrow b', s}
-     {\neg b, s \Longrightarrow \neg b', s}
 </math>
-Reguły dla <math>e_1 \leq e_2</math> są następujące:
+Wyrażenie <math> \mathbf{let}\, x = e_1 \,\mathbf{in}\, e_2 </math> zawiera w sobie deklarację
+<math> x = e_1 </math>, która stanowi jedyny mechannizm wiązania
-<math>
+identyfikatorów w naszym języku.
-\frac{e_1, s \Longrightarrow e'_1, s}
+Wartość wyrażenia <math> \mathbf{let}\, x = e_1 \,\mathbf{in}\, e_2 </math> obliczamy następująco:
-{e_1 \leq e_2, s \Longrightarrow e'_1 \leq e_2, s}
+najpierw oblicza się wartość <math> e_1 </math>, podstawia ją na zmienna
+<math> x </math>, a następnie oblicza wyrażenie <math> e_2 </math>.
+Zakresem zmiennej <math> x </math> jest wyrażenie <math> e_2 </math>, ale jeśli w
+<math> e_2 </math> występuje podwyrażenie <math> \mathbf{let}\, x = \ldots \,\mathbf{in}\, e </math> to
+odwołania do <math> x </math> wewnątrz <math> e </math> odnoszą się do ''najbliższej''
+(najbardziej zagnieżdzonej) deklaracji zmiennej <math> x </math>.
+Taki mechanizm wiązania identyfikatorów nazywamy ''wiązaniem
+statycznym''.
-\frac{e_2, s \Longrightarrow e'_2, s}
+Zakładamy, że na początku wartości wszystkich zmiennych są
-{e_1 \leq e_2, s \Longrightarrow e_1 \leq e'_2, s}
+''nieokreślone'', czyli zmienne są niezainicjowane, a odwołanie do
+niezainicjowanej zmiennej jest uważane za niepoprawne.
-n_1 \leq n_2, s \Longrightarrow true, s   \quad \mbox{ o ile }
-n_1 \leq n_2
-n_1 \leq n_2, s \Longrightarrow false, s  \quad  \mbox{ o ile }
+==== Przykłady ====
-n_1 > n_2
-</math>
-Reguły powyższe zależą od semantyki wyrażen arytmetycznych.
-Zauważmy, że ponownie pozostawiliśmy dowolność jeśli chodzi o
-kolejność obliczania wyrażeń arytmetycznych e_1 i e_2.
-Rozważmy teraz instrukcję warunkową i instrukcję pętli.
-Najpierw obliczamy wartość dozoru:
 <math>
-\frac{b, s \Longrightarrow b', s}
+\mathbf{let}\, x = z+z \,\mathbf{in}\, \mathbf{let}\, y = 7 \,\mathbf{in}\, \mathbf{let}\, x = y+3 \,\mathbf{in}\, x+x+y
-{\mathbf{if}\, b\, \mathbf{then}\, I_1\, \mathbf{else}\, I_2, s \Longrightarrow
+\quad \quad \mbox{wynik} = 24
-\mathbf{if}\, b'\, \mathbf{then}\, I_1\, \mathbf{else}\, I_2, s}
+</math>
-\quad \quad
+<math>
-\frac{b, s \Longrightarrow b', s}
+\mathbf{let}\, y = 5 \,\mathbf{in}\, \mathbf{let}\, x = (\, \mathbf{let}\, y = 3 \,\mathbf{in}\, y+y \,) \,\mathbf{in}\, x+y
-{\mathbf{while}\, b\, \mathbf{do}\, I, s \Longrightarrow \mathbf{while}\, b'\, \mathbf{do}\, I, s}
+\quad \quad \mbox{wynik} = 11
 </math>
-a gdy dozór jest już obliczony, podejmujemy decyzję.
-W przypadku instrukcji warunkowej reguły są oczywiste:
 <math>
-\mathbf{if}\, true\, \mathbf{then}\, I_1\, \mathbf{else}\, I_2, s \Longrightarrow I_1, s
+\mathbf{let}\, z = 5 \,\mathbf{in}\, x+z
-\quad \quad \quad
+\quad \quad \mbox{brak wyniku; odwołanie do niezainicjowanej
-\mathbf{if}\, false\, \mathbf{then}\, I_1\, \mathbf{else}\, I_2, s \Longrightarrow I_2, s
+zmiennej}\, x
 </math>
-Gorzej jest w przypadku instukcji pętli. Reguła mogłaby wyglądać tak:
 <math>
-\mathbf{while}\, true\, \mathbf{do}\, I, s \Longrightarrow
+\mathbf{let}\, x = 1 \,\mathbf{in}\, \mathbf{let}\, x = x+x \,\mathbf{in}\, x
-I;\, \mathbf{while}\, ?\, \mathbf{do}\, I, s
+\quad \quad \mbox{wynik} = 2
 </math>
-ale nie wiemy już, jaki był dozór pętli (widzimy tylko wynik
-obliczenia tego dozoru w stanie s, true).
-Możemy odwołać się do tranzycji dużych kroków:
-<math>
+==== Rozwiązanie ====
-\frac{b, s \longrightarrow true}
-{\mathbf{while}\, b\, \mathbf{do}\, I, s \Longrightarrow
- I;\, \mathbf{while}\, b\, \mathbf{do}\, I, s}
-\quad \quad \quad
-\frac{b, s \longrightarrow false}
-{\mathbf{while}\, b\, \mathbf{do}\, I, s \Longrightarrow s}
-</math>
-Takie rozwiązanie nie jest zatem ''czystą'' semantyką
-małych kroków.
-Istnieją inne możliwe rozwiązania, w stylu małych kroków,
-których znalezienie pozostawiamy dociekliwemu czytelnikowi.
-Na koniec podajemy reguły dla operacji arytmetycznych, na przykładzie
+Podobnie jak poprzednio,
-dodawania.
+stan powinien opisywać wartości przypisane zmiennym, ale powinniśmy też
-Przyjmijmy, dla przykładu, strategię lewostronną:
+uwzględnić niezainicjowane zmienne, czyli zmienne bez żadnej wartości.
+Przyjmijmy zatem, że stan to skończona funkcja częściowa z <math> \mathbf{Var} </math> do <math> \mathbf{Num} </math>.
+Oznaczmy przez <math> \mathbf{State} </math> zbiór wszystkich takich funkcji.
+Naturalnym stanem początkowym jest stan ''pusty'', tzn.
+pusta funkcja częściowa, który będziemy oznaczać <math> \emptyset </math>.
+A wartość wyrażenia <math> e </math> w stanie początkowym wynosi <math> n </math>
+o ile zachodzi:
 <math>
-\frac{e_1, s \Longrightarrow e'_1, s}
+e, \emptyset \,\Longrightarrow^{*}\, n.
-{e_1 + e_2, s \Longrightarrow e'_1 + e_2, s}
-\frac{e_2, s \Longrightarrow e'_2, s}
-{n + e_2, s \Longrightarrow n + e'_2, s}
-n_1 + n_2, s \Longrightarrow n, s  \quad \mbox{ o ile }
-n = n_1 + n_2
 </math>
-Niektóre konfiguracje nie były wogóle przez nas używane. Które?
+Będziemy potrzebowac tranzycji dwóch postaci, podobnie jak poprzednio,
+ale pierwsza postać będzie trochę ogólniejsza:
-==== Zadanie 2 ====
-Rozważ dodatkowo operację dzielenia:
 <math>
-e \, ::= \,\,   \ldots   \,\,|\,\,
+e, s \,\Longrightarrow\, e', s'.
-        e_1 / e_2
 </math>
-i rozszerz semantyki z poprzedniego zadania.
-Dzielenie przez zero jest błądem i  kończy natychmiast wykonanie
-programu.
-Oprócz stanu wynikiem programu powinna byc informacja o błędzie,
-jeśli błąd wystąpił.
-==== Rozwiązanie (szkic) ====
+Tranzycja ta oznacza mały krok w trankcie obliczania wyrażenia <math> e </math>
+w stanie <math> s </math>, w wyniku którego <math> e </math> wyewoluowało do
+<math> e' </math> a nowym stanem jest <math> s' </math>.
+Stan może się teraz zmienić na skutek deklaracji zmiennych.
-Dopóki nie wystąpi błąd dzielenia przez zero, semantyka programu
+Ponieważ stan jest funkcją częściową, musimy zmienić niektóre reguły, np.
-powinna być identyczna jak w poprzednim zadaniu. Zatem pozostawiamy
-wszystkie reguły z poprzedniego zadania, tak w semantyce naturalnej
-jak i w semantyce małych kroków.
-Dodatkowo potrzebujemy reguł, które opiszą
-** kiedy powstaje błąd oraz
-** jak zachowuje się program po wystąpieniu błędu
-Zaczynamy od pierwszego punktu.
-W tym celu dodajemy do konfiguracji jedną konfigurację końcową
-<math>Blad</math>.
-Reguła opisująca powstanie błędu może wyglądać np. tak
-w semantyce naturalnej:
 <math>
-\frac{e_2, s \longrightarrow 0}
+x, s \,\Longrightarrow\, n, s \quad \mbox{ o ile } s(x) \mbox{ jest określone i } s(x) = n
-{e_1 / e_2, s \longrightarrow Blad}
 </math>
-a tak w semantyce małych kroków:
-<math>
+==== Zadanie 3 ====
-e_1 / 0, s \Longrightarrow Blad
-</math>
-Pomijamy tutaj reguły dla przypadku, gdy <math>e_2</math>
+Zmodyfikuj semantykę z poprzedniego zadania tak, aby uzyskać
-oblicza się do wartości różnej od zera.
+''leniwą'' ewaluację wyrażeń, zgodnie z dyrektywą: nie obliczaj
-Ponadto dla czytelności przyjęliśmy, że wynikiem tranzycji jest
+wyrażenia o ile jego wynik nie jest potrzebny
-wyłącznie informacja o błędzie, a stan jest zapominany.
+(albo: obliczaj wartość wyrażenia dopiero wtedy, gdy jego wynik jest
-Bez trudu możnaby wszystkie reguły (zarówno te powyżej jak i te
+naprawdę potrzebny). Spojrzmy na przykład:
-poniżej) zmodyfikować tak, by wraz z
-informacją o błędzie zwracany był też stan, w którym błąd się
-pojawił. Np. ostatnia reguła wyglądałaby następująco:
 <math>
-e_1 / 0, s \Longrightarrow Blad, s
+\mathbf{let}\, x = 7 \,\mathbf{in}\, \mathbf{let}\, y = y+y \,\mathbf{in}\, x+x
 </math>
-I zamiast pojedyńczej konfiguracji końcowej <math>Blad</math>, potrzebowalibyśmy
+Według semantyki z poprzedniego zadania wyrażnie to nie ma wartości,
-oczywiście całego zbioru <math>\{Blad\} \times State</math>.
+bo w deklaracji <math> y = y+y </math> jest odwołanie do niezainicjowanej
+zmiennej.
+Natomiast w semantyce leniwej wyrażenie to obliczy się do wartości
+<math> 14 </math>, ponieważ wyrażenie <math> y+y </math> nie będzie wogóle obliczane.
+Będzie tak dlatego, że w wyrażeniu <math> x+x </math> nie ma odwołań do
+zmiennej <math> y </math>.
-Przejdźmy teraz do drugiego punktu. Potrzebujemy dodatkowych reguł,
-które zagwarantują, że błąd, raz pojawiwszy się, propaguje się przez
-wszystkie konstrukcje składniowe, a normalne obliczenie wyrażenia
-jest wstrzymame.
-Zacznijmy od sementyki naturalnej:
-<math>
+==== Rozwiązanie ====
-\frac{e_1, s \longrightarrow Blad}
-{e_1 \leq e_2, s \longrightarrow Blad}
-\quad \quad \quad
-\frac{e_2, s \longrightarrow Blad}
-{e_1 \leq e_2, s \longrightarrow Blad}
-</math>
-Następnie, błąd w wyrażeniu powinien wstrzymać normalne wykonanie
-instrukcji:
-<math>
+==== Zadanie 4 ====
-\frac{b \longrightarrow Blad}
-{\mathbf{if}\, b\, \mathbf{then}\, I_1\, \mathbf{else}\, I_2, s \longrightarrow Blad}
-\quad \quad \quad
-\frac{b \longrightarrow Blad}
-{\mathbf{while}\, b\, \mathbf{do}\, I, s \longrightarrow Blad}
-</math>
-I wreszcie błąd powinien propagować się do kolejnych instrukcji:
+Dotychczas wystąpienie błędu podczas obliczania wyrażenia,
+np. odwołanie do niezainicjowanej zmiennej, powodowało, że
+wyrażenie nie posiadało wartości (nie było ciągu tranzycji
+prowadzących do konfiguracji końcowej). Zmodyfikuj którąś z semantyk
+z poprzednich zadań tak, aby błąd był komunikowany
+jako jedna z konfiguracji końcowych. To znaczy: jeśli obliczenie
+wyrażenia <math> e </math> w stanie <math> s </math> jest niemożliwe bo wystąpił
+błąd, to
 <math>
-\frac{I_1, s \longrightarrow Blad}
+e, s \,\Longrightarrow^{*}\, Blad
-{I_1;\, I_2, s \longrightarrow Blad}
-\quad \quad \quad
-\frac{I_1, s \longrightarrow Blad}
-{\mathbf{if}\, b\, \mathbf{then}\, I_1\, \mathbf{else}\, I_2, s \longrightarrow Blad}
-\quad \quad \quad
-\frac{I_2, s \longrightarrow Blad}
-{\mathbf{if}\, b\, \mathbf{then}\, I_1\, \mathbf{else}\, I_2, s \longrightarrow Blad}
-\quad \quad \quad
-\frac{I, s \longrightarrow Blad}
-{\mathbf{while}\, b\, \mathbf{do}\, I, s \longrightarrow Blad}
 </math>
-I tak dalej.
-Pytanie dla Czytelnika: jak napisać tę semantykę w podejściu mało-krokowym?
-(Powyżej traktowaliśmy tranzycję
-<math> I, s \longrightarrow Blad </math> jak ''duży krok''.
-Ale tak naprawdę pojawienie się błędu powinno spowodować
-''natychmiastowe'' zatrzymanie programu, więc może tranzycję taką
-można również traktować jak ''mały krok'',
-<math> I, s \Longrightarrow Blad </math>?)