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

Wersja z 08:24, 11 sie 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 semantyki języka Tiny

Ćwiczenie 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ślenia znaczenia wyrażeń boolowskich i arytmetycznych. Zdefiniuj znaczenie wyrażeń za pomocą semantyki operacyjnej, w stylu małych kroków.

Rozwiązanie

{{{3}}}

Ćwiczenie 2

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

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

Napisz semantykę małych kroków dla powyższych konstrukcji.

Rozwiązanie

{{{3}}}

Kalkulator binarny

Ćwiczenie 3

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. $ϵ 1011$ oznacza binarną liczbę 1011. Napisz semantykę operacyjną obliczającą wartość wyrażeń.

Rozwiązanie

{{{3}}}

Ćwiczenie 4

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ą wartość wyrażenia wraz z informacja o ewentualnym przepełnieniu. Wynik powinien byc poprawny przynajmniej dla wyrażeń $e$ w składni ograniczonej:

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

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

reprezentujących sumę liczb binarnych.

Rozwiązanie

{{{3}}}

Zadania domowe

Ćwiczenie 1

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

Ćwiczenie 2

Zmodyfikuj semantykę wyrażeń następująco: dla każdego podwyrażenia niedeterministycznie wybierana jest albo strategia lewo- albo prawostronna, ale niedozwolony jest ,,przeplot".

Ćwiczenie 3

Rozważ inną semantykę pętli $𝐟 𝐨 𝐫 x = e_{1} 𝐭 𝐨 e_{2} 𝐝 𝐨 I$ , w której wyrażenie $e_{2}$ jest obliczane na nowo przed każdą iteracją pętli.

Ćwiczenie 4

Dodaj do wyrażeń binarnych operację odejmowania.

Ćwiczenie 5

Zaproponuj semantykę przypisania równoległego w języku Tiny:

$x_{1} : = e_{1} | | \dots | | x_{n} : = e_{n}$

polegającego na obliczeniu najpierw wartości wyrażeń $e_{1}, \dots, e_{n}$ a następnie na podstawieniu tych wartości na zmienne $x_{1}, \dots, x_{n}$ .

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

Wersja z 08:24, 11 sie 2006

Spis treści

Zawartość

Rozszerzenia semantyki języka Tiny

Kalkulator binarny

Zadania domowe

Menu nawigacyjne

Działania na stronie

Opcje strony

Narzędzia osobiste

Nawigacja

Szukaj

Narzędzia

@@ Linia 4: / Linia 4: @@
 Ćwiczymy dalej semantykę małych kroków.
-Uzupełnimy semantykę języka Tiny o semantykę operacyjną
+Uzupełnimy semantykę języka Tiny o semantykę operacyjną wyrażeń boolowskich i arytmetycznych.
-wyrażeń boolowskich i arytmetycznych.
 Następnie rozszerzymy nasz język o róznorodne konstrukcje iteracji.
 Na koniec zdefiniujemy operacje arytmetyczne liczb binarnych.
@@ Linia 20: / Linia 19: @@
 </math>
 dla określenia znaczenia wyrażeń boolowskich i arytmetycznych.
-Zdefiniuj znaczenie wyrażeń za pomocą semantyki operacyjnej,
+Zdefiniuj znaczenie wyrażeń za pomocą semantyki operacyjnej, w stylu małych kroków.
-w stylu małych kroków.
 }}
@@ Linia 60: / Linia 58: @@
 </math>
-Niech <math>\mathbf{BExp}</math>  oznacza zbiór wyrażeń boolowskich,
+Niech <math>\mathbf{BExp}</math>  oznacza zbiór wyrażeń boolowskich, <math>b \in \mathbf{BExp}</math>.
-<math>b \in \mathbf{BExp}</math>.
 Chcemy, aby tranzycje dla wyrażeń były postaci:
@@ Linia 84: / Linia 81: @@
 b, s \,\Longrightarrow\, l
 </math>
-gdzie <math>n \in</math> jest liczbą całkowitą,
+gdzie <math>n \in</math> jest liczbą całkowitą, <math>n \in \mathbf{Num}</math>, a <math>l \in \mathbf{Bool} = \{ \mathbf{true}, \mathbf{false} \}</math>.
-<math>n \in \mathbf{Num}</math>, a <math>l \in \mathbf{Bool} = \{ \mathbf{true}, \mathbf{false} \}</math>.
 Formalnie, zbiór konfiguracji dla semantyki całego języka Tiny to
@@ Linia 93: / Linia 89: @@
 </math>
-a konfiguracje końcowe to <math>\mathbf{State}</math>; aczkolwiek
+a konfiguracje końcowe to <math>\mathbf{State}</math>; aczkolwiek konfiguracje ze zbioru <math>\mathbf{Num} \, \cup \, \mathbf{Bool}</math> pełnią podobną rolę dla wyrażeń arytmetycznych i boolowskich jako konfiguracje końcowe dla instrukcji.
-konfiguracje ze zbioru <math>\mathbf{Num} \, \cup \, \mathbf{Bool}</math> pełnią podobną rolę
-dla wyrażeń arytmetycznych i boolowskich jako konfiguracje końcowe dla
-instrukcji.
 Przypomnijmy, że <math>\mathbf{Stmt}</math>  oznacza zbiór instrukcji, <math>I \in \mathbf{Stmt}</math>.
@@ Linia 107: / Linia 100: @@
 </math>
-Podobnie jak poprzednio, zakładamy tutaj dla wygody, że
+Podobnie jak poprzednio, zakładamy tutaj dla wygody, że <math>\mathbf{Num} \subseteq \mathbf{Exp}</math> oraz <math>\mathbf{Bool} \subseteq \mathbf{BExp}</math>.
-<math>\mathbf{Num} \subseteq \mathbf{Exp}</math> oraz <math>\mathbf{Bool} \subseteq \mathbf{BExp}</math>.
+Pozwala nam to nie odróżniać stałych występujących w wyrażeniach a zatem pojawiających się po lewej stonie tranzycji od wartości im odpowiadających pojawiających się po prawej stronie.
-Pozwala nam to nie odróżniać stałych występujących w wyrażeniach
-a zatem pojawiających się po lewej stonie tranzycji
-od wartości im odpowiadających pojawiających się po prawej stronie.
 Przejdźmy do spójników logicznych, powiedzmy <math>b_1 \land b_2</math>.
-Ponieważ opisujemy teraz pojedyncze (małe) kroki składające się na
+Ponieważ opisujemy teraz pojedyncze (małe) kroki składające się na wykonanie programu, musimy podać w jakiej kolejności będą się obliczać <math>b_1</math> i <math>b_2</math>. Zacznijmy od strategii lewostronnej:
-wykonanie programu, musimy podać w jakiej kolejności będą się
-obliczać <math>b_1</math> i <math>b_2</math>. Zacznijmy od strategii lewostronnej:
 <math>
@@ Linia 129: / Linia 117: @@
 </math>
-Możemy zaniechać obliczania
+Możemy zaniechać obliczania <math>b_2</math> jeśli <math>b_1</math> oblicza się do false.
-<math>b_2</math> jeśli <math>b_1</math> oblicza się do false.
 Oto odpowiednio zmodyfikowane reguły:
@@ Linia 139: / Linia 126: @@
 \mathbf{false} \land b_2, s \,\Longrightarrow\, \mathbf{false}, s
 \quad \quad
-\mathbf{true}  \land b_2, s \,\Longrightarrow\, b_2, s
+\mathbf{true}  \land b_2, s \,\Longrightarrow\, b_2, s.
 </math>
@@ Linia 150: / Linia 137: @@
 b_1 \land \mathbf{false}, s \,\Longrightarrow\, \mathbf{false}, s
 \quad \quad
-b_1 \land \mathbf{true}, s \,\Longrightarrow\, b_1, s
+b_1 \land \mathbf{true}, s \,\Longrightarrow\, b_1, s.
 </math>
-Reguły ''równoległe'' otrzymujemy jako sumę reguł lewo- i
+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 tzw. ,,przeplocie": Pojedynczy krok polega na wykonaniu jednego kroku obliczenia <math>b_1</math> albo jednego kroku obliczenia <math>b_2</math>.
-prawostronnych (w sumie 6 reguł). Zauważmy, że obliczanie
+Zwróćmy też uwagę, że nasze tranzycje nie posiadają teraz 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>.
-wyrażeń <math>b_1</math> i <math>b_2</math> odbywa się teraz
+Na szczęście końcowy wynik, do jakiego oblicza się wyrażenie jest zawsze taki sam, niezależnie od przeplotu.
-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 nasze tranzycje nie posiadają teraz
-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ły dla negacji:
@@ Linia 185: / Linia 163: @@
 \frac{e_2, s \,\Longrightarrow\, e'_2, s}
 {e_1 \leq e_2, s \,\Longrightarrow\, e_1 \leq e'_2, s}
+</math>
+<math>
+n_1 \leq n_2, s \,\Longrightarrow\, \mathbf{true}, s   \quad \mbox{ o ile } n_1 \leq n_2
 \quad \quad
-n_1 \leq n_2, s \,\Longrightarrow\, \mathbf{true}, s   \quad \mbox{ o ile }
+n_1 \leq n_2, s \,\Longrightarrow\, \mathbf{false}, s  \quad  \mbox{ o ile } n_1 > n_2.
-n_1 \leq n_2
-\quad \quad
-n_1 \leq n_2, s \,\Longrightarrow\, \mathbf{false}, s  \quad  \mbox{ o ile }
-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
+Zauważmy, że ponownie pozostawiliśmy dowolność jeśli chodzi o kolejność obliczania wyrażeń arytmetycznych <math>e_1</math> i <math>e_2</math>.
-kolejność obliczania wyrażeń arytmetycznych <math>e_1</math> i <math>e_2</math>.
 Jako pierwszą z instrukcji rozważmy przypisanie.
-Najpierw obliczamy wyrażenie po prawej stronie przypisania,
+Najpierw obliczamy wyrażenie po prawej stronie przypisania, a gdy wyrażenie to wyewoluuje do stałej (obliczy się), modyfikujemy stan:
-a gdy wyrażenie to wyewoluuje do stałej (obliczy się), modyfikujemy
-stan:
 <math>
@@ Linia 237: / Linia 212: @@
 </math>
-ale nie wiemy już, jaki był dozór pętli (widzimy tylko wynik
+ale nie wiemy już, jaki był dozór pętli (widzimy tylko wynik obliczenia tego dozoru w stanie s, czyli <math>\mathbf{true}</math>).
-obliczenia tego dozoru w stanie s, czyli <math>\mathbf{true}</math>).
+Możemy odwołać się do tranzytywnego domknięcia relacji <math>\,\Longrightarrow\,</math> (czyli w zasadzie do semantyki dużych kroków):
-Możemy odwołać się do tranzytywnego domknięcia relacji
-<math>\,\Longrightarrow\,</math> (czyli w zadadzie do semantyki dużych kroków):
 <math>
@@ Linia 251: / Linia 224: @@
 </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.
-Jedno z nich oparte jest na pomyśle, aby ''rozwinąc'' pętlę
+Jedno z nich oparte jest na pomyśle, aby ''rozwinąc'' pętlę <math>\mathbf{while}\,</math>, zanim obliczymy wartość dozoru <math>b</math>.
-<math>\mathbf{while}\,</math>, zanim obliczymy wartość dozoru <math>b</math>.
 Jedyną reguła dla pętli <math>\mathbf{while}\,</math> byłaby wtedy reguła:
@@ Linia 262: / Linia 232: @@
 </math>
-Dzięki temu obliczany warunek logiczny <math>b</math> jest zawsze
+Dzięki temu obliczany warunek logiczny <math>b</math> jest zawsze ''jednorazowy''.
-''jednorazowy''.
+Znalezienie innych rozwiązań, np. opartych na rozszerzeniu składni, pozostawiamy dociekliwemu Czytelnikowi.
-Znalezienie innych rozwiązań, np. opartych na rozszerzeniu składni,
-pozostawiamy dociekliwemu Czytelnikowi.
 Reguły dla operacji arytmetycznych również pozostawiamy do napisania Czytelnikowi.
@@ Linia 297: / Linia 265: @@
 Zacznijmy od pętli <math>\mathbf{repeat}\, I \,\mathbf{until}\, b</math>.
-Przyjrzyjmy się dwóm podejściom, które zastosowaliśmy dla
+Przyjrzyjmy się dwóm podejściom, które zastosowaliśmy dla pętli <math>\mathbf{while}\,</math> w poprzednim zadaniu.
-pętli <math>\mathbf{while}\,</math> w poprzednim zadaniu.
 Po pierwsze rozwinięcie:
@@ Linia 320: / Linia 287: @@
 </math>
-Okazuje się, że jest jeszcze gorzej niż w przypadku pętli <math>\mathbf{while}\,</math>:
+Okazuje się, że jest jeszcze gorzej niż w przypadku pętli <math>\mathbf{while}\,</math>: nie pamiętamy już, jaka była instrukcja wewnętrzna naszej pętli!
-nie pamiętamy już, jaka była instrukcja wewnętrzna naszej pętli!
 Czyli takie podejście jest teraz nieskuteczne.
 <br>
@@ Linia 329: / Linia 294: @@
 <br>
-Pętla <math>\,\mathbf{do}\, e \,\mathbf{times}\, I</math>, w stanie <math>s</math>, oznacza wykonianie instrukcji <math>I</math>
+Pętla <math>\,\mathbf{do}\, e \,\mathbf{times}\, I</math>, w stanie <math>s</math>, oznacza wykonanie instrukcji <math>I</math> <math>n</math> razy, gdzie <math>n</math> to wartość, do której oblicza się <math>e</math> w stanie <math>s</math>.
-<math>n</math> razy, gdzie <math>n</math> to wartość, do której oblicza się
-<math>e</math> w stanie <math>s</math>.
 Czyli najpierw obliczmy <math>e</math> przy pomocy reguły:
@@ Linia 356: / Linia 319: @@
 \quad \mbox{ o ile } n = 0.
 </math>
 <br>
@@ Linia 362: / Linia 324: @@
 <br>
-W przypadku pętli <math>\mathbf{for}\,</math> przyjmijmy, że wartości wyrażeń
+W przypadku pętli <math>\mathbf{for}\,</math> przyjmijmy, że wartości wyrażeń <math>e_1</math> i <math>e_2</math> obliczane są przed pierwszą iteracją pętli.
-<math>e_1</math> i <math>e_2</math> obliczane są przed pierwszą iteracją
+Dodatkowo ustalmy, że np. <math>e_1</math> będzie obliczone jako pierwsze.
-pętli.
+Następnie podstawiamy wartość <math>e_1</math> na zmienną <math>x</math>.
-Dodatkowo ustalmy, że <math>e_1</math> będzie obliczone jako pierwsze.
 Czyli:
@@ Linia 378: / Linia 339: @@
 </math>
-Zatem zakres zmiennej <math>x</math> mamy już obliczony, tzn. jesteśmy
+Zatem zakres zmiennej <math>x</math> mamy już obliczony, tzn. jesteśmy w konfiguracji
-w konfiguracji
 <math>
@@ Linia 397: / Linia 357: @@
 </math>
+Zauważmy, wartość zmiennej <math>x</math> po zakończeniu pętli wynosi albo <math>n_2</math> albo pozostaje niezmieniona, o ile nie była ona zmieniana wewnątrz instrukcji <math>I</math>.
+Ponieważ nie zostało wyspecyfikowane jaka powinna być wartość tej zmiennej, możemy taką semantykę uznać za poprawną.
-Zauważmy, wartość zmiennej <math>x</math> po zakończeniu pętli
+'''Pytanie:''' oto inna wersja jednej z powyższych reguł:
-wynosi albo <math>n_2</math> albo pozostaje niezmieniona.
+<math>
-Ponieważ nie zostało wyspecyfikowane jaka
+\mathbf{for}\, x = n_1 \,\mathbf{to}\, n_2 \,\mathbf{do}\, I, s \,\Longrightarrow\, I; \mathbf{for}\, x = n_1+1 \,\mathbf{to}\, n_2 \,\mathbf{do}\, I, s[x \mapsto s(x)+1]
-powinna być wartość tej zmiennej, możemy taką semantykę uznać
+\quad \mbox{ o ile } s(x) \leq n_2.
-za poprawną.
+</math>
+Czy semantyka jest taka sama?
+(Rozważ sytuację, gdy zmienna <math>x</math> jest zmieniana przez instrukcję <math>I</math>.)
-'''Pytanie:'''
+'''Pytanie:''' a gdybyśmy jednak zażądali przywrócenia na koniec wartości zmiennej <math>x</math>  sprzed pętli?
-A gdybyśmy jednak zażądali przywrócenia na koniec wartości zmiennej <math>x</math>
-sprzed pętli?
 Jak należałoby zmienić nasze reguły?
-Semantykę dla <math>\,\mathbf{do}\, I \, \mathbf{while}\, b</math> pozostawiamy Czytelnikowi jako
+Semantykę dla <math>\,\mathbf{do}\, I \, \mathbf{while}\, b</math> pozostawiamy Czytelnikowi jako proste ćwiczenie.
-proste ćwiczenie.
 Oczywiście minimalistyczne rozwiązanie to
 <math>
-\,\mathbf{do}\, I \,\mathbf{while}\, b, s \,\Longrightarrow\, \mathbf{repeat}\, I \,\mathbf{until}\, \neg b, s
+\,\mathbf{do}\, I \,\mathbf{while}\, b, s \,\Longrightarrow\, \mathbf{repeat}\, I \,\mathbf{until}\, \neg b, s.
 </math>
@@ Linia 437: / Linia 398: @@
 </math>
-<math>\epsilon</math> oznacza słowo puste, czyli np. <math>\epsilon 1 0 1 1</math>
+<math>\epsilon</math> oznacza słowo puste, czyli np. <math>\epsilon 1 0 1 1</math> oznacza binarną liczbę 1011.
-oznacza binarną liczbę 1011.
 Napisz semantykę operacyjną obliczającą wartość wyrażeń.
 }}
@@ Linia 447: / Linia 407: @@
 <div class="mw-collapsible mw-made=collapsible mw-collapsed"><div class="mw-collapsible-content" style="display:none">
-Składnia wyrażeń pozwala na wygodny dostęp do najmniej znaczącego
+Składnia wyrażeń pozwala na wygodny dostęp do najmniej znacząceg bitu liczby. Spróbujmy zatem zastosować metodę dodawania pisemnego:
-bitu liczby. Spróbujmy zatem zastosować metodę dodawania
-pisemnego:
 <math>
@@ Linia 475: / Linia 433: @@
 </math>
-Zauważmy, że w składni dopuszcza się dowolne przeplatanie operatora dodawania
+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.
-i bitów <math>0, 1</math>. Tę dowolność wykorzystaliśmy właśnie w regułach
+Gdyby nasz język ograniczyć tylko do składni
-powyżej. Gdyby nasz język ograniczyć tylko do składni
 <math>
@@ Linia 494: / Linia 451: @@
 (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
+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).
-zbiór wyrażeń. Konfiguracje końcowe to wyrażenia bez operatora dodawania
+Nasz pomysł jest taki, że tranzycje stopniowo przesuwają operator dodawania w lewo, aż się go ostatecznie ''pozbędą''.
-(liczby binarne). Nasz pomysł jest taki, że tranzycje stopniowo przesuwają
-operator dodawania w lewo, aż się go ostatecznie ''pozbędą''.
-Gdy obydwa składniki mają tyle samo cyfr, do zakończenia dodawania
+Gdy obydwa składniki mają tyle samo cyfr, do zakończenia dodawania potrzebujemy reguły:
-potrzebujemy reguły:
 <math>
@@ Linia 530: / Linia 484: @@
 gdyż spowodowałaby ona możliwość ''pętlenia się'', a zatem braku wyniku obliczenia.
-Na koniec dodajemy typowe reguły opisujące jak krok podwyrażenia indukuje
+Na koniec dodajemy typowe reguły opisujące jak krok podwyrażenia indukuje krok całego wyrażenia:
-krok całego wyrażenia:
 <math>
@@ Linia 554: / Linia 507: @@
 {{cwiczenie|4|cw4|
-Rozszerzmy składnię o jeden symbol <math>p</math> oznaczający
+Rozszerzmy składnię o jeden symbol <math>p</math> oznaczający ''przepełnienie'':
-''przepełnienie'':
 <math>
@@ Linia 566: / Linia 518: @@
 </math>
-Na przykład <math>p 1 0 1</math> oznacza tę samą liczbę co <math>\epsilon 1 0 1
+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''.
-</math>, ale z dodatkową informacją, że podczas jej obliczania nastąpiło
+Rozumiemy przez to sytuację, gdy wynik ma więcej cyfr niż każdy z argumentów.
-''przepełnienie''.
+Cyfry zero z lewej strony (najbardziej znaczące) również uważamy za pełnoprawne cyfry, nie należy ich usuwać ani dodawać nowych.
-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ą wartość wyrażenia wraz z
+Napisz semantykę operacyjną obliczającą wartość wyrażenia wraz z informacja o ewentualnym przepełnieniu.
-informacja o ewentualnym przepełnieniu.
+Wynik powinien byc poprawny przynajmniej dla wyrażeń <math>e</math> w składni ograniczonej:
-Wynik powinien byc poprawny przynajmniej dla wyrażeń <math>e</math> w składni
-ograniczonej:
 <math>
@@ Linia 591: / Linia 537: @@
        b 1.
 </math>
+reprezentujących sumę liczb binarnych.
 }}
@@ Linia 598: / Linia 546: @@
 <div class="mw-collapsible mw-made=collapsible mw-collapsed"><div class="mw-collapsible-content" style="display:none">
-Zadanie dotyczy w zasadzie składni ograniczonej, ale jako konfiguracji
+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.
-pośrednich będziemy zapewne potrzebować wyrażeń wykraczających poza
+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ć :)
-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
+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>).
-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
+Zacznijmy od najprostszej sytuacji, gdy jeden ze składników ma mniej cyfr, i to ten właśnie składnik odnotował przepełnienie:
-cyfr, i to ten właśnie składnik odnotował przepełnienie:
 <math>
@@ Linia 624: / Linia 565: @@
 </math>
-W takiej sytuacji oczywiście informacja o przepełnieniu zostaje
+W takiej sytuacji oczywiście informacja o przepełnieniu zostaje wymazana.
-wymazana.
+Jeśli przepełnienie zostało odnotowane w składniku o większej liczbie cyfr, to reguły
-Jeśli przepełnienie zostało odnotowane w składniku o większej liczbie
-cyfr, to reguły
 <math>
@@ Linia 641: / Linia 580: @@
 z poprzedniego zadania są wystarczające.
-Rozważmy teraz przypadek, gdy obydwa składniki mają tę samą liczbę
+Rozważmy teraz przypadek, gdy obydwa składniki mają tę samą liczbę cyfr.
-cyfr.
+Jeśli obydwa odnotowały przepełnienie, to oczywiście informacja ta powinna zostać zachowana:
-Jeśli obydwa odnotowały przepełnienie, to oczywiście informacja ta
-powinna zostać zachowana:
 <math>
@@ Linia 650: / Linia 587: @@
 </math>
-Ale co należy zrobić, gdy tylko jeden ze składników odnotował
+Ale co należy zrobić, gdy tylko jeden ze składników odnotował przepełnienie? <math>p + \epsilon \,\Longrightarrow\, ?</math>
-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ć.
-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:
@@ Linia 662: / Linia 597: @@
 </math>
-Na koniec zostało najważniejsze: kiedy powinniśmy generować sygnał o
+Na koniec zostało najważniejsze: kiedy powinniśmy generować sygnał o przepełnieniu?
-przepełnieniu?
+Przypomnijmy sobie reguły dla dadawania pisemnego w poprzednim zadaniu.
-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
+Natomiast jeśli jest przeniesienie, to stanowi ono ''potencjalne przepełnienie''.
-przepełnienie''.
 Odpowiednia reguła to
@@ Linia 675: / Linia 607: @@
 </math>
-Nowy sztuczny składnik <math>p 1</math> zawiera jakby na wszelki wypadek
+Nowy sztuczny składnik <math>p 1</math> zawiera jakby na wszelki wypadek informacje o potencjalnym przepełnieniu.
-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ę,
-Jeśli którykolwiek z pozostałych składników  <math>e_1</math> i <math>e_2</math>
+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.
-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.
 </div></div>
@@ Linia 692: / Linia 620: @@
 {{cwiczenie|1|cw1.dom|
-Podaj przykład wyrażenia boolowskiego, które nie policzy się
+Podaj przykład wyrażenia boolowskiego, które nie policzy się ani przy użyciu strategii lewo- ani prawostronnej, a policzy się przy strategii równoległej.
-ani przy użyciu strategii lewo- ani prawostronnej, a policzy się przy strategii
-równoległej.
 }}
@@ Linia 700: / Linia 626: @@
 {{cwiczenie|2|cw2.dom|
-Zmodyfikuj semantykę wyrażeń następująco: dla każdego podwyrażenia niedeterministycznie
+Zmodyfikuj semantykę wyrażeń następująco: dla każdego podwyrażenia niedeterministycznie wybierana jest albo strategia lewo- albo prawostronna, ale niedozwolony jest ,,przeplot".
-wybierana jest albo strategia lewo- albo prawostronna, ale
-niedozwolony jest ,,przeplot".
 }}
@@ Linia 708: / Linia 632: @@
 {{cwiczenie|3|cw3.dom|
-Rozważ inną semantykę pętli <math>\mathbf{for}\, x = e_1 \,\mathbf{to}\, e_2 \,\mathbf{do}\, I</math>,
+Rozważ inną semantykę pętli <math>\mathbf{for}\, x = e_1 \,\mathbf{to}\, e_2 \,\mathbf{do}\, I</math>, w której wyrażenie <math>e_2</math> jest obliczane na nowo przed każdą iteracją pętli.
-w której wyrażenie <math>e_2</math> jest obliczane na nowo
-przed każdą iteracją pętli.
-Napisz reguły semantyczne dla tej instrukcji, nie odwołując
-się do innych istrukcji pętli.
 }}
@@ Linia 730: / Linia 650: @@
 </math>
-polegającego na obliczeniu najpierw wartości wyrażeń
+polegającego na obliczeniu najpierw wartości wyrażeń <math>e_1, \ldots, e_n</math> a następnie na podstawieniu tych wartości na zmienne <math>x_1, \ldots, x_n</math>.
-<math>e_1, \ldots, e_n</math> a następnie na podstawieniu
-tych wartości na zmienne <math>x_1, \ldots, x_n</math>.
 }}