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

Wersja z 17:02, 27 lip 2006

Zawartość

Ćwiczymy dalej semantykę małych kroków. Uzupełnimy semantykę języka Tiny o semantykę operacyjną wyrażeń boolowskich i arytmetycznych. Następnie rozszerzymy nasz język o róznorodne konstrukcje iteracji. Na koniec zdefiniujemy operacje arytmetyczne liczb binarnych.

Rozszerzenia języka Tiny

Zadanie 1

Semantyka języka Tiny z wykładu używała funkcji semantycznych $B, E : S t a t e \to S t a t e$ dla określenie znaczenia wyrażeń boolowskich i arytmetycznych. Zdefiniuj znaczenie wyrażeń za pomocą semantyki operacyjnej, w stylu małych kroków.

Rozwiązanie

Przypomnijmy składnię wyrażeń boolowskich i arytmetycznych:

$b : : = t r u e | f a l s e | e_{1} \leq e_{2} | \neg b | b_{1} \land b_{2} | \dots$

$e : : = 0 | 1 | \dots | x | e_{1} + e_{2} | \dots$

Chcemy, aby tranzycje dla wyrażeń były postaci: $e, s ⟶ e^{'}, s$ i podobnie dla wyrażeń boolowskich: $b, s ⟶ b^{'}, s$ gdzie $s \in S t a t e$ .

Zacznijmy od wyrażeń boolowskich.

$t r u e, s ⟹ t r u e f a l s e, s ⟹ f a l s e$

Przejdźmy do spójników logicznych, powiedzmy $b_{1} \land b_{2}$ . Ponieważ opisujemy teraz pojedyncze (małe) kroki składające się na wykonanie programu, musimy podać w jakiej kolejności będą się obliczać $b_{1}$ i $b_{2}$ . Zacznijmy od strategii lewostronnej:

$\frac{b_{1}, s ⟹ b'_{1}, s}{b_{1} \land b_{2}, s ⟹ b'_{1} \land b_{2}, s} \frac{b_{2}, s ⟹ b'_{2}, s}{l_{1} \land b_{2}, s ⟹ l_{1} \land b_{2}, s} l_{1} \land l_{2} ⟹ l, o ile l = l_{1} \land l_{2}$

Możemy zaniechać obliczania $b_{2}$ jeśli $b_{1}$ oblicza się do false. Oto odpowiednio zmodyfikowane reguły:

$\frac{b_{1}, s ⟹ b'_{1}, s}{b_{1} \land b_{2}, s ⟹ b'_{1} \land b_{2}, s} f a l s e \land b_{2}, s ⟹ f a l s e t r u e \land b_{2}, s ⟹ b_{2}, s$

Analogicznie reguły prawostronne to:

$\frac{b_{2}, s ⟹ b'_{2}, s}{b_{1} \land b_{2}, s ⟹ b_{1} \land b'_{2}, s} b_{1} \land f a l s e, s ⟹ f a l s e b_{1} \land t r u e, s ⟹ b_{1}, s$

Reguły równoległe otrzymujemy jako sumę reguł lewo- i prawostronnych (w sumie 6 reguł). Zauważmy, że obliczanie wyrażeń $b_{1}$ i $b_{2}$ odbywa się teraz w twz. przeplocie: Pojedynczy krok polega na wykonaniu jednego kroku obliczenia $b_{1}$ albo jednego kroku obliczenia $b_{2}$ . Zwróćmy też uwagę, że nasze tranzycje nie posiadają teraz własności determinizmu: wyrażenie $b_{1} \land b_{2}$ może wyewoluować w pojedyńczym kroku albo do $b'_{1} \land b_{2}$ albo do $b_{1} \land b'_{2}$ . 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:

$\neg t r u e, s ⟹ f a l s e, s \neg f a l s e, s ⟹ t r u e, s \frac{b, s ⟹ b^{'}, s}{\neg b, s ⟹ \neg b^{'}, s}$

Reguły dla $e_{1} \leq e_{2}$ są następujące:

$\frac{e_{1}, s ⟹ e'_{1}, s}{e_{1} \leq e_{2}, s ⟹ e'_{1} \leq e_{2}, s} \frac{e_{2}, s ⟹ e'_{2}, s}{e_{1} \leq e_{2}, s ⟹ e_{1} \leq e'_{2}, s} n_{1} \leq n_{2}, s ⟹ t r u e, s o ile n_{1} \leq n_{2} n_{1} \leq n_{2}, s ⟹ f a l s e, s o ile n_{1} > n_{2}$

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:

$\frac{b, s ⟹ b^{'}, s}{𝐢 𝐟 b 𝐭 𝐡 𝐞 𝐧 I_{1} 𝐞 𝐥 𝐬 𝐞 I_{2}, s ⟹ 𝐢 𝐟 b^{'} 𝐭 𝐡 𝐞 𝐧 I_{1} 𝐞 𝐥 𝐬 𝐞 I_{2}, s} \frac{b, s ⟹ b^{'}, s}{𝐰 𝐡 𝐢 𝐥 𝐞 b 𝐝 𝐨 I, s ⟹ 𝐰 𝐡 𝐢 𝐥 𝐞 b^{'} 𝐝 𝐨 I, s}$

a gdy dozór jest już obliczony, podejmujemy decyzję. W przypadku instrukcji warunkowej reguły są oczywiste:

$𝐢 𝐟 t r u e 𝐭 𝐡 𝐞 𝐧 I_{1} 𝐞 𝐥 𝐬 𝐞 I_{2}, s ⟹ I_{1}, s 𝐢 𝐟 f a l s e 𝐭 𝐡 𝐞 𝐧 I_{1} 𝐞 𝐥 𝐬 𝐞 I_{2}, s ⟹ I_{2}, s$

Gorzej jest w przypadku instukcji pętli. Reguła mogłaby wyglądać tak:

$𝐰 𝐡 𝐢 𝐥 𝐞 t r u e 𝐝 𝐨 I, s ⟹ I; 𝐰 𝐡 𝐢 𝐥 𝐞 ? 𝐝 𝐨 I, s$

ale nie wiemy już, jaki był dozór pętli (widzimy tylko wynik obliczenia tego dozoru w stanie s, czyli $𝐭 𝐫 𝐮 𝐞$ ). Możemy odwołać się do tranzytywnego domknięcia relacji $⟹$ (czyli w zadadzie do semantyki dużych kroków):

$\frac{b, s ⟹^{*} t r u e}{𝐰 𝐡 𝐢 𝐥 𝐞 b 𝐝 𝐨 I, s ⟹ I; 𝐰 𝐡 𝐢 𝐥 𝐞 b 𝐝 𝐨 I, s} \frac{b, s ⟹^{*} f a l s e}{𝐰 𝐡 𝐢 𝐥 𝐞 b 𝐝 𝐨 I, s ⟹ s}$

Takie rozwiązanie nie jest zatem czystą semantyką małych kroków. Istnieją inne możliwe rozwiązania, w stylu małych kroków, np. przy użyciu rozszerzonej składni. Znalezienie takiego rozwiązania pozostawiamy dociekliwemu czytelnikowi.

Reguły dla operacji arytmetycznych pozostawiamy do napisania Czytelnikowi.

Zadanie 2

Rozszerzmy język Tiny o następujące dobrze znane konstrukcje iteracji:

$I : : = 𝐫 𝐞 𝐩 𝐞 𝐚 𝐭 I 𝐮 𝐧 𝐭 𝐢 𝐥 b | 𝐅 𝐎 𝐑 x : = e_{1} 𝐭 𝐨 e_{2} 𝐝 𝐨 I | 𝐝 𝐨 I e 𝐭 𝐢 𝐦 𝐞 𝐬 | 𝐝 𝐨 I 𝐰 𝐡 𝐢 𝐥 𝐞 b$

Napisz semantykę małych kroków dla powyższych konstrukcji. Niedozwolone jest korzystanie z jakiejś konstrukcji w semantyce innej, np.

$𝐝 𝐨 I 𝐰 𝐡 𝐢 𝐥 𝐞 b ⟹ 𝐫 𝐞 𝐩 𝐞 𝐚 𝐭 I 𝐮 𝐧 𝐭 𝐢 𝐥 \neg b$

Rozwiązanie

.....

Kalkulator binarny

Zadanie 1

Rozważmy następujący język wyrażeń (liczby binarne z dodawaniem):

$e : : = ϵ | e 0 | e 1 | e_{1} + e_{2}$

$ϵ$ oznacza słowo puste, czyli np. $ϵ 101$ oznacza binarną liczbę 101. Napisz semantykę operacyjną obliczającą wartość wyrażeń.

Rozwiązanie

Składnia wyrażeń pozwala na wygodny dostęp do najmniej znaczącego bitu liczby. Spróbujmy zatem zastosować metodę dodawania pisemnego:

$e_{1} 0 + e_{2} 0 ⟹ (e_{1} + e_{2}) 0$

$e_{1} 0 + e_{2} 1 ⟹ (e_{1} + e_{2}) 1$

$e_{1} 1 + e_{2} 0 ⟹ (e_{1} + e_{2}) 1$

Ale co zrobić z przeniesieniem?

$e_{1} 1 + e_{2} 1 ⟹ ?$

Podstawowy pomysł polega na potraktowaniu przeniesienia jak dodatkowego składnika:

$e_{1} 1 + e_{2} 1 ⟹ ((e_{1} + e_{2}) + ϵ 1) 0$

Zauważmy, że w składni dopuszcza się dowolne przeplatanie operatora dodawania i bitów $0, 1$ . Tę dowolność wykorzystaliśmy właśnie w regułach powyżej. Gdyby nasz język ograniczyć tylko do składni

$e : : = b | e_{1} + e_{2}$

$b : : = ϵ | b 0 | b 1$

(nazwijmy ją składnią ograniczoną) to powyższe reguły byłyby niepoprawne.

Zanim dopiszemy pozostałe reguły, określmy zbiór konfiguracji jako zbiór wyrażeń. Konfiguracje końcowe to wyrażenia bez operatora dodawania (liczby binarne). Nasz pomysł jest taki, że tranzycje stopniowo przesuwają operator dodawania w lewo, aż się go ostatecznie pozbędą.

Gdy jeden ze składników ma mniej cyfr niż drugi, potrzebujemy reguł:

$ϵ + e 0 ⟹ e 0 ϵ + e 1 ⟹ e 1$

oraz ich odpowiedników:

$e 0 + ϵ ⟹ e 0 e 1 + ϵ ⟹ e 1 .$

Niestety, nie możemy użyć reguły przemienności:

$e_{1} + e_{2} ⟹ e_{2} + e_{1}$

gdyż spowodowałaby ona możliwość pętlenia się, a zatem braku wyniku obliczania wyrażenie.

Na koniec dodajemy typowe reguły opisujące jak krok podwyrażenia daje krok całęgo wyrażenia:

$\frac{e_{1} ⟹ e'_{1}}{e_{1} + e_{2} ⟹ e'_{1} + e_{2}} \frac{e_{2} ⟹ e'_{2}}{e_{1} + e_{2} ⟹ e_{1} + e'_{2}} \frac{e ⟹ e^{'}}{e 0 ⟹ e^{'} 0} \frac{e ⟹ e^{'}}{e 1 ⟹ e^{'} 1}$

Zadanie 2

Rozszerzmy składnię o jeden symbol $p$ oznaczający przepełnienie: $e : : = ϵ | p | e 0 | e 1 | e_{1} + e_{2}$ Na przykład $p 101$ oznacza tę samą liczbę co $ϵ 101$ , ale z dodatkową informacją, że podczas jej obliczania nastąpiło przepełnienie. Rozumiemy przez to sytuację, gdy wynik ma więcej cyfr niż każdy z argumentów. Cyfry zero z lewej strony (najbardziej znaczące) również uważamy za pełnoprawne cyfry, nie należy ich usuwać ani dodawać nowych.

Napisz semantykę operacyjną obliczającą wyrażenie wraz z informacja o ewentualnym przepełnieniu. Wynik powinien byc poprawny przynajmniej dal wyrażeń w składni ograniczonej.

Rozwiązanie

Zadanie dotyczy w zasadzie składni ograniczonej, ale jako konfiguracji pośrednich będziemy zapewne potrzebować wyrażeń wykraczających poza tę składnię, np. $(e_{1} + e_{2}) 0$ , podobnie jak w poprzednim zadaniu. Zatem mamy tu do czynienia z typowym zabiegiem rozszerzania składni na użytek semantyki operacyjnej (z tym, że rozszerzenie jest dane z góry i nie musimy go wymyślać :)

Przyjmijmy, że konfiguracjami są dowolne wyrażenia, a konfiguracjami końcowymi wyrażenia bez operatora dodawania (ale teraz mogą to być np. wyrażenia postaci $p 100$ ). Spróbujmy pozostawić wszystkie reguły z poprzedniego zadania. Dodamy tylko kilka nowych reguł, odpowiedzialnych za przepełnienie.

Zacznijmy od najprostszej sytuacji, gdy jeden ze składników ma mniej cyfr, i to ten właśnie składnik odnotował przepełnienie:

$p + e 0 ⟹ e 0 p + e 1 ⟹ e 1 e 0 + p ⟹ e 0 e 1 + p ⟹ e 1$

W takiej sytuacji oczywiście informacja o przepełnieniu zostaje wymazana. Jeśli przepełnienie zostało odnotowane w składniku o większej liczbie cyfr, to reguły

$ϵ + e 0 ⟹ e 0 ϵ + e 1 ⟹ e 1 e 0 + ϵ ⟹ e 0 e 1 + ϵ ⟹ e 1 .$

z poprzedniego zadania są wystarczające.

Rozważmy teraz przypadek, gdy obydwa składniki mają tę samą liczbę cyfr. Jeśli obydwa odnotowały przepełnienie, to oczywiście informacja ta powinna zostać zachowana:

$p + p ⟹ p$

Ale co należy zrobić, gdy tylko jeden ze składników odnotował przepełnienie? $p + ϵ ⟹ ?$ Oczywiście, w tej sytuacji żadnego przepełnienia nie ma, ponieważ drugi składnik ma wystarczająco dużo cyfr by je przesłonić. Oto odpowiednie reguły:

$p + ϵ ⟹ ϵ ϵ + p ⟹ ϵ$

Na koniec zostało najważniejsze: kiedy powinniśmy generować sygnał o przepełnieniu? Przypomnijmy sobie reguły dla dadawania pisemnego w poprzednim zadaniu. Jeśli nie ma przeniesienia, to przepełnienie nie może powstać. Natomiast jeśli jest przeniesienie, to stanowi ono potencjalne przepełnienie. Odpowiednia reguła to

$e_{1} 1 + e_{2} 1 ⟹ ((e_{1} + e_{2}) + p 1) 0 .$

Nowy sztuczny składnik $p 1$ zawiera jakby na wszelki wypadek informacje o potencjalnym przepełnieniu. Jeśli którykolwiek z pozostałych składników $e_{1}$ i $e_{2}$ ma przynajmniej jedną cyfrę, to $p$ zostanie usunięte. W przeciwnym wypadku symbol $p$ i przetrwa i będzie poprawnie informował o sytuacji przepełnienia.

Zadania domowe

Zadanie 1

Podaj przykład wyrażenia, które nie policzy się ani przy użyciu strategii lewo- ani prawostronnej, a policzy się przy strategii równoległej.

Zadanie 2

Dodaj do wyrażeń binarnych operację odejmowania.

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

Wersja z 17:02, 27 lip 2006

Spis treści

Zawartość

Rozszerzenia języka Tiny

Zadanie 1

Rozwiązanie

Zadanie 2

Rozwiązanie

Kalkulator binarny

Zadanie 1

Rozwiązanie

Zadanie 2

Rozwiązanie

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: @@
-== Ćwiczenia 2: Rozszerzenie języka Tiny (małe kroki) ==
+== Zawartość ==
-== Zadania z rozwiązaniami ==
+Ćwiczymy dalej semantykę małych kroków.
+Uzupełnimy semantykę języka Tiny o semantykę operacyjną
+wyrażeń boolowskich i arytmetycznych.
+Następnie rozszerzymy nasz język o róznorodne konstrukcje iteracji.
+Na koniec zdefiniujemy operacje arytmetyczne liczb binarnych.
+== Rozszerzenia języka Tiny ==
 ==== Zadanie 1 ====
 Semantyka języka Tiny z wykładu używała funkcji semantycznych
 <math>
@@ Linia 155: / Linia 163: @@
 <math>
 \mathbf{if}\, true\, \mathbf{then}\, I_1\, \mathbf{else}\, I_2, s \Longrightarrow I_1, s
-\quad \quad \quad
+\quad \quad
 \mathbf{if}\, false\, \mathbf{then}\, I_1\, \mathbf{else}\, I_2, s \Longrightarrow I_2, s
 </math>
@@ Linia 175: / Linia 183: @@
 {\mathbf{while}\, b\, \mathbf{do}\, I, s \Longrightarrow
   I;\, \mathbf{while}\, b\, \mathbf{do}\, I, s}
-\quad \quad \quad
+\quad \quad
 \frac{b, s \,\Longrightarrow\,^{*} false}
 {\mathbf{while}\, b\, \mathbf{do}\, I, s \Longrightarrow s}
@@ Linia 196: / Linia 204: @@
 I \, ::= \,\,
          \mathbf{repeat}\, I \,\mathbf{until}\, b  \,\,|\,\,
-         FOR x := e_1 \,\mathbf{to}\, e_2 \,\mathbf{do}\, I  \,\,|\,\,
+         \mathbf{FOR}\, x := e_1 \,\mathbf{to}\, e_2 \,\mathbf{do}\, I  \,\,|\,\,
          \,\mathbf{do}\, I e \,\mathbf{times}  \,\,|\,\,
-         \,\mathbf{do}\, I \mathbf{while}\, b
+         \,\mathbf{do}\, I \,\mathbf{while}\, b
 </math>
@@ Linia 206: / Linia 214: @@
 <math>
-\,\mathbf{do}\, I \mathbf{while}\, b \,\Longrightarrow\, \mathbf{repeat}\, I \,\mathbf{until}\, \neg b
+\,\mathbf{do}\, I \,\mathbf{while}\, b \,\Longrightarrow\, \mathbf{repeat}\, I \,\mathbf{until}\, \neg b
+</math>
+==== Rozwiązanie ====
+.....
+== Kalkulator binarny ==
+==== Zadanie 1 ====
+Rozważmy następujący język wyrażeń (liczby binarne z dodawaniem):
+<math>
+e \, ::= \,\,
+      \epsilon  \,\,|\,\,
+      e 0  \,\,|\,\,
+      e 1  \,\,|\,\,
+      e_1 + e_2
 </math>
+<math> \epsilon </math> oznacza słowo puste, czyli np. <math> \epsilon 1 0 1 </math>
+oznacza binarną liczbę 101.
+Napisz semantykę operacyjną obliczającą wartość wyrażeń.
 ==== Rozwiązanie ====
+Składnia wyrażeń pozwala na wygodny dostęp do najmniej znaczącego
+bitu liczby. Spróbujmy zatem zastosować metodę dodawania
+pisemnego:
+<math>
+e_1 0 + e_2 0 \,\Longrightarrow\, (e_1 + e_2) 0
+</math>
+<math>
+e_1 0 + e_2 1 \,\Longrightarrow\, (e_1 + e_2) 1
+</math>
+<math>
+e_1 1 + e_2 0 \,\Longrightarrow\, (e_1 + e_2) 1
+</math>
+Ale co zrobić z przeniesieniem?
+<math>
+e_1 1 + e_2 1 \,\Longrightarrow\, ?
+</math>
+Podstawowy pomysł polega na potraktowaniu przeniesienia jak dodatkowego składnika:
+<math>
+e_1 1 + e_2 1 \,\Longrightarrow\, ((e_1 + e_2) + \epsilon 1) 0
+</math>
+Zauważmy, że w składni dopuszcza się dowolne przeplatanie operatora dodawania
+i bitów <math> 0, 1 </math>. Tę dowolność wykorzystaliśmy właśnie w regułach
+powyżej. Gdyby nasz język ograniczyć tylko do składni
+<math>
+e \, ::= \,\,
+      b  \,\,|\,\,
+      e_1 + e_2
+</math>
+<math>
+b \, ::= \,\,
+      \epsilon  \,\,|\,\,
+      b 0  \,\,|\,\,
+      b 1
+</math>
+(nazwijmy ją ''składnią ograniczoną'') to powyższe reguły byłyby niepoprawne.
+Zanim dopiszemy pozostałe reguły, określmy zbiór konfiguracji jako
+zbiór wyrażeń. Konfiguracje końcowe to wyrażenia bez operatora dodawania
+(liczby binarne). Nasz pomysł jest taki, że tranzycje stopniowo przesuwają
+operator dodawania w lewo, aż się go ostatecznie ''pozbędą''.
+Gdy jeden ze składników ma mniej cyfr niż drugi, potrzebujemy reguł:
+<math>
+\epsilon + e 0 \,\Longrightarrow\, e 0
+\quad \quad
+\epsilon + e 1 \,\Longrightarrow\, e 1
+</math>
+oraz ich odpowiedników:
+<math>
+e 0 + \epsilon \,\Longrightarrow\, e 0
+\quad \quad
+e 1 + \epsilon \,\Longrightarrow\, e 1.
+</math>
+Niestety, nie możemy użyć reguły przemienności:
+<math>
+e_1 + e_2 \,\Longrightarrow\, e_2 + e_1
+</math>
-==== Zadanie 3 ====
+gdyż spowodowałaby ona możliwość ''pętlenia się'', a zatem braku wyniku obliczania wyrażenie.
-Rozszerz język Tiny o następującą instrukcję pętli:
+Na koniec dodajemy typowe reguły opisujące jak krok podwyrażenia daje
+krok całęgo wyrażenia:
 <math>
-I \, ::= \,\,
+\frac{e_1 \,\Longrightarrow\, e'_1}
-       LOOP I \,\,|\,\,
+     {e_1 + e_2 \,\Longrightarrow\, e'_1 + e_2}
-       EXIT \,\,|\,\,
+\quad \quad
-       CONT\,\mathbf{in}\,UE
+\frac{e_2 \,\Longrightarrow\, e'_2}
+     {e_1 + e_2 \,\Longrightarrow\, e_1 + e'_2}
+\quad \quad
+\frac{e \,\Longrightarrow\, e'}
+     {e 0 \,\Longrightarrow\, e' 0}
+\quad \quad
+\frac{e \,\Longrightarrow\, e'}
+     {e 1 \,\Longrightarrow\, e' 1}
+\quad \quad
 </math>
-<math> LOOP I </math> to instrukcja pętli, <math> I </math> stanowi instrukcję wewnętrzną.
-Instrukcja <math> EXIT </math> wychodzi z nabliższej pętli <math> LOOP </math>
-i kontynuuje wykonanie programu od pierwszej instrukcji za tą pętlą.
-Instrukcje <math> CONT\,\mathbf{in}\,UE </math> powraca na początek instrukcji wewnętrznej.
+==== Zadanie 2 ====
+Rozszerzmy składnię o jeden symbol <math> p </math> oznaczający
+''przepełnienie'':
+<math>
+e \, ::= \,\,
+      \epsilon  \,\,|\,\,
+      p  \,\,|\,\,
+      e 0  \,\,|\,\,
+      e 1  \,\,|\,\,
+      e_1 + e_2
+</math>
+Na przykład <math> p 1 0 1 </math> oznacza tę samą liczbę co <math> \epsilon 1 0 1
+</math>, ale z dodatkową informacją, że podczas jej obliczania nastąpiło
+''przepełnienie''.
+Rozumiemy przez to sytuację, gdy wynik ma więcej cyfr niż każdy z
+argumentów. Cyfry zero z lewej strony (najbardziej znaczące) również
+uważamy za pełnoprawne cyfry, nie należy ich usuwać ani dodawać nowych.
+Napisz semantykę operacyjną obliczającą wyrażenie wraz z
+informacja o ewentualnym przepełnieniu.
+Wynik powinien byc poprawny przynajmniej dal wyrażeń w składni
+ograniczonej.
 ==== Rozwiązanie ====
+Zadanie dotyczy w zasadzie składni ograniczonej, ale jako konfiguracji
+pośrednich będziemy zapewne potrzebować wyrażeń wykraczających poza
+tę składnię, np. <math> (e_1 + e_2) 0 </math>, podobnie jak w poprzednim
+zadaniu. Zatem mamy tu do czynienia z typowym zabiegiem rozszerzania
+składni na użytek semantyki operacyjnej (z tym, że rozszerzenie jest
+dane z góry i nie musimy go wymyślać :)
+Przyjmijmy, że konfiguracjami są dowolne wyrażenia, a konfiguracjami
+końcowymi wyrażenia bez operatora dodawania (ale teraz mogą to być
+np. wyrażenia postaci <math> p 1 0 0 </math>).
+Spróbujmy pozostawić wszystkie reguły z poprzedniego zadania.
+Dodamy tylko kilka nowych reguł, odpowiedzialnych za przepełnienie.
+Zacznijmy od najprostszej sytuacji, gdy jeden ze składników ma mniej
+cyfr, i to ten właśnie składnik odnotował przepełnienie:
+<math>
+p + e 0 \,\Longrightarrow\, e 0
+\quad \quad
+p + e 1 \,\Longrightarrow\, e 1
+\quad \quad
+e 0 + p \,\Longrightarrow\, e 0
+\quad \quad
+e 1 + p \,\Longrightarrow\, e 1
+</math>
+W takiej sytuacji oczywiście informacja o przepełnieniu zostaje
+wymazana.
+Jeśli przepełnienie zostało odnotowane w składniku o większej liczbie
+cyfr, to reguły
+<math>
+\epsilon + e 0 \,\Longrightarrow\, e 0
+\quad \quad
+\epsilon + e 1 \,\Longrightarrow\, e 1
+\quad \quad
+e 0 + \epsilon \,\Longrightarrow\, e 0
+\quad \quad
+e 1 + \epsilon \,\Longrightarrow\, e 1.
+</math>
+z poprzedniego zadania są wystarczające.
+Rozważmy teraz przypadek, gdy obydwa składniki mają tę samą liczbę
+cyfr.
+Jeśli obydwa odnotowały przepełnienie, to oczywiście informacja ta
+powinna zostać zachowana:
+<math>
+p + p \,\Longrightarrow\, p
+</math>
+Ale co należy zrobić, gdy tylko jeden ze składników odnotował
+przepełnienie? <math> p + \epsilon \,\Longrightarrow\, ? </math>
+Oczywiście, w tej sytuacji żadnego przepełnienia nie ma, ponieważ
+drugi składnik ma wystarczająco dużo cyfr by je przesłonić.
+Oto odpowiednie reguły:
+<math>
+p + \epsilon \,\Longrightarrow\, \epsilon
+\quad \quad
+\epsilon + p \,\Longrightarrow\, \epsilon
+</math>
+Na koniec zostało najważniejsze: kiedy powinniśmy generować sygnał o
+przepełnieniu?
+Przypomnijmy sobie reguły dla dadawania pisemnego w poprzednim
+zadaniu.
+Jeśli nie ma przeniesienia, to przepełnienie nie może powstać.
+Natomiast jeśli jest przeniesienie, to stanowi ono ''potencjalne
+przepełnienie''.
+Odpowiednia reguła to
+<math>
+e_1 1 + e_2 1 \,\Longrightarrow\, ((e_1 + e_2) + p 1) 0.
+</math>
+Nowy sztuczny składnik <math> p 1 </math> zawiera jakby na wszelki wypadek
+informacje o potencjalnym przepełnieniu.
+Jeśli którykolwiek z pozostałych składników  <math> e_1 </math> i <math> e_2 </math>
+ma przynajmniej jedną cyfrę,
+to <math> p </math> zostanie usunięte. W przeciwnym wypadku symbol <math> p </math>
+i przetrwa i będzie poprawnie informował o sytuacji przepełnienia.
 == Zadania domowe ==
+==== Zadanie 1 ====
+Podaj przykład wyrażenia, które nie policzy się
+ani przy użyciu strategii lewo- ani prawostronnej, a policzy się przy strategii
+równoległej.
+==== Zadanie 2 ====
+Dodaj do wyrażeń binarnych operację odejmowania.