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ść ==
 Ć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.
-== Rozszerzenia języka Tiny ==
+== Rozszerzenia semantyki języka Tiny ==
-==== Zadanie 1 ====
+{{cwiczenie|1|cw1|
 Semantyka języka Tiny z wykładu używała funkcji semantycznych
@@ Linia 19: / Linia 17: @@
 B, E : State \to State
 </math>
-dla określenie 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.
+}}
-==== Rozwiązanie ====
+<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">
 Przypomnijmy składnię wyrażeń boolowskich i arytmetycznych:
 <math>
 b \, ::= \,\,
-         true   \,\,|\,\,
+         l \,\,|\,\,
-        false  \,\,|\,\,
          e_1 \leq e_2  \,\,|\,\,
          \neg b  \,\,|\,\,
          b_1  \land  b_2   \,\,|\,\, \ldots
+</math>
+<math>
+l \, ::= \,\,
+        \mathbf{true}    \,\,|\,\,
+        \mathbf{false}
 </math>
 <math>
 e \,  ::= \,\,
-   \,\,|\,\,   1     \,\,|\,\,   \ldots   \,\,|\,\,
+         n  \,\,|\,\,
          x  \,\,|\,\,
          e_1 + e_2  \,\,|\,\, \ldots
 </math>
+<math>
+n \, ::= \,\, 0 \,\,|\,\, 1 \,\,|\,\, \ldots
+</math>
+<math>
+x \, ::= \,\, \ldots \, (identyfikatory) \, \ldots
+</math>
+Niech <math>\mathbf{BExp}</math>  oznacza zbiór wyrażeń boolowskich, <math>b \in \mathbf{BExp}</math>.
 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:
 <math>
-b, s \longrightarrow b', s
+b, s \,\Longrightarrow, b', s
 </math>
-gdzie <math>s \in State</math>.
-Zacznijmy od wyrażeń boolowskich.
+gdzie <math>s \in \mathbf{State}</math>.
+Dodatkowo będziemy potrzebować również tranzycji postaci:
 <math>
-true, s \Longrightarrow true
+e, s \,\Longrightarrow, n
+\quad \quad
+\mbox{ oraz }
 \quad \quad
-false, s \Longrightarrow false
+b, s \,\Longrightarrow, l
 </math>
+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>.
+Formalnie, zbiór konfiguracji dla semantyki całego języka Tiny to
+<math>
+( (\mathbf{Exp} \, \cup \, \mathbf{BExp} \, \cup \, \mathbf{Stmt}) \times \mathbf{State} ) \, \bigcup \,
+\mathbf{Num} \, \cup \, \mathbf{Bool} \, \cup \, \mathbf{State}
+</math>
+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.
+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:
+<math>
+l, s \,\Longrightarrow, l
+\quad \quad
+n, s \,\Longrightarrow, n</math>
+Podobnie jak poprzednio, zakładamy tutaj dla wygody, że <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.
 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 \Longrightarrow l,
+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:
 <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
-false \land b_2, s \Longrightarrow false
+\mathbf{false} \land b_2, s \,\Longrightarrow, \mathbf{false}, s
 \quad \quad
-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:
 <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 false, s \Longrightarrow false
+b_1 \land \mathbf{false}, s \,\Longrightarrow, \mathbf{false}, s
 \quad \quad
-b_1 \land 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ła dla negacji:
+Oto reguły dla negacji:
 <math>
-\neg true, s \Longrightarrow false, s
+\neg \mathbf{true}, s \,\Longrightarrow, \mathbf{false}, s
 \quad \quad \quad
-\neg false, s \Longrightarrow 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>
@@ Linia 129: / Linia 154: @@
 <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}
+{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{false}, s  \quad  \mbox{ o ile } n_1 > n_2</math>
-\frac{e_2, s \Longrightarrow e'_2, s}
+Reguły powyższe zależą od semantyki wyrażen arytmetycznych.
-{e_1 \leq e_2, s \Longrightarrow e_1 \leq e'_2, s}
+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>.
-n_1 \leq n_2, s \Longrightarrow true, s   \quad \mbox{ o ile }
+Jako pierwszą z instrukcji rozważmy przypisanie.
-n_1 \leq n_2
+Najpierw obliczamy wyrażenie po prawej stronie przypisania, a gdy wyrażenie to wyewoluuje do stałej (obliczy się), modyfikujemy stan:
-n_1 \leq n_2, s \Longrightarrow false, s  \quad  \mbox{ o ile }
+<math>
-n_1 > n_2
+\frac{e, s \,\Longrightarrow, e', s}
+     {x := e, s \,\Longrightarrow, x := e', s}
+\quad \quad
+{x := n, s \,\Longrightarrow, s[x \mapsto n]}
 </math>
-Reguły powyższe zależą od semantyki wyrażen arytmetycznych.
-Zauważmy, że ponownie pozostawiliśmy dowolność jeśli chodzi o
-kolejność obliczania wyrażeń arytmetycznych e_1 i e_2.
 Rozważmy teraz instrukcję warunkową i instrukcję pętli.
@@ Linia 150: / Linia 183: @@
 <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}
+\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>
@@ Linia 162: / Linia 195: @@
 <math>
-\mathbf{if}\, 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}\, 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 instukcji 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}\, true\, \mathbf{do}\, I, s \Longrightarrow
+\mathbf{while}\, \mathbf{true} \,\mathbf{do}\, I, s \,\Longrightarrow,
-I;\, \mathbf{while}\, ?\, \mathbf{do}\, I, s
+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\,^{*} 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}
+  I;\, \mathbf{while}\, b \,\mathbf{do}\, I, s}
 \quad \quad
-\frac{b, s \,\Longrightarrow\,^{*} 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ą
-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ąć" pętlę <math>\mathbf{while}\ </math>, zanim obliczymy wartość dozoru <math>b</math>.
-<math> \mathbf{while}\, </math> jeden raz:
+Jedyną reguła dla pętli <math>\mathbf{while}\ </math>, byłaby wtedy reguła:
- <math>
+<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 ''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.
-Dzięki temu obliczany warunek logiczny <math> b </math> jest zawsze
+</div></div>
-''jednorazowy''.
-Znalezienie innych rozwiązań, np. opartych na rozszerzeniu składni,
-pozostawiamy dociekliwemu czytelnikowi.
-Reguły dla operacji arytmetycznych pozostawiamy do napisania Czytelnikowi.
-==== Zadanie 2 ====
+{{cwiczenie|2|cw2|
 Rozszerzmy język Tiny o następujące dobrze znane konstrukcje iteracji:
@@ Linia 214: / Linia 243: @@
          \mathbf{repeat}\, I \,\mathbf{until}\, b  \,\,|\,\,
          \mathbf{for}\, x := e_1 \,\mathbf{to}\, e_2 \,\mathbf{do}\, I  \,\,|\,\,
-         \,\mathbf{do}\, I e \, \,\mathbf{times}  \,\,|\,\,
+         \,\mathbf{do}\, e \,\mathbf{times}\, I  \,\,|\,\,
          \,\mathbf{do}\, I \,\mathbf{while}\, b
 </math>
 Napisz semantykę małych kroków dla powyższych konstrukcji.
+}}
-==== Rozwiązanie ====
+<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>,'''
+<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>
+<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>
+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'}
+     {\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}}
+     {\mathbf{repeat}\, I \,\mathbf{until}\, b, s \,\Longrightarrow, s'}
+\quad \quad
+\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'}
 </math>
-Po drugie, spróbujmy odwołać się do <math> \,\Longrightarrow\,^{*} </math> dla dozoru pętli
+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!
-<math> b </math>:
+Czyli takie podejście jest teraz nieskuteczne.
- <math>
+<br>
-\frac{I, s \,\Longrightarrow\, I', s'}
+'''Instrukcja <math>\,\mathbf{do}\, e \,\mathbf{times}\, I</math>'''
-     {\mathbf{repeat}\, I \,\mathbf{until}\, b, s \,\Longrightarrow\, \mathbf{repeat}\, I' \,\mathbf{until}\, b, s'}
+<br>
+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>.
+Czyli najpierw obliczmy <math>e</math> przy pomocy reguły:
+<math>
+\frac{e, s \,\Longrightarrow, e', s}
+     {\,\mathbf{do}\, e \,\mathbf{times}\, I, s \,\Longrightarrow, D e' \,\mathbf{times}\, I, s}
 </math>
- <math>
+która doprowadza nas do konfiguracji:
-\frac{I, s \,\Longrightarrow\, s' \quad b, s \,\Longrightarrow\,^{*} \mathbf{true}}
-     {\mathbf{repeat}\, I \,\mathbf{until}\, b, s \,\Longrightarrow\, s'}
+<math>
-\quad \quad
+\,\mathbf{do}\, n \,\mathbf{times}\, I, s</math>
-\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'}
+Teraz jest już łatwo:
+<math>
+\,\mathbf{do}\, n \,\mathbf{times}\, I, s \,\Longrightarrow, I; \,\mathbf{do}\, n{-}1 \,\mathbf{times}\, I, s
+\quad \mbox{ o ile } n > 0
 </math>
-Okazuje się, że jest jeszcze gorzej niż w przypadku pętli <math> \mathbf{while}\, </math>:
+<math>
-nie pamiętamy już, jaka była instrukcja wewnętrzna naszej pętli!
+\,\mathbf{do}\, n \,\mathbf{times}\, I, s \,\Longrightarrow, s
+\quad \mbox{ o ile } n = 0</math>
+<br>
+'''Instrukcja <math>\mathbf{for}\ </math>,'''
+<br>
+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.
+Dodatkowo ustalmy, że np. <math>e_1</math> będzie obliczone jako pierwsze.
+Następnie podstawiamy wartość <math>e_1</math> na zmienną <math>x</math>.
+Czyli:
+<math>
+\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}
+</math>
+<math>
+\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}
+</math>
-.....
+Zatem zakres zmiennej <math>x</math> mamy już obliczony, tzn. jesteśmy w konfiguracji
+<math>
+\mathbf{for}\, x = n_1 \,\mathbf{to}\, n_2 \,\mathbf{do}\, I, s</math>
+Dalsze reguły mogą być podobne do reguł dla pętli <math>\,\mathbf{do}\, n \,\mathbf{times}\, I</math>:
-Semantykę dla <math> \,\mathbf{do}\, I \mathbf{while}\, b </math> pozostawiamy Czytelnikowi jako
+<math>
-ćwiczenie.
+\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]
-Oczywiście minimalistyczne rozwiązanie to
+\quad \mbox{ o ile } n_1 \leq n_2
+</math>
- <math>
+<math>
-\,\mathbf{do}\, I \,\mathbf{while}\, b, s \,\Longrightarrow\, \mathbf{repeat}\, I \,\mathbf{until}\, \neg b, 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ą.
+'''Pytanie:''' oto inna wersja jednej z powyższych reguł:
+<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 s(x)+1]
+\quad \mbox{ o ile } s(x) \leq n_2</math>
+Czy semantyka jest taka sama?
+(Rozważ sytuację, gdy zmienna <math>x</math> jest zmieniana przez instrukcję <math>I</math>.)
+'''Pytanie:''' 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 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</math>
+</div></div>
 == Kalkulator binarny ==
-==== Zadanie 1 ====
+{{cwiczenie|3|cw3|
 Rozważmy następujący język wyrażeń (liczby binarne z dodawaniem):
@@ Linia 284: / Linia 385: @@
 </math>
-<math> \epsilon </math> oznacza słowo puste, czyli np. <math> \epsilon 1 0 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ę 101.
 Napisz semantykę operacyjną obliczającą wartość wyrażeń.
+}}
-==== Rozwiązanie ====
+<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>
+<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>
+<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>
+<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?
- <math>
+<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:
- <math>
+<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 338: / Linia 439: @@
 (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 potrzebujemy reguły:
+<math>
+\epsilon + \epsilon \,\Longrightarrow, \epsilon</math>
 Gdy jeden ze składników ma mniej cyfr niż drugi, potrzebujemy reguł:
- <math>
+<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>
 oraz ich odpowiedników:
- <math>
+<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:
- <math>
+<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>
+<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|
-==== Zadanie 2 ====
+Rozszerzmy składnię o jeden symbol <math>p</math> oznaczający "przepełnienie":
-Rozszerzmy składnię o jeden symbol <math> p </math> oznaczający
-''przepełnienie'':
 <math>
 e \, ::= \,\,
@@ Linia 396: / Linia 501: @@
        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ą wartość wyrażenia wraz z informacja o ewentualnym przepełnieniu.
+Wynik powinien byc poprawny przynajmniej dla wyrażeń <math>e</math> w składni ograniczonej:
+<math>
+e \, ::= \,\,
+      b  \,\,|\,\,
        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
+<math>
-informacja o ewentualnym przepełnieniu.
+b \, ::= \,\,
-Wynik powinien byc poprawny przynajmniej dla wyrażeń w składni
+      \epsilon  \,\,|\,\,
-ograniczonej.
+      b 0  \,\,|\,\,
+      b 1</math>
+reprezentujących sumę liczb binarnych.
+}}
-==== Rozwiązanie ====
+<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">
-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>
+<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>
+<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.
-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>
+<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ż
-drugi składnik ma wystarczająco dużo cyfr by je przesłonić.
 Oto odpowiednie reguły:
- <math>
+<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
-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
- <math>
+<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.
+</div></div>
+== Zadania domowe ==
+{{cwiczenie|1|cw1.dom|
-Nowy sztuczny składnik <math> p 1 </math> zawiera jakby na wszelki wypadek
+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.
-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.
+{{cwiczenie|2|cw2.dom|
-== Zadania domowe ==
+Zmodyfikuj semantykę wyrażeń następująco: dla każdego podwyrażenia niedeterministycznie wybierana jest strategia lewo- albo prawostronna, ale niedozwolony jest "przeplot".
+}}
-==== Zadanie 1 ====
+{{cwiczenie|3|cw3.dom|
-Podaj przykład wyrażenia, które nie policzy się
+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.
-ani przy użyciu strategii lewo- ani prawostronnej, a policzy się przy strategii
+}}
-równoległej.
-==== Zadanie 2 ====
+{{cwiczenie|4|cw4.dom|
 Dodaj do wyrażeń binarnych operację odejmowania.
+}}
+{{cwiczenie|5|cw15.dom|
+Zaproponuj semantykę przypisania równoległego w języku TINY:
+<math>
+x_1 := e_1 || \ldots || x_n := e_n
+</math>
+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>.
+}}