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

← poprzednia edycja następna edycja →

WizualnieWikikod

Wersja z 10:18, 27 wrz 2006

Zawartość

Tematem tych zajęć jest semantyka operacyjna wyrażeń (małe kroki).

Semantyka operacyjna wyrażeń

Ćwiczenie 1

Rozważmy bardzo 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

{{{3}}}

Ćwiczenie 2

{{{3}}}

Przykład

$𝐥 𝐞 𝐭 x = 0 𝐢 𝐧 𝐥 𝐞 𝐭 y = 7 𝐢 𝐧 𝐥 𝐞 𝐭 x = y + 3 𝐢 𝐧 x + x + y \mapsto wynik = 24$

$𝐥 𝐞 𝐭 y = 5 𝐢 𝐧 𝐥 𝐞 𝐭 x = (𝐥 𝐞 𝐭 y = 3 𝐢 𝐧 y + y) 𝐢 𝐧 x + y \mapsto wynik = 11$

Parser nie mógł rozpoznać (błąd składni): {\displaystyle \mathbf{let}\, z = 5 \,\mathbf{in}\, x+z \quad \quad \mapsto \quad \quad \mbox{brak wyniku; odwołanie do niezainicjowanej zmiennej}\, x }

$𝐥 𝐞 𝐭 x = 1 𝐢 𝐧 𝐥 𝐞 𝐭 x = x + x 𝐢 𝐧 x + x \mapsto wynik = 4$

Rozwiązanie

{{{3}}}

Zadania domowe

Ćwiczenie 1

Zapisz wariant 2 semantyki z poprzedniego zadania.

Ćwiczenie 2

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 .$

Ćwiczenie 3

Rozważ rozszerzenie języka wyrażeń o wyrażenia boolowskie:

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

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

$b : : = 𝐭 𝐫 𝐮 𝐞 | 𝐟 𝐚 𝐥 𝐬 𝐞 | e_{1} \leq e_{2} | \neg b | b_{1} \land b_{2}$

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

Zaproponuj semantykę małych kroków dla tego języka. Rozważ różne strategie obliczania wyrażeń boolowskich, oraz podejście leniwe. Na przykład w strategii lewostronnej dla $b_{1} \land b_{2}$ , gdy $b_{1}$ zostało obliczone do $𝐟 𝐚 𝐥 𝐬 𝐞$ , w podejściu leniwym nie ma wogóle potrzeby obliczania $b_{2}$ .

@@ Linia 1: / Linia 1: @@
 == Zawartość ==
@@ Linia 43: / Linia 42: @@
 Podobnie, niech <math>\mathbf{Var}</math> oznacza zbiór identyfikatorów, które 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 są wyrażeniami, czyli <math>\mathbf{Num} \subseteq \mathbf{Exp}</math>.
+Dla ułatwienia zapisywania reguł zakładamy, że stałe  liczbowe są wyrażeniami, czyli <math>\mathbf{Num} \subseteq \mathbf{Exp}</math>.
-Będziemy potrzebować zbioru ''stanów'', opisujących wartości przypisane zmiennym.
+Będziemy potrzebować zbioru "stanów", opisujących wartości przypisane zmiennym.
-Najprostszym rozwiązaniem jest przyjąc, że stan to funkcja z <math>\mathbf{Var}</math> do <math>\mathbf{Num}</math>.
+Najprostszym rozwiązaniem jest przyjąć, że stan to funkcja z <math>\mathbf{Var}</math> do <math>\mathbf{Num}</math>.
-Oznaczmy przez <math>\mathbf{State}</math> zbiór wszystkich takich funkcji; stany oznaczac będziemy przez <math>s, s_1, s', \ldots \in \mathbf{State}</math>.
+Oznaczmy przez <math>\mathbf{State}</math> zbiór wszystkich takich funkcji; stany oznaczać będziemy przez <math>s, s_1, s', \ldots \in \mathbf{State}</math>.
 W naszej semantyce będziemy potrzebowac tranzycji dwóch postaci.
@@ Linia 57: / Linia 56: @@
 oznaczające mały krok w trakcie obliczania wyrażenia <math>e</math> w stanie <math>s</math>,  w wyniku którego <math>e</math> wyewoluowało do <math>e'</math>.
-Stan nie ulega zmiania podczas obliczania wyrażenia (nie ma tzw. ''efektów ubocznych''), więc to samo <math>s</math> figuruje po lewej i prawej stronie strzałki.
+Stan nie ulega zmianie podczas obliczania wyrażenia (nie ma tzw. ''efektów ubocznych''), więc to samo <math>s</math> figuruje po lewej i prawej stronie strzałki.
 Po drugie, tranzycje postaci
@@ Linia 77: / Linia 76: @@
 {{
 uwaga||uwaga1|
-Tak naprawdę to druga postać tranzycji nie jest niezbędna, gdyż moglibyśmy umówić się, że konfiguracje końcowe to <math>\mathbf{Num} \times \mathbf{State}</math>.
+Tak naprawdę, druga postać tranzycji nie jest niezbędna, gdyż moglibyśmy umówić się, że konfiguracje końcowe to <math>\mathbf{Num} \times \mathbf{State}</math>.
 }}
@@ Linia 94: / Linia 93: @@
 </math>
-Teraz zajmiemy się dodawaniem <math>e_1 + e_2</math>. Ponieważ semantyka jest w stylu małych kroków, musimy zdecydować się czy najpierw obliczyć pierwszy (lewy) składnik <math>e_1</math> czy drugi?
+Teraz zajmiemy się dodawaniem <math>e_1 + e_2</math>. Ponieważ semantyka jest w stylu małych kroków, musimy zdecydować się, czy najpierw obliczyć pierwszy (lewy) składnik <math>e_1</math>, czy drugi?
-Jeśli wybierzemy lewy (strategia ''lewostronna''), otrzymamy regułę:
+Jeśli wybierzemy lewy (strategia "lewostronna"), otrzymamy regułę:
 <math>
@@ Linia 125: / Linia 124: @@
 Zwróćmy tutaj uwagę na pewną subtelność, dotyczącą dwóch wystąpień symbolu <math>+</math>: pierwsze wystąpienie oznacza jedną z konstrukcji składniowych języka, a drugie oznacza operację dodawania w zbiorze <math>\mathbf{Num}</math>.
-Pozwalamy sobie na taką kolizję oznaczeń, gdyż nie powinna ona prowadzić do niejednoznaczności. Pamiętajmy, że składnia języka jest składnią abstrakcyjną, więc zamiast <math>e_1 + e_2</math> moglibyśmy równie dobrze pisać np. <math>{\mathrm{add}}(e_1, e_2)</math> a wtedy reguła wyglądałaby tak:
+Pozwalamy sobie na taką kolizję oznaczeń, gdyż nie powinna ona prowadzić do niejednoznaczności. Pamiętajmy, że składnia języka jest składnią abstrakcyjną, więc zamiast <math>e_1 + e_2</math> moglibyśmy równie dobrze pisać np. <math>{\mathrm{add}}(e_1, e_2)</math>, a wtedy reguła wyglądałaby tak:
 <math>
@@ Linia 131: / Linia 130: @@
 </math>
-Inną możliwą strategią obliczania <math>e_1 + e_2</math> jest strategia ''prawostronna'', którą otrzymujemy zastępując pierwsze dwie z trzech powyższych reguł przez:
+Inną możliwą strategią obliczania <math>e_1 + e_2</math> jest strategia "prawostronna", którą otrzymujemy zastępując pierwsze dwie z trzech powyższych reguł przez:
 <math>
@@ Linia 141: / Linia 140: @@
 </math>
-Ponadto, jeśli przyjmiemy regułę pierwszą (dla <math>e_1</math>), trzecią i czwartą (dla <math>e_2</math>), otrzymamy strategię ''równoległą'', polegającą na obliczaniu jednocześnie <math>e_1</math> i <math>e_2</math>:
+Ponadto, jeśli przyjmiemy regułę pierwszą (dla <math>e_1</math>), trzecią i czwartą (dla <math>e_2</math>), otrzymamy strategię "równoległą", polegającą na obliczaniu jednocześnie <math>e_1</math> i <math>e_2</math>:
 <math>
@@ Linia 196: / Linia 195: @@
 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 mechanizm wiązania identyfikatorów w naszym języku.
 Deklaracja <math>x = e_1</math> wprowadza nową zmienną <math>x</math> oraz przypisuje jej wartość.
-Wartość wyrażenia <math>\mathbf{let}\, x = e_1 \,\mathbf{in}\, e_2</math> obliczamy następująco: 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>.
+Wartość wyrażenia <math>\mathbf{let}\, x = e_1 \,\mathbf{in}\, e_2</math> obliczamy następująco: najpierw oblicza się wartość <math>e_1</math>, podstawia ją <font color=red>za</font> zmienną <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>, czyli wewnątrz <math>e_2</math> można odwoływać się (wielokrotnie) do zmiennej <math>x</math>;
-Ogólniej, odwołania do zmiennej w wyrażeniu odnoszą się do ''najbliższej'' (najbardziej zagnieżdzonej) deklaracji tej zmiennej.
+Ogólniej, odwołania do zmiennej w wyrażeniu odnoszą się do "najbliższej" (najbardziej zagnieżdzonej) deklaracji tej zmiennej.
 Taki mechanizm wiązania identyfikatorów nazywamy ''wiązaniem statycznym''.
-Przyjmujemy zwykłe (statyczne) reguły przesłaniania zmiennych, np. jeśli w <math>e_2</math> występuje podwyrażenie <math>\mathbf{let}\, x = e \,\mathbf{in}\, e'</math> to
+Przyjmujemy zwykłe (statyczne) reguły przesłaniania zmiennych, np. jeśli w <math>e_2</math> występuje podwyrażenie <math>\mathbf{let}\, x = e \,\mathbf{in}\, e'</math>, to
-deklaracja <math>x = e</math> ''przesłania'' deklarację <math>x = e_1</math> w wyrażeniu <math>e'</math>.
+deklaracja <math>x = e</math> "przesłania" deklarację <math>x = e_1</math> w wyrażeniu <math>e'</math>.
 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.
@@ Linia 243: / Linia 242: @@
 \mathbf{State} = \mathbf{Var} \to_{\mathrm{fin}} \mathbf{Num}
 </math>.
-Naturalnym stanem początkowym jest stan ''pusty'', tzn. pusta funkcja częściowa, który będziemy oznaczać symbolem <math>\emptyset</math>.
+Naturalnym stanem początkowym jest stan "pusty", tzn. pusta funkcja częściowa, który będziemy oznaczać symbolem <math>\emptyset</math>.
 Wartość wyrażenia <math>e</math> w stanie początkowym wynosi <math>n</math>, o ile zachodzi:
@@ Linia 256: / Linia 255: @@
 </math>
-Tranzycja ta oznacza mały krok w trakcie 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>.
+Tranzycja ta oznacza mały krok w trakcie 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.
-Spróbujmy rozszerzyc semantykę z poprzedniego zadania.
+Spróbujmy rozszerzyć semantykę z poprzedniego zadania.
 Ponieważ stan jest funkcją częściową, musimy zmienić niektóre reguły, np.
@@ Linia 286: / Linia 285: @@
 W szczególności dla <math>y \neq x</math>, <math>s[x \mapsto n](y)</math> jest określone wtedy i tylko wtedy, gdy <math>s(y)</math> jest określone.
-Natomiast aby obliczyc <math>e_1</math> potrzebujemy reguły:
+Natomiast aby obliczyc <math>e_1</math>, potrzebujemy reguły:
 <math>
@@ Linia 315: / Linia 314: @@
 </math>
-Nasz błąd polega na tym, że po zakończeniu obliczania podwyrażenia <math>\mathbf{let}\, z = 4 \,\mathbf{in}\, z+z+z</math> ''zapominamy'' przywrócić zmiennej <math>z</math> poprzednią wartość (a właściwie brak wartości w przykładzie powyżej).
+Nasz błąd polega na tym, że po zakończeniu obliczania podwyrażenia <math>\mathbf{let}\, z = 4 \,\mathbf{in}\, z+z+z</math> "zapominamy" przywrócić zmiennej <math>z</math> poprzednią wartość (a właściwie brak wartości w przykładzie powyżej).
 Przedyskutujmy kilka wariantów.
@@ Linia 332: / Linia 331: @@
 <math>
-\mathbf{let}\, x = n \,\mathbf{in}\, e_2, s \,\Longrightarrow\, e_2 \,\mathbf{then}\, \mbox{,,przywróć wartość zmiennej x''}, s[x \mapsto n].
+\mathbf{let}\, x = n \,\mathbf{in}\, e_2, s \,\Longrightarrow\, e_2 \,\mathbf{then}\, \mbox{"przywróć wartość zmiennej x"}, s[x \mapsto n].
 </math>
-czyli potrzebujemy konstrukcji składniowej, która polega na obliczeniu wyrażenia <math>e_2</math> a następnie na przypisaniu zmiennej <math>x</math> danej wartości.
+czyli potrzebujemy konstrukcji składniowej, która polega na obliczeniu wyrażenia <math>e_2</math>, a następnie na przypisaniu zmiennej <math>x</math> danej wartości.
 Rozszerzmy zatem składnię następujaco:
@@ Linia 344: / Linia 343: @@
 </math>
-Wyrażenie <math>e \,\mathbf{then}\, x:= n</math> jest w pewnym sensie dualne do <math>\mathbf{let}\, x = n \,\mathbf{in}\, e</math>, gdyż jedyna (choc niewątpliwie istotna) różnica między nimi to kolejność obliczenia <math>e</math> i przypisania wartości na zmienną <math>x</math>.
+Wyrażenie <math>e \,\mathbf{then}\, x:= n</math> jest w pewnym sensie dualne do <math>\mathbf{let}\, x = n \,\mathbf{in}\, e</math>, gdyż jedyna (choć niewątpliwie istotna) różnica między nimi to kolejność obliczenia <math>e</math> i przypisania wartości na zmienną <math>x</math>.
 Oto nowa reguła
@@ Linia 371: / Linia 370: @@
 Rozwiązanie to jest odrobinę nieeleganckie, gdyż prawie identyczne reguły musimy napisać dwukrotnie.
-Widać to np. w poniższych regułach, ''scalających'' semantykę dla <math>e \,\mathbf{then}\, x := n</math> z semantyką pozostałych wyrażeń:
+Widać to np. w poniższych regułach, "scalających" semantykę dla <math>e \,\mathbf{then}\, x := n</math> z semantyką pozostałych wyrażeń:
 <math>
@@ Linia 391: / Linia 390: @@
 <br>
-Zanim przejdziemy do kolejnego wariantu, zastanówmy się czy istnieje inny sposób rozwiązania trudności związanej z <math>n = \bot</math>, który pozwalałby uniknąć wprowadzania dodatkowej konstrukcji
+Zanim przejdziemy do kolejnego wariantu, zastanówmy się, czy istnieje inny sposób rozwiązania trudności związanej z <math>n = \bot</math>, który pozwalałby uniknąć wprowadzania dodatkowej konstrukcji
 <math>e \,\mathbf{then}\, x := \bot</math>.
 Pomysł może polegać na rozszerzeniu zbioru <math>\mathbf{Num}</math> o dodatkowy element <math>\bot</math>:
@@ Linia 401: / Linia 400: @@
 Wtedy nie musimy pisać dwóch bardzo podobnych wariantów reguł.
 Dodatkowo, w tym rozwiązaniu warto poczynić umowę, że <math>s(x) = \bot</math> reprezentuje brak wartości zmiennej <math>x</math>.
-Wtedy stany są funkcjami całkowitymi z <math>\mathbf{Var}</math> w <math>\mathbf{Num}</math> przyjmującymi wartość różną od <math>\bot</math> tylko dla skończenie wielu elementów.
+Wtedy stany są funkcjami całkowitymi z <math>\mathbf{Var}</math> w <math>\mathbf{Num}</math>, przyjmującymi wartość różną od <math>\bot</math> tylko dla skończenie wielu elementów.
-Pewnym mankamentem jest to, że teraz <math>n = \bot</math> może pojawiać sie w wyrażeniach podobnie jak stałe.
+Pewnym mankamentem jest to, że teraz <math>n = \bot</math> może pojawiać się w wyrażeniach podobnie jak stałe.
 Tym niemniej nie musimy adaptować reguł dla stałych tak, aby radziły one sobie z <math>n = \bot</math>, ponieważ wyrażenia zawierające <math>\bot</math> możemy również uważać za roszerzenie składni.
@@ Linia 431: / Linia 430: @@
 </math>
-Spróbujmy! Oto nowa wersja jednej z reguł dla <math>\mathbf{let}\, x = e_1 \,\mathbf{in}\, e_2</math> dotycząca kroku wewnątrz <math>e_1</math>:
+Spróbujmy! Oto nowa wersja jednej z reguł dla <math>\mathbf{let}\, x = e_1 \,\mathbf{in}\, e_2</math>, dotycząca kroku wewnątrz <math>e_1</math>:
 <math>
@@ Linia 449: / Linia 448: @@
 Okazuje się, że wszystko jest w porządku. Wyrażenie <math>e</math> obliczamy w prawidłowym stanie, tzn. z wartością <math>n</math> przypisaną zmiennej <math>x</math>.
 Mały krok w <math>e</math> daje przyczynek do małego kroku w całym wyrażeniu, a przy tym stan pozostaje niezmieniony.
-Przy tym wogóle nie potrzebujemy przywracać poprzedniej wartości zmiennej <math>x</math>, ponieważ <math>x</math> zyskuje nową wartość ''tylko'' na potrzeby obliczania podwyrażenia <math>e</math>!
+Przy tym wogóle nie potrzebujemy przywracać poprzedniej wartości zmiennej <math>x</math>, ponieważ <math>x</math> zyskuje nową wartość "tylko" na potrzeby obliczania podwyrażenia <math>e</math>!
 Można na to również spojrzeć inaczej: informacja o nowej wartości <math>n</math>  dla zmiennej <math>x</math> nie jest jawnie dodawana do stanu <math>s</math>, ale jest przechowywana w składni wyrażenia <math>\mathbf{let}\, x = n \,\mathbf{in}\, \ldots</math> jako deklaracja <math>x = n</math>.
 Na końcu musimy oczywiście pozbyć się tej deklaracji za pomocą następującej tranzycji:
@@ Linia 458: / Linia 457: @@
 Podsumujmy. Okazuje się, że rozwiązanie nie było wcale łatwe, nawet dla tak prościutkiego języka. W przyszłości przekonamy się, że łatwiej jest poradzić sobie z zagadnieniem wiązania identyfikatorów w semantyce naturalnej (duże kroki).
-W wariancie 1 i 2 wprowadziliśmy do języka dodatkowe elementy, tak, by łatwiej było pisać reguły. W przyszłości będziemy czasem stosować takie podejście.
+W wariancie 1 i 2 wprowadziliśmy do języka dodatkowe elementy, tak by łatwiej było pisać reguły. W przyszłości będziemy czasem stosować takie podejście.
 Niekiedy jednak rozszerzanie języka będzie zabronione.

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

Wersja z 10:18, 27 wrz 2006

Zawartość

Semantyka operacyjna wyrażeń

Zadania domowe

Menu nawigacyjne

Działania na stronie

Opcje strony

Narzędzia osobiste

Nawigacja

Szukaj

Narzędzia