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

Aktualna wersja na dzień 21:29, 11 wrz 2023

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

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

$b : : = l | e_{1} \leq e_{2} | \neg b | b_{1} \land b_{2} | \dots$

$l : : = 𝐭 𝐫 𝐮 𝐞 | 𝐟 𝐚 𝐥 𝐬 𝐞$

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

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

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

Niech $𝐁 𝐄 𝐱 𝐩$ oznacza zbiór wyrażeń boolowskich, $b \in 𝐁 𝐄 𝐱 𝐩$ . 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 𝐒 𝐭 𝐚 𝐭 𝐞$ . Dodatkowo będziemy potrzebować również tranzycji postaci:

$e, s ⟹, n oraz b, s ⟹, l$ gdzie $n \in$ jest liczbą całkowitą, $n \in 𝐍 𝐮 𝐦$ , a $l \in 𝐁 𝐨 𝐨 𝐥 = {𝐭 𝐫 𝐮 𝐞, 𝐟 𝐚 𝐥 𝐬 𝐞}$ . Formalnie, zbiór konfiguracji dla semantyki całego języka Tiny to

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

a konfiguracje końcowe to $𝐒 𝐭 𝐚 𝐭 𝐞$ , aczkolwiek konfiguracje ze zbioru $𝐍 𝐮 𝐦 \cup 𝐁 𝐨 𝐨 𝐥$ pełnią podobną rolę dla wyrażeń arytmetycznych i boolowskich jako konfiguracje końcowe dla instrukcji. Przypomnijmy, że $𝐒 𝐭 𝐦 𝐭$ oznacza zbiór instrukcji, $I \in 𝐒 𝐭 𝐦 𝐭$ .

Zacznijmy od (chyba najprostszych) tranzycji dla stałych boolowskich i liczbowych:

$l, s ⟹, l n, s ⟹, n$

Podobnie jak poprzednio, zakładamy tutaj dla wygody, że $𝐍 𝐮 𝐦 \subseteq 𝐄 𝐱 𝐩$ oraz $𝐁 𝐨 𝐨 𝐥 \subseteq 𝐁 𝐄 𝐱 𝐩$ . 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 $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}, s ⟹, l, s 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} 𝐟 𝐚 𝐥 𝐬 𝐞 \land b_{2}, s ⟹, 𝐟 𝐚 𝐥 𝐬 𝐞, s 𝐭 𝐫 𝐮 𝐞 \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 𝐟 𝐚 𝐥 𝐬 𝐞, s ⟹, 𝐟 𝐚 𝐥 𝐬 𝐞, s b_{1} \land 𝐭 𝐫 𝐮 𝐞, 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 tzw. "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ły dla negacji:

$\neg 𝐭 𝐫 𝐮 𝐞, s ⟹, 𝐟 𝐚 𝐥 𝐬 𝐞, s \neg 𝐟 𝐚 𝐥 𝐬 𝐞, s ⟹, 𝐭 𝐫 𝐮 𝐞, 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 ⟹, 𝐭 𝐫 𝐮 𝐞, s o ile n_{1} \leq n_{2} n_{1} \leq n_{2}, s ⟹, 𝐟 𝐚 𝐥 𝐬 𝐞, 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}$ .

Jako pierwszą z instrukcji rozważmy przypisanie. Najpierw obliczamy wyrażenie po prawej stronie przypisania, a gdy wyrażenie to wyewoluuje do stałej (obliczy się), modyfikujemy stan:

$\frac{e, s ⟹, e^{'}, s}{x : = e, s ⟹, x : = e^{'}, s} x : = n, s ⟹, s [x \mapsto n]$

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:

$𝐢 𝐟 𝐭 𝐫 𝐮 𝐞 𝐭 𝐡 𝐞 𝐧 I_{1} 𝐞 𝐥 𝐬 𝐞 I_{2}, s ⟹, I_{1}, s 𝐢 𝐟 𝐟 𝐚 𝐥 𝐬 𝐞 𝐭 𝐡 𝐞 𝐧 I_{1} 𝐞 𝐥 𝐬 𝐞 I_{2}, s ⟹, I_{2}, s$

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

$𝐰 𝐡 𝐢 𝐥 𝐞 𝐭 𝐫 𝐮 𝐞 𝐝 𝐨 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 zasadzie do semantyki dużych kroków):

$\frac{b, s ⟹,^{*} 𝐭 𝐫 𝐮 𝐞}{𝐰 𝐡 𝐢 𝐥 𝐞 b 𝐝 𝐨 I, s ⟹, I; 𝐰 𝐡 𝐢 𝐥 𝐞 b 𝐝 𝐨 I, s} \frac{b, s ⟹,^{*} 𝐟 𝐚 𝐥 𝐬 𝐞}{𝐰 𝐡 𝐢 𝐥 𝐞 b 𝐝 𝐨 I, s ⟹, s}$

Istnieją inne możliwe rozwiązania w stylu małych kroków. Jedno z nich oparte jest na pomyśle, aby "rozwinąć" pętlę $𝐰 𝐡 𝐢 𝐥 𝐞$ , zanim obliczymy wartość dozoru $b$ . Jedyną reguła dla pętli $𝐰 𝐡 𝐢 𝐥 𝐞$ , byłaby wtedy reguła:

$𝐰 𝐡 𝐢 𝐥 𝐞 b 𝐝 𝐨 I, s ⟹, 𝐢 𝐟 b 𝐭 𝐡 𝐞 𝐧 (I; 𝐰 𝐡 𝐢 𝐥 𝐞 b 𝐝 𝐨 I) 𝐞 𝐥 𝐬 𝐞 𝐬 𝐤 𝐢 𝐩, s$

Dzięki temu obliczany warunek logiczny $b$ jest zawsze jednorazowy. Znalezienie innych rozwiązań, np. opartych na rozszerzeniu składni, pozostawiamy dociekliwemu Czytelnikowi.

Reguły dla operacji arytmetycznych również pozostawiamy do napisania Czytelnikowi.

Ć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

Instrukcja $𝐫 𝐞 𝐩 𝐞 𝐚 𝐭$ ,

Zacznijmy od pętli $𝐫 𝐞 𝐩 𝐞 𝐚 𝐭 I 𝐮 𝐧 𝐭 𝐢 𝐥 b$ . Przyjrzyjmy się dwóm podejściom, które zastosowaliśmy dla pętli $𝐰 𝐡 𝐢 𝐥 𝐞$ , w poprzednim zadaniu. Po pierwsze, rozwinięcie:

$𝐫 𝐞 𝐩 𝐞 𝐚 𝐭 I 𝐮 𝐧 𝐭 𝐢 𝐥 b, s ⟹, I; 𝐢 𝐟 b 𝐭 𝐡 𝐞 𝐧 (𝐫 𝐞 𝐩 𝐞 𝐚 𝐭 I 𝐮 𝐧 𝐭 𝐢 𝐥 b) 𝐞 𝐥 𝐬 𝐞 𝐬 𝐤 𝐢 𝐩, s$

Po drugie, spróbujmy odwołać się do $⟹,^{*}$ dla dozoru pętli $b$ :

$\frac{I, s ⟹, I^{'}, s^{'}}{𝐫 𝐞 𝐩 𝐞 𝐚 𝐭 I 𝐮 𝐧 𝐭 𝐢 𝐥 b, s ⟹, 𝐫 𝐞 𝐩 𝐞 𝐚 𝐭 I^{'} 𝐮 𝐧 𝐭 𝐢 𝐥 b, s^{'}}$

$\frac{I, s ⟹, s^{'} b, s ⟹,^{*} 𝐟 𝐚 𝐥 𝐬 𝐞}{𝐫 𝐞 𝐩 𝐞 𝐚 𝐭 I 𝐮 𝐧 𝐭 𝐢 𝐥 b, s ⟹, s^{'}} \frac{I, s ⟹, s^{'} b, s ⟹,^{*} 𝐭 𝐫 𝐮 𝐞}{𝐫 𝐞 𝐩 𝐞 𝐚 𝐭 I 𝐮 𝐧 𝐭 𝐢 𝐥 b, s ⟹, 𝐫 𝐞 𝐩 𝐞 𝐚 𝐭 ? 𝐮 𝐧 𝐭 𝐢 𝐥 b, s^{'}}$

Okazuje się, że jest jeszcze gorzej niż w przypadku pętli $𝐰 𝐡 𝐢 𝐥 𝐞$ ,: nie pamiętamy już, jaka była instrukcja wewnętrzna naszej pętli! Czyli takie podejście jest teraz nieskuteczne.

Instrukcja $𝐝 𝐨 e 𝐭 𝐢 𝐦 𝐞 𝐬 I$

Pętla $𝐝 𝐨 e 𝐭 𝐢 𝐦 𝐞 𝐬 I$ , w stanie $s$ , oznacza wykonanie instrukcji $I$ $n$ razy, gdzie $n$ to wartość, do której oblicza się $e$ w stanie $s$ . Czyli najpierw obliczmy $e$ przy pomocy reguły:

$\frac{e, s ⟹, e^{'}, s}{𝐝 𝐨 e 𝐭 𝐢 𝐦 𝐞 𝐬 I, s ⟹, D e^{'} 𝐭 𝐢 𝐦 𝐞 𝐬 I, s}$

która doprowadza nas do konfiguracji:

$𝐝 𝐨 n 𝐭 𝐢 𝐦 𝐞 𝐬 I, s$

Teraz jest już łatwo:

$𝐝 𝐨 n 𝐭 𝐢 𝐦 𝐞 𝐬 I, s ⟹, I; 𝐝 𝐨 n - 1 𝐭 𝐢 𝐦 𝐞 𝐬 I, s o ile n > 0$

$𝐝 𝐨 n 𝐭 𝐢 𝐦 𝐞 𝐬 I, s ⟹, s o ile n = 0$

Instrukcja $𝐟 𝐨 𝐫$ ,

W przypadku pętli $𝐟 𝐨 𝐫$ , przyjmijmy, że wartości wyrażeń $e_{1}$ i $e_{2}$ obliczane są przed pierwszą iteracją pętli. Dodatkowo ustalmy, że np. $e_{1}$ będzie obliczone jako pierwsze. Następnie podstawiamy wartość $e_{1}$ na zmienną $x$ . Czyli:

$\frac{e_{1}, s ⟹, e'_{1}, s}{𝐟 𝐨 𝐫 x = e_{1} 𝐭 𝐨 e_{2} 𝐝 𝐨 I, s ⟹, 𝐟 𝐨 𝐫 x = e'_{1} 𝐭 𝐨 e_{2} 𝐝 𝐨 I, s}$

$\frac{e_{2}, s ⟹, e'_{2}, s}{𝐟 𝐨 𝐫 x = n 𝐭 𝐨 e_{2} 𝐝 𝐨 I, s ⟹, 𝐟 𝐨 𝐫 x = n 𝐭 𝐨 e'_{2} 𝐝 𝐨 I, s}$

Zatem zakres zmiennej $x$ mamy już obliczony, tzn. jesteśmy w konfiguracji

$𝐟 𝐨 𝐫 x = n_{1} 𝐭 𝐨 n_{2} 𝐝 𝐨 I, s$

Dalsze reguły mogą być podobne do reguł dla pętli $𝐝 𝐨 n 𝐭 𝐢 𝐦 𝐞 𝐬 I$ :

$𝐟 𝐨 𝐫 x = n_{1} 𝐭 𝐨 n_{2} 𝐝 𝐨 I, s ⟹, I; 𝐟 𝐨 𝐫 x = n_{1} + 1 𝐭 𝐨 n_{2} 𝐝 𝐨 I, s [x \mapsto n_{1}] o ile n_{1} \leq n_{2}$

$𝐟 𝐨 𝐫 x = n_{1} 𝐭 𝐨 n_{2} 𝐝 𝐨 I, s ⟹, s o ile n_{1} > n_{2}$

Zauważmy, wartość zmiennej $x$ po zakończeniu pętli wynosi albo $n_{2}$ , albo pozostaje niezmieniona, o ile nie była ona zmieniana wewnątrz instrukcji $I$ . Ponieważ nie zostało wyspecyfikowane, jaka powinna być wartość tej zmiennej, możemy taką semantykę uznać za poprawną.

Pytanie: oto inna wersja jednej z powyższych reguł: $𝐟 𝐨 𝐫 x = n_{1} 𝐭 𝐨 n_{2} 𝐝 𝐨 I, s ⟹, I; 𝐟 𝐨 𝐫 x = n_{1} + 1 𝐭 𝐨 n_{2} 𝐝 𝐨 I, s [x \mapsto s (x) + 1] o ile s (x) \leq n_{2}$ Czy semantyka jest taka sama? (Rozważ sytuację, gdy zmienna $x$ jest zmieniana przez instrukcję $I$ .)

Pytanie: a gdybyśmy jednak zażądali przywrócenia na koniec wartości zmiennej $x$ sprzed pętli? Jak należałoby zmienić nasze reguły?

Semantykę dla $𝐝 𝐨 I 𝐰 𝐡 𝐢 𝐥 𝐞 b$ pozostawiamy Czytelnikowi jako proste ćwiczenie. Oczywiście minimalistyczne rozwiązanie to

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

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

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 obydwa składniki mają tyle samo cyfr, do zakończenia dodawania potrzebujemy reguły:

$ϵ + ϵ ⟹, ϵ$

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

Na koniec dodajemy typowe reguły opisujące jak krok podwyrażenia indukuje krok całego 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}$

Ć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

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 dodawania 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

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

Aktualna wersja na dzień 21:29, 11 wrz 2023

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 1: / Linia 1: @@
+== Zawartość ==
-== Zawarto¶æ ==
+Ćwiczymy dalej semantykę małych kroków.
+Uzupełnimy semantykę języka Tiny o semantykę operacyjną wyrażeń boolowskich i arytmetycznych.
-Æwiczymy dalej semantykê ma³ych kroków.
+Następnie rozszerzymy nasz język o róznorodne konstrukcje iteracji.
-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 ==
+== Rozszerzenia semantyki języka Tiny ==
 {{cwiczenie|1|cw1|
-Semantyka jêzyka Tiny z wyk³adu u¿ywa³a funkcji semantycznych
+Semantyka języka Tiny z wykładu używała funkcji semantycznych
 <math>
 B, E : State \to State
 </math>
-dla okre¶lenia znaczenia wyra¿eñ boolowskich i arytmetycznych.
+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.
 }}
-{{rozwiazanie||roz1|
+<div class="mw-collapsible mw-made=collapsible mw-collapsed">
+<span class="mw-collapsible-toogle mw-collapsible-toogle-default style="font-variant:small-caps">Rozwiązanie</span>
+<div class="mw-collapsible-content" style="display:none">
-<div class="mw-collapsible mw-made=collapsible mw-collapsed"><div class="mw-collapsible-content" style="display:none">
+Przypomnijmy składnię wyrażeń boolowskich i arytmetycznych:
-Przypomnijmy sk³adniê wyra¿eñ boolowskich i arytmetycznych:
 <math>
@@ Linia 60: / Linia 57: @@
 </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:
-Chcemy, aby tranzycje dla wyra¿eñ by³y postaci:
 <math>
-e, s \,\Longrightarrow\, e', s
+e, s \,\Longrightarrow, e', s
 </math>
-i podobnie dla wyra¿eñ boolowskich:
+i podobnie dla wyrażeń boolowskich:
 <math>
-b, s \,\Longrightarrow\, b', s
+b, s \,\Longrightarrow, b', s
 </math>
 gdzie <math>s \in \mathbf{State}</math>.
-Dodatkowo bêdziemy potrzebowaæ równie¿ tranzycji postaci:
+Dodatkowo będziemy potrzebować również tranzycji postaci:
 <math>
-e, s \,\Longrightarrow\, n
+e, s \,\Longrightarrow, n
 \quad \quad
 \mbox{ oraz }
 \quad \quad
-b, s \,\Longrightarrow\, l
+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
-Formalnie, zbiór konfiguracji dla semantyki ca³ego jêzyka Tiny to
 <math>
@@ Linia 93: / Linia 88: @@
 </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ê
+Przypomnijmy, że <math>\mathbf{Stmt}</math>  oznacza zbiór instrukcji, <math>I \in \mathbf{Stmt}</math>.
-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>.
-Zacznijmy od (chyba najprostszych) tranzycji dla sta³ych boolowskich i liczbowych:
+Zacznijmy od (chyba najprostszych) tranzycji dla stałych boolowskich i liczbowych:
 <math>
-l, s \,\Longrightarrow\, l
+l, s \,\Longrightarrow, l
 \quad \quad
-n, s \,\Longrightarrow\, n.
+n, s \,\Longrightarrow, n</math>
-</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>.
+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>
-\frac{b_1, s \,\Longrightarrow\, b'_1, s}
+\frac{b_1, s \,\Longrightarrow, b'_1, s}
-{b_1 \land b_2, s \,\Longrightarrow\, b'_1 \land b_2, s}
+{b_1 \land b_2, s \,\Longrightarrow, b'_1 \land b_2, s}
 \quad \quad
-\frac{b_2, s \,\Longrightarrow\, b'_2, s}
+\frac{b_2, s \,\Longrightarrow, b'_2, s}
-{l_1 \land b_2, s \,\Longrightarrow\, l_1 \land b_2, s}
+{l_1 \land b_2, s \,\Longrightarrow, l_1 \land b_2, s}
 \quad \quad
-l_1 \land l_2, s \,\Longrightarrow\, l, s
+l_1 \land l_2, s \,\Longrightarrow, l, s
 \mbox{ o ile } l = l_1 \land l_2
 </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:
-Oto odpowiednio zmodyfikowane regu³y:
 <math>
-\frac{b_1, s \,\Longrightarrow\, b'_1, s}
+\frac{b_1, s \,\Longrightarrow, b'_1, s}
-{b_1 \land b_2, s \,\Longrightarrow\, b'_1 \land b_2, s}
+{b_1 \land b_2, s \,\Longrightarrow, b'_1 \land b_2, s}
 \quad \quad
-\mathbf{false} \land b_2, s \,\Longrightarrow\, \mathbf{false}, s
+\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>
-</math>
-Analogicznie regu³y prawostronne to:
+Analogicznie reguły prawostronne to:
 <math>
-\frac{b_2, s \,\Longrightarrow\, b'_2, s}
+\frac{b_2, s \,\Longrightarrow, b'_2, s}
-{b_1 \land b_2, s \,\Longrightarrow\, b_1 \land b'_2, s}
+{b_1 \land b_2, s \,\Longrightarrow, b_1 \land b'_2, s}
 \quad \quad
-b_1 \land \mathbf{false}, s \,\Longrightarrow\, \mathbf{false}, s
+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>
-</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:
+Oto reguły dla negacji:
 <math>
-\neg \mathbf{true}, s \,\Longrightarrow\, \mathbf{false}, s
+\neg \mathbf{true}, s \,\Longrightarrow, \mathbf{false}, s
 \quad \quad \quad
-\neg \mathbf{false}, s \,\Longrightarrow\, \mathbf{true}, s
+\neg \mathbf{false}, s \,\Longrightarrow, \mathbf{true}, s
 \quad \quad \quad
-\frac{b, s \,\Longrightarrow\, b', s}
+\frac{b, s \,\Longrightarrow, b', s}
-      {\neg b, s \,\Longrightarrow\, \neg b', s}
+      {\neg b, s \,\Longrightarrow, \neg b', s}
 </math>
-Regu³y dla <math>e_1 \leq e_2</math> s± nastêpuj±ce:
+Reguły dla <math>e_1 \leq e_2</math> są następujące:
 <math>
-\frac{e_1, s \,\Longrightarrow\, e'_1, s}
+\frac{e_1, s \,\Longrightarrow, e'_1, s}
-{e_1 \leq e_2, s \,\Longrightarrow\, e'_1 \leq e_2, s}
+{e_1 \leq e_2, s \,\Longrightarrow, e'_1 \leq e_2, s}
 \quad \quad
-\frac{e_2, s \,\Longrightarrow\, e'_2, s}
+\frac{e_2, s \,\Longrightarrow, e'_2, s}
-{e_1 \leq e_2, s \,\Longrightarrow\, e_1 \leq 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</math>
-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.
+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.
+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>
-\frac{e, s \,\Longrightarrow\, e', s}
+\frac{e, s \,\Longrightarrow, e', s}
-      {x := e, s \,\Longrightarrow\, x := e', s}
+      {x := e, s \,\Longrightarrow, x := e', s}
 \quad \quad
-{x := n, s \,\Longrightarrow\, s[x \mapsto n]}
+{x := n, s \,\Longrightarrow, s[x \mapsto n]}
 </math>
-Rozwa¿my teraz instrukcjê warunkow± i instrukcjê pêtli.
+Rozważmy teraz instrukcję warunkową i instrukcję pętli.
-Najpierw obliczamy warto¶æ dozoru:
+Najpierw obliczamy wartość dozoru:
 <math>
-\frac{b, s \,\Longrightarrow\, b', s}
+\frac{b, s \,\Longrightarrow, b', s}
-{\mathbf{if}\, b \,\mathbf{then}\, I_1 \,\mathbf{else}\, I_2, s \,\Longrightarrow\,
+{\mathbf{if}\, b \,\mathbf{then}\, I_1 \,\mathbf{else}\, I_2, s \,\Longrightarrow,
 \mathbf{if}\, b' \,\mathbf{then}\, I_1 \,\mathbf{else}\, I_2, s}
 \quad \quad
-\frac{b, s \,\Longrightarrow\, b', s}
+\frac{b, s \,\Longrightarrow, b', s}
-{\mathbf{while}\, b \,\mathbf{do}\, I, s \,\Longrightarrow\, \mathbf{while}\, b' \,\mathbf{do}\, I, s}
+{\mathbf{while}\, b \,\mathbf{do}\, I, s \,\Longrightarrow, \mathbf{while}\, b' \,\mathbf{do}\, I, s}
 </math>
-a gdy dozór jest ju¿ obliczony, podejmujemy decyzjê.
+a gdy dozór jest już obliczony, podejmujemy decyzję.
-W przypadku instrukcji warunkowej regu³y s± oczywiste:
+W przypadku instrukcji warunkowej reguły są oczywiste:
 <math>
-\mathbf{if}\, \mathbf{true} \,\mathbf{then}\, I_1 \,\mathbf{else}\, I_2, s \,\Longrightarrow\, I_1, s
+\mathbf{if}\, \mathbf{true} \,\mathbf{then}\, I_1 \,\mathbf{else}\, I_2, s \,\Longrightarrow, I_1, s
 \quad \quad
-\mathbf{if}\, \mathbf{false} \,\mathbf{then}\, I_1 \,\mathbf{else}\, I_2, s \,\Longrightarrow\, I_2, s
+\mathbf{if}\, \mathbf{false} \,\mathbf{then}\, I_1 \,\mathbf{else}\, I_2, s \,\Longrightarrow, I_2, s
 </math>
-Gorzej jest w przypadku instrukcji pêtli. Regu³a mog³aby wygl±daæ tak:
+Gorzej jest w przypadku instrukcji pętli. Reguła mogłaby wyglądać tak:
 <math>
-\mathbf{while}\, \mathbf{true} \,\mathbf{do}\, I, s \,\Longrightarrow\,
+\mathbf{while}\, \mathbf{true} \,\mathbf{do}\, I, s \,\Longrightarrow,
 I;\, \mathbf{while}\, ? \,\mathbf{do}\, I, s
 </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>
-\frac{b, s \,\Longrightarrow\,^{*} \mathbf{true}}
+\frac{b, s \,\Longrightarrow,^{*} \mathbf{true}}
-{\mathbf{while}\, b \,\mathbf{do}\, I, s \,\Longrightarrow\,
+{\mathbf{while}\, b \,\mathbf{do}\, I, s \,\Longrightarrow,
   I;\, \mathbf{while}\, b \,\mathbf{do}\, I, s}
 \quad \quad
-\frac{b, s \,\Longrightarrow\,^{*} \mathbf{false}}
+\frac{b, s \,\Longrightarrow,^{*} \mathbf{false}}
-{\mathbf{while}\, b \,\mathbf{do}\, I, s \,\Longrightarrow\, s}
+{\mathbf{while}\, b \,\mathbf{do}\, I, s \,\Longrightarrow, s}
 </math>
-Takie rozwi±zanie nie jest zatem ''czyst±'' semantyk±
+Istnieją inne możliwe rozwiązania w stylu małych kroków.
-ma³ych kroków.
+Jedno z nich oparte jest na pomyśle, aby "rozwinąć" pętlę <math>\mathbf{while}\ </math>, zanim obliczymy wartość dozoru <math>b</math>.
-Istniej± inne mo¿liwe rozwi±zania w stylu ma³ych kroków.
+Jedyną reguła dla pętli <math>\mathbf{while}\ </math>, byłaby wtedy reguła:
-Jedno z nich oparte jest na pomy¶le, aby ''rozwin±c'' pêtlê
-<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:
 <math>
-\mathbf{while}\, b \,\mathbf{do}\, I, s \,\Longrightarrow\, \mathbf{if}\, b \,\mathbf{then}\, (I; \mathbf{while}\, b \,\mathbf{do}\, I) \,\mathbf{else}\, \mathbf{skip}, s.
+\mathbf{while}\, b \,\mathbf{do}\, I, s \,\Longrightarrow, \mathbf{if}\, b \,\mathbf{then}\, (I; \mathbf{while}\, b \,\mathbf{do}\, I) \,\mathbf{else}\, \mathbf{skip}, s</math>
-</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.
+Reguły dla operacji arytmetycznych również pozostawiamy do napisania Czytelnikowi.
 </div></div>
-}}
 {{cwiczenie|2|cw2|
-Rozszerzmy jêzyk Tiny o nastêpuj±ce dobrze znane konstrukcje iteracji:
+Rozszerzmy język Tiny o następujące dobrze znane konstrukcje iteracji:
 <math>
@@ Linia 285: / Linia 247: @@
 </math>
-Napisz semantykê ma³ych kroków dla powy¿szych konstrukcji.
+Napisz semantykę małych kroków dla powyższych konstrukcji.
 }}
-{{rozwiazanie||roz2|
-<div class="mw-collapsible mw-made=collapsible mw-collapsed"><div class="mw-collapsible-content" style="display:none">
+<div class="mw-collapsible mw-made=collapsible mw-collapsed">
+<span class="mw-collapsible-toogle mw-collapsible-toogle-default style="font-variant:small-caps">Rozwiązanie</span>
+<div class="mw-collapsible-content" style="display:none">
-'''Instrukcja <math>\mathbf{repeat}\,</math>'''
+'''Instrukcja <math>\mathbf{repeat}\ </math>,'''
 <br>
-Zacznijmy od pêtli <math>\mathbf{repeat}\, I \,\mathbf{until}\, b</math>.
+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:
-Po pierwsze rozwiniêcie:
 <math>
-\mathbf{repeat}\, I \,\mathbf{until}\, b, s \,\Longrightarrow\, I; \mathbf{if}\, b \,\mathbf{then}\, (\mathbf{repeat}\, I \,\mathbf{until}\, b) \,\mathbf{else}\, \mathbf{skip}, s.
+\mathbf{repeat}\, I \,\mathbf{until}\, b, s \,\Longrightarrow, I; \mathbf{if}\, b \,\mathbf{then}\, (\mathbf{repeat}\, I \,\mathbf{until}\, b) \,\mathbf{else}\, \mathbf{skip}, s</math>
-</math>
-Po drugie, spróbujmy odwo³aæ siê do <math>\,\Longrightarrow\,^{*}</math> dla dozoru pêtli <math>b</math>:
+Po drugie, spróbujmy odwołać się do <math>\,\Longrightarrow,^{*}</math> dla dozoru pętli <math>b</math>:
 <math>
-\frac{I, s \,\Longrightarrow\, I', s'}
+\frac{I, s \,\Longrightarrow, I', s'}
-      {\mathbf{repeat}\, I \,\mathbf{until}\, b, s \,\Longrightarrow\, \mathbf{repeat}\, I' \,\mathbf{until}\, b, s'}
+      {\mathbf{repeat}\, I \,\mathbf{until}\, b, s \,\Longrightarrow, \mathbf{repeat}\, I' \,\mathbf{until}\, b, s'}
 </math>
 <math>
-\frac{I, s \,\Longrightarrow\, s' \quad b, s \,\Longrightarrow\,^{*} \mathbf{false}}
+\frac{I, s \,\Longrightarrow, s' \quad b, s \,\Longrightarrow,^{*} \mathbf{false}}
-      {\mathbf{repeat}\, I \,\mathbf{until}\, b, s \,\Longrightarrow\, s'}
+      {\mathbf{repeat}\, I \,\mathbf{until}\, b, s \,\Longrightarrow, s'}
 \quad \quad
-\frac{I, s \,\Longrightarrow\, s' \quad b, s \,\Longrightarrow\,^{*} \mathbf{true}}
+\frac{I, s \,\Longrightarrow, s' \quad b, s \,\Longrightarrow,^{*} \mathbf{true}}
-      {\mathbf{repeat}\, I \,\mathbf{until}\, b, s \,\Longrightarrow\, \mathbf{repeat}\, ? \,\mathbf{until}\, b, s'}
+      {\mathbf{repeat}\, I \,\mathbf{until}\, b, s \,\Longrightarrow, \mathbf{repeat}\, ? \,\mathbf{until}\, b, s'}
 </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.
-Czyli takie podej¶cie jest teraz nieskuteczne.
 <br>
@@ Linia 329: / Linia 288: @@
 <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ê
+Czyli najpierw obliczmy <math>e</math> przy pomocy reguły:
-<math>e</math> w stanie <math>s</math>.
-Czyli najpierw obliczmy <math>e</math> przy pomocy regu³y:
 <math>
-\frac{e, s \,\Longrightarrow\, e', s}
+\frac{e, s \,\Longrightarrow, e', s}
-      {\,\mathbf{do}\, e \,\mathbf{times}\, I, s \,\Longrightarrow\, D e' \,\mathbf{times}\, I, s}
+      {\,\mathbf{do}\, e \,\mathbf{times}\, I, s \,\Longrightarrow, D e' \,\mathbf{times}\, I, s}
 </math>
@@ Linia 342: / Linia 299: @@
 <math>
-\,\mathbf{do}\, n \,\mathbf{times}\, I, s.
+\,\mathbf{do}\, n \,\mathbf{times}\, I, s</math>
-</math>
-Teraz jest juz ³atwo:
+Teraz jest już łatwo:
 <math>
-\,\mathbf{do}\, n \,\mathbf{times}\, I, s \,\Longrightarrow\, I; \,\mathbf{do}\, n{-}1 \,\mathbf{times}\, I, s
+\,\mathbf{do}\, n \,\mathbf{times}\, I, s \,\Longrightarrow, I; \,\mathbf{do}\, n{-}1 \,\mathbf{times}\, I, s
 \quad \mbox{ o ile } n > 0
 </math>
 <math>
-\,\mathbf{do}\, n \,\mathbf{times}\, I, s \,\Longrightarrow\, s
+\,\mathbf{do}\, n \,\mathbf{times}\, I, s \,\Longrightarrow, s
-\quad \mbox{ o ile } n = 0.
+\quad \mbox{ o ile } n = 0</math>
-</math>
 <br>
-'''Instrukcja <math>\mathbf{for}\,</math>'''
+'''Instrukcja <math>\mathbf{for}\ </math>,'''
 <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:
 <math>
-\frac{e_1, s \,\Longrightarrow\, e'_1, s}
+\frac{e_1, s \,\Longrightarrow, e'_1, s}
-      {\mathbf{for}\, x = e_1 \,\mathbf{to}\, e_2 \,\mathbf{do}\, I,s \,\Longrightarrow\, \mathbf{for}\, x = e'_1 \,\mathbf{to}\, e_2 \,\mathbf{do}\, I, s}
+      {\mathbf{for}\, x = e_1 \,\mathbf{to}\, e_2 \,\mathbf{do}\, I,s \,\Longrightarrow, \mathbf{for}\, x = e'_1 \,\mathbf{to}\, e_2 \,\mathbf{do}\, I, s}
 </math>
 <math>
-\frac{e_2, s \,\Longrightarrow\, e'_2, s}
+\frac{e_2, s \,\Longrightarrow, e'_2, s}
-      {\mathbf{for}\, x = n \,\mathbf{to}\, e_2 \,\mathbf{do}\, I,s \,\Longrightarrow\, \mathbf{for}\, x = n \,\mathbf{to}\, e'_2 \,\mathbf{do}\, I, s}
+      {\mathbf{for}\, x = n \,\mathbf{to}\, e_2 \,\mathbf{do}\, I,s \,\Longrightarrow, \mathbf{for}\, x = n \,\mathbf{to}\, e'_2 \,\mathbf{do}\, I, s}
 </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>
-\mathbf{for}\, x = n_1 \,\mathbf{to}\, n_2 \,\mathbf{do}\, I, s.
+\mathbf{for}\, x = n_1 \,\mathbf{to}\, n_2 \,\mathbf{do}\, I, s</math>
-</math>
-Dalsze regu³y mog± byæ podobne do regu³ dla pêtli <math>\,\mathbf{do}\, n \,\mathbf{times}\, I</math>:
+Dalsze reguły mogą być podobne do reguł dla pętli <math>\,\mathbf{do}\, n \,\mathbf{times}\, I</math>:
 <math>
-\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 n_1]
+\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 n_1]
 \quad \mbox{ o ile } n_1 \leq n_2
 </math>
 <math>
-\mathbf{for}\, x = n_1 \,\mathbf{to}\, n_2 \,\mathbf{do}\, I, s \,\Longrightarrow\, s
+\mathbf{for}\, x = n_1 \,\mathbf{to}\, n_2 \,\mathbf{do}\, I, s \,\Longrightarrow, s
 \quad \mbox{ o ile } n_1 > n_2
 </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</math>
-za poprawn±.
+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>
+Jak należałoby zmienić nasze reguły?
-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
-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>
-</math>
 </div></div>
-}}
 == Kalkulator binarny ==
@@ Linia 427: / Linia 375: @@
 {{cwiczenie|3|cw3|
-Rozwa¿my nastêpuj±cy jêzyk wyra¿eñ (liczby binarne z dodawaniem):
+Rozważmy następujący język wyrażeń (liczby binarne z dodawaniem):
 <math>
@@ Linia 437: / Linia 385: @@
 </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ń.
-Napisz semantykê operacyjn± obliczaj±c± warto¶æ wyra¿eñ.
 }}
-{{rozwiazanie||roz3|
-<div class="mw-collapsible mw-made=collapsible mw-collapsed"><div class="mw-collapsible-content" style="display:none">
+<div class="mw-collapsible mw-made=collapsible mw-collapsed">
+<span class="mw-collapsible-toogle mw-collapsible-toogle-default style="font-variant:small-caps">Rozwiązanie</span>
+<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ącego bitu liczby. Spróbujmy zatem zastosować metodę dodawania pisemnego:
-bitu liczby. Spróbujmy zatem zastosowaæ metodê dodawania
-pisemnego:
 <math>
-e_1 0 + e_2 0 \,\Longrightarrow\, (e_1 + e_2) 0
+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
+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
+e_1 1 + e_2 0 \,\Longrightarrow, (e_1 + e_2) 1
 </math>
-Ale co zrobiæ z przeniesieniem?
+Ale co zrobić z przeniesieniem?
 <math>
-e_1 1 + e_2 1 \,\Longrightarrow\, ?
+e_1 1 + e_2 1 \,\Longrightarrow, ?
 </math>
-Podstawowy pomys³ polega na potraktowaniu przeniesienia jak dodatkowego sk³adnika:
+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
+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
+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 492: / Linia 437: @@
 </math>
-(nazwijmy j± ''sk³adni± ograniczon±'') to powy¿sze regu³y by³yby niepoprawne.
+(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>
-\epsilon + \epsilon \,\Longrightarrow\, \epsilon.
+\epsilon + \epsilon \,\Longrightarrow, \epsilon</math>
-</math>
-Gdy jeden ze sk³adników ma mniej cyfr ni¿ drugi, potrzebujemy regu³:
+Gdy jeden ze składników ma mniej cyfr niż drugi, potrzebujemy reguł:
 <math>
-\epsilon + e 0 \,\Longrightarrow\, e 0
+\epsilon + e 0 \,\Longrightarrow, e 0
 \quad \quad
-\epsilon + e 1 \,\Longrightarrow\, e 1
+\epsilon + e 1 \,\Longrightarrow, e 1
 </math>
@@ Linia 517: / Linia 458: @@
 <math>
-e 0 + \epsilon \,\Longrightarrow\, e 0
+e 0 + \epsilon \,\Longrightarrow, e 0
 \quad \quad
-e 1 + \epsilon \,\Longrightarrow\, e 1.
+e 1 + \epsilon \,\Longrightarrow, e 1</math>
-</math>
-Niestety, nie mo¿emy u¿yæ regu³y przemienno¶ci:
+Niestety, nie możemy użyć reguły przemienności:
 <math>
-e_1 + e_2 \,\Longrightarrow\, e_2 + e_1
+e_1 + e_2 \,\Longrightarrow, e_2 + e_1
 </math>
-gdy¿ spowodowa³aby ona mo¿liwo¶æ ''pêtlenia siê'', a zatem braku wyniku obliczenia.
+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>
-\frac{e_1 \,\Longrightarrow\, e'_1}
+\frac{e_1 \,\Longrightarrow, e'_1}
-      {e_1 + e_2 \,\Longrightarrow\, e'_1 + e_2}
+      {e_1 + e_2 \,\Longrightarrow, e'_1 + e_2}
 \quad \quad
-\frac{e_2 \,\Longrightarrow\, e'_2}
+\frac{e_2 \,\Longrightarrow, e'_2}
-      {e_1 + e_2 \,\Longrightarrow\, e_1 + e'_2}
+      {e_1 + e_2 \,\Longrightarrow, e_1 + e'_2}
 \quad \quad
-\frac{e \,\Longrightarrow\, e'}
+\frac{e \,\Longrightarrow, e'}
-      {e 0 \,\Longrightarrow\, e' 0}
+      {e 0 \,\Longrightarrow, e' 0}
 \quad \quad
-\frac{e \,\Longrightarrow\, e'}
+\frac{e \,\Longrightarrow, e'}
-      {e 1 \,\Longrightarrow\, e' 1}
+      {e 1 \,\Longrightarrow, e' 1}
 \quad \quad
 </math>
 </div></div>
-}}
 {{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 563: / Linia 501: @@
        e 0  \,\,|\,\,
        e 1  \,\,|\,\,
-       e_1 + e_2 .
+       e_1 + e_2 </math>
-</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 589: / Linia 520: @@
        \epsilon  \,\,|\,\,
        b 0  \,\,|\,\,
-       b 1.
+       b 1</math>
-</math>
+reprezentujących sumę liczb binarnych.
 }}
-{{rozwiazanie||roz4|
+<div class="mw-collapsible mw-made=collapsible mw-collapsed">
+<span class="mw-collapsible-toogle mw-collapsible-toogle-default style="font-variant:small-caps">Rozwiązanie</span>
+<div class="mw-collapsible-content" style="display:none">
-<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 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ć :)
-Zadanie dotyczy w zasadzie sk³adni ograniczonej, ale jako konfiguracji
+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>).
-po¶rednich bêdziemy zapewne potrzebowaæ wyra¿eñ wykraczaj±cych poza
+Spróbujmy pozostawić wszystkie reguły z poprzedniego zadania.
-tê sk³adniê, np. <math>(e_1 + e_2) 0</math>, podobnie jak w poprzednim
+Dodamy tylko kilka nowych reguł, odpowiedzialnych za przepełnienie.
-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
+Zacznijmy od najprostszej sytuacji, gdy jeden ze składników ma mniej cyfr, i to ten właśnie składnik odnotował przepełnienie:
-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
+p + e 0 \,\Longrightarrow, e 0
 \quad \quad
-p + e 1 \,\Longrightarrow\, e 1
+p + e 1 \,\Longrightarrow, e 1
 \quad \quad
-e 0 + p \,\Longrightarrow\, e 0
+e 0 + p \,\Longrightarrow, e 0
 \quad \quad
-e 1 + p \,\Longrightarrow\, e 1.
+e 1 + p \,\Longrightarrow, e 1</math>
-</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>
-\epsilon + e 0 \,\Longrightarrow\, e 0
+\epsilon + e 0 \,\Longrightarrow, e 0
 \quad \quad
-\epsilon + e 1 \,\Longrightarrow\, e 1
+\epsilon + e 1 \,\Longrightarrow, e 1
 \quad \quad
-e 0 + \epsilon \,\Longrightarrow\, e 0
+e 0 + \epsilon \,\Longrightarrow, e 0
 \quad \quad
-e 1 + \epsilon \,\Longrightarrow\, e 1.
+e 1 + \epsilon \,\Longrightarrow, e 1</math>
-</math>
-z poprzedniego zadania s± wystarczaj±ce.
+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>
-p + p \,\Longrightarrow\, p.
+p + p \,\Longrightarrow, p</math>
-</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¿
+Oto odpowiednie reguły:
-drugi sk³adnik ma wystarczaj±co du¿o cyfr by je przes³oniæ.
-Oto odpowiednie regu³y:
 <math>
-p + \epsilon \,\Longrightarrow\, \epsilon
+p + \epsilon \,\Longrightarrow, \epsilon
 \quad \quad
-\epsilon + p \,\Longrightarrow\, \epsilon.
+\epsilon + p \,\Longrightarrow, \epsilon</math>
-</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 dodawania pisemnego w poprzednim zadaniu.
-Przypomnijmy sobie regu³y dla dadawania pisemnego w poprzednim
+Jeśli nie ma przeniesienia, to przepełnienie nie może powstać.
-zadaniu.
+Natomiast jeśli jest przeniesienie, to stanowi ono ''potencjalne przepełnienie''.
-Je¶li nie ma przeniesienia, to przepe³nienie nie mo¿e powstaæ.
+Odpowiednia reguła to
-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.
+e_1 1 + e_2 1 \,\Longrightarrow, ((e_1 + e_2) + p 1) 0</math>
-</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.
+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.
 </div></div>
-}}
 == Zadania domowe ==
@@ Linia 692: / Linia 597: @@
 {{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 603: @@
 {{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 strategia lewo- albo prawostronna, ale niedozwolony jest "przeplot".
-wybierana jest albo strategia lewo- albo prawostronna, ale
-niedozwolony jest ,,przeplot".
 }}
@@ Linia 708: / Linia 609: @@
 {{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 718: / Linia 615: @@
 {{cwiczenie|4|cw4.dom|
-Dodaj do wyra¿eñ binarnych operacjê odejmowania.
+Dodaj do wyrażeń binarnych operację odejmowania.
 }}
@@ Linia 724: / Linia 621: @@
 {{cwiczenie|5|cw15.dom|
-Zaproponuj semantykê przypisania równoleg³ego w jêzyku Tiny:
+Zaproponuj semantykę przypisania równoległego w języku TINY:
 <math>
@@ Linia 730: / Linia 627: @@
 </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>.
 }}