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

Wersja z 08:54, 7 sie 2006

Zawartość

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

Rozszerzenia semantyki języka Tiny

Zadanie 1

Semantyka języka Tiny z wykładu używała funkcji semantycznych $B, E : S t a t e \to S t a t e$ dla okreś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 $𝐍 𝐮 𝐦 s u b s e t e q 𝐄 𝐱 𝐩$ 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 $m k r o k$ 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 twz. przeplocie: Pojedynczy krok polega na wykonaniu jednego kroku obliczenia $b_{1}$ albo jednego kroku obliczenia $b_{2}$ . Zwróćmy też uwagę, że nasze tranzycje nie posiadają teraz własności determinizmu: wyrażenie $b_{1} \land b_{2}$ może wyewoluować w pojedyńczym kroku albo do $b'_{1} \land b_{2}$ albo do $b_{1} \land b'_{2}$ . Na szczęście, końcowy wynik, do jakiego oblicza się wyrażenie jest zawsze taki sam, niezależnie od przeplotu.

Oto reguł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 zadadzie do semantyki dużych kroków):

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

Takie rozwiązanie nie jest zatem czystą semantyką małych kroków. Istnieją inne możliwe rozwiązania w stylu małych kroków. Jedno z nich oparte jest na pomyśle, aby rozwinąc 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.

Zadanie 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 wykonianie 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 juz ł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 $e_{1}$ będzie obliczone jako pierwsze. 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 ⟹ x : = n_{1}; I; 𝐟 𝐨 𝐫 x = n_{1} + 1 𝐭 𝐨 n_{2} 𝐝 𝐨 I, s 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 $n_{2}$ . Ponieważ nie zostało wyspecyfikowane jaka powinna być wartość tej zmiennej, taką semantykę uważamy za poprawną.

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

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

Kalkulator binarny

Zadanie 1

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

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

$ϵ$ oznacza słowo puste, czyli np. $ϵ 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}$

Zadanie 2

Rozszerzmy składnię o jeden symbol $p$ oznaczający przepełnienie:

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

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

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

Rozwiązanie

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

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

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

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

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

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

z poprzedniego zadania są wystarczające.

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

$p + p ⟹ p .$

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

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

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

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

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

Zadania domowe

Zadanie 1

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

Zadanie 2

Rozważ inną semantykę pętli $𝐟 𝐨 𝐫 x = e_{1} 𝐭 𝐨 e_{2} d o I$ , w której wyrażenie $e_{2}$ 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.

Zadanie 3

Dodaj do wyrażeń binarnych operację odejmowania.

Zadanie 4

Zaproponuj semantykę przypisania równoległego

$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 nowych wartości na zmienne $x_{1}, \dots, x_{n}$ .

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

Wersja z 08:54, 7 sie 2006

Spis treści

Zawartość

Rozszerzenia semantyki języka Tiny

Zadanie 1

Rozwiązanie

Zadanie 2

Rozwiązanie

Instrukcja $𝐫 𝐞 𝐩 𝐞 𝐚 𝐭$

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

Instrukcja $𝐟 𝐨 𝐫$

Kalkulator binarny

Zadanie 1

Rozwiązanie

Zadanie 2

Rozwiązanie

Zadania domowe

Zadanie 1

Zadanie 2

Zadanie 3

Zadanie 4

Menu nawigacyjne

Działania na stronie

Opcje strony

Narzędzia osobiste

Nawigacja

Szukaj

Narzędzia

@@ Linia 22: / Linia 22: @@
 Zdefiniuj znaczenie wyrażeń za pomocą semantyki operacyjnej,
 w stylu małych kroków.
 ==== Rozwiązanie ====
 Przypomnijmy składnię wyrażeń boolowskich i arytmetycznych:
@@ Linia 60: / Linia 63: @@
 Chcemy, aby tranzycje dla wyrażeń były postaci:
- <math>
+<math>
 e, s \,\Longrightarrow\, e', s
 </math>
@@ Linia 66: / Linia 69: @@
 i podobnie dla wyrażeń boolowskich:
- <math>
+<math>
 b, s \,\Longrightarrow\, b', s
 </math>
@@ Linia 73: / Linia 76: @@
 Dodatkowo będziemy potrzebować również tranzycji postaci:
- <math>
+<math>
 e, s \,\Longrightarrow\, n
 \quad \quad
@@ Linia 97: / Linia 100: @@
 Zacznijmy od (chyba najprostszych) tranzycji dla stałych boolowskich i liczbowych:
- <math>
+<math>
 l, s \,\Longrightarrow\, l
 \quad \quad
@@ Linia 114: / Linia 117: @@
 obliczać <math> b_1 </math> i <math> b_2 </math>. Zacznijmy od strategii lewostronnej:
- <math>
+<math>
 \frac{b_1, s \,\Longrightarrow\, b'_1, s}
 {b_1 \land b_2, s \,\Longrightarrow\, b'_1 \land b_2, s}
@@ Linia 129: / Linia 132: @@
 Oto odpowiednio zmodyfikowane reguły:
- <math>
+<math>
 \frac{b_1, s \,\Longrightarrow\, b'_1, s}
 {b_1 \land b_2, s \,\Longrightarrow\, b'_1 \land b_2, s}
@@ Linia 140: / Linia 143: @@
 Analogicznie reguły prawostronne to:
- <math>
+<math>
 \frac{b_2, s \,\Longrightarrow\, b'_2, s}
 {b_1 \land b_2, s \,\Longrightarrow\, b_1 \land b'_2, s}
@@ Linia 164: / Linia 167: @@
 Oto reguły dla negacji:
- <math>
+<math>
 \neg \mathbf{true}, s \,\Longrightarrow\, \mathbf{true}, s
 \quad \quad \quad
@@ Linia 175: / Linia 178: @@
 Reguły dla <math> e_1 \leq e_2 </math> są następujące:
- <math>
+<math>
 \frac{e_1, s \,\Longrightarrow\, e'_1, s}
 {e_1 \leq e_2, s \,\Longrightarrow\, e'_1 \leq e_2, s}
@@ Linia 198: / Linia 201: @@
 stan:
- <math>
+<math>
 \frac{e, s \,\Longrightarrow\, e', s}
       {x := e, s \,\Longrightarrow\, x := e', s}
@@ Linia 208: / Linia 211: @@
 Najpierw obliczamy wartość dozoru:
- <math>
+<math>
 \frac{b, s \,\Longrightarrow\, b', s}
 {\mathbf{if}\, b \,\mathbf{then}\, I_1 \,\mathbf{else}\, I_2, s \,\Longrightarrow\,
@@ Linia 220: / Linia 223: @@
 W przypadku instrukcji warunkowej reguły są oczywiste:
- <math>
+<math>
 \mathbf{if}\, \mathbf{true} \,\mathbf{then}\, I_1 \,\mathbf{else}\, I_2, s \,\Longrightarrow\, I_1, s
 \quad \quad
@@ Linia 228: / Linia 231: @@
 Gorzej jest w przypadku instrukcji pętli. Reguła mogłaby wyglądać tak:
- <math>
+<math>
 \mathbf{while}\, \mathbf{true} \,\mathbf{do}\, I, s \,\Longrightarrow\,
 I;\, \mathbf{while}\, ? \,\mathbf{do}\, I, s
@@ Linia 238: / Linia 241: @@
 <math> \,\Longrightarrow\, </math> (czyli w zadadzie do semantyki dużych kroków):
- <math>
+<math>
 \frac{b, s \,\Longrightarrow\,^{*} \mathbf{true}}
 {\mathbf{while}\, b \,\mathbf{do}\, I, s \,\Longrightarrow\,
@@ Linia 254: / Linia 257: @@
 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.
 </math>
@@ Linia 264: / Linia 267: @@
 Reguły dla operacji arytmetycznych również pozostawiamy do napisania Czytelnikowi.
@@ Linia 283: / Linia 288: @@
 ==== Rozwiązanie ====
@@ Linia 292: / Linia 299: @@
 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.
 </math>
@@ Linia 298: / Linia 305: @@
 Po drugie, spróbujmy odwołać się do <math> \,\Longrightarrow\,^{*} </math> dla dozoru pętli <math> b </math>:
- <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>
+<math>
 \frac{I, s \,\Longrightarrow\, s' \quad b, s \,\Longrightarrow\,^{*} \mathbf{true}}
       {\mathbf{repeat}\, I \,\mathbf{until}\, b, s \,\Longrightarrow\, s'}
@@ Linia 323: / Linia 330: @@
 Czyli najpierw obliczmy <math> e </math> przy pomocy reguły:
- <math>
+<math>
 \frac{e, s \,\Longrightarrow\, e', s}
       {\,\mathbf{do}\, e \,\mathbf{times}\, I, s \,\Longrightarrow\, D e' \,\mathbf{times}\, I, s}
@@ Linia 355: / Linia 362: @@
 Czyli:
- <math>
+<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>
+<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}
@@ Linia 368: / Linia 375: @@
 w konfiguracji
- <math>
+<math>
 \mathbf{for}\, x = n_1 \,\mathbf{to}\, n_2 \,\mathbf{do}\, I, s.
 </math>
@@ Linia 374: / Linia 381: @@
 Dalsze reguły mogą być podobne do reguł dla pętli <math> \,\mathbf{do}\, n \,\mathbf{times}\, I </math>:
- <math>
+<math>
 \mathbf{for}\, x = n_1 \,\mathbf{to}\, n_2 \,\mathbf{do}\, I, s \,\Longrightarrow\, x:= n_1; I; \mathbf{for}\, x = n_1+1 \,\mathbf{to}\, n_2 \,\mathbf{do}\, I, s
 \quad \mbox{ o ile } n_1 \leq n_2
 </math>
- <math>
+<math>
 \mathbf{for}\, x = n_1 \,\mathbf{to}\, n_2 \,\mathbf{do}\, I, s \,\Longrightarrow\, \mathbf{skip}, s
 \quad \mbox{ o ile } n_1 > n_2
@@ Linia 395: / Linia 402: @@
 Oczywiście minimalistyczne rozwiązanie to
- <math>
+<math>
 \,\mathbf{do}\, I \,\mathbf{while}\, b, s \,\Longrightarrow\, \mathbf{repeat}\, I \,\mathbf{until}\, \neg b, s
 </math>
@@ Linia 422: / Linia 430: @@
 ==== Rozwiązanie ====
 Składnia wyrażeń pozwala na wygodny dostęp do najmniej znaczącego
@@ Linia 427: / Linia 437: @@
 pisemnego:
- <math>
+<math>
 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
 </math>
- <math>
+<math>
 e_1 1 + e_2 0 \,\Longrightarrow\, (e_1 + e_2) 1
 </math>
@@ Linia 441: / Linia 451: @@
 Ale co zrobić z przeniesieniem?
- <math>
+<math>
 e_1 1 + e_2 1 \,\Longrightarrow\, ?
 </math>
@@ Linia 447: / Linia 457: @@
 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
 </math>
@@ Linia 478: / Linia 488: @@
 potrzebujemy reguły:
- <math>
+<math>
 \epsilon + \epsilon \,\Longrightarrow\, \epsilon.
 </math>
@@ Linia 484: / Linia 494: @@
 Gdy jeden ze składników ma mniej cyfr niż drugi, potrzebujemy reguł:
- <math>
+<math>
 \epsilon + e 0 \,\Longrightarrow\, e 0
 \quad \quad
@@ Linia 492: / Linia 502: @@
 oraz ich odpowiedników:
- <math>
+<math>
 e 0 + \epsilon \,\Longrightarrow\, e 0
 \quad \quad
@@ Linia 500: / Linia 510: @@
 Niestety, nie możemy użyć reguły przemienności:
- <math>
+<math>
 e_1 + e_2 \,\Longrightarrow\, e_2 + e_1
 </math>
@@ Linia 509: / Linia 519: @@
 krok całego wyrażenia:
- <math>
+<math>
 \frac{e_1 \,\Longrightarrow\, e'_1}
       {e_1 + e_2 \,\Longrightarrow\, e'_1 + e_2}
@@ Linia 523: / Linia 533: @@
 \quad \quad
 </math>
@@ Linia 552: / Linia 564: @@
 ==== Rozwiązanie ====
 Zadanie dotyczy w zasadzie składni ograniczonej, ale jako konfiguracji
@@ Linia 569: / Linia 583: @@
 cyfr, i to ten właśnie składnik odnotował przepełnienie:
- <math>
+<math>
 p + e 0 \,\Longrightarrow\, e 0
 \quad \quad
@@ Linia 584: / Linia 598: @@
 cyfr, to reguły
- <math>
+<math>
 \epsilon + e 0 \,\Longrightarrow\, e 0
 \quad \quad
@@ Linia 601: / Linia 615: @@
 powinna zostać zachowana:
- <math>
+<math>
 p + p \,\Longrightarrow\, p.
 </math>
@@ Linia 611: / Linia 625: @@
 Oto odpowiednie reguły:
- <math>
+<math>
 p + \epsilon \,\Longrightarrow\, \epsilon
 \quad \quad
@@ Linia 626: / Linia 640: @@
 Odpowiednia reguła to
- <math>
+<math>
 e_1 1 + e_2 1 \,\Longrightarrow\, ((e_1 + e_2) + p 1) 0.
 </math>
@@ Linia 636: / Linia 650: @@
 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.

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

Wersja z 08:54, 7 sie 2006

Zawartość

Rozszerzenia semantyki języka Tiny

Zadanie 1

Rozwiązanie

Zadanie 2

Rozwiązanie

Instrukcja 𝐫𝐞𝐩𝐞𝐚𝐭

Instrukcja 𝐝𝐨e𝐭𝐢𝐦𝐞𝐬I

Instrukcja 𝐟𝐨𝐫

Kalkulator binarny

Zadanie 1

Rozwiązanie

Zadanie 2

Rozwiązanie

Zadania domowe

Zadanie 1

Zadanie 2

Zadanie 3

Zadanie 4

Menu nawigacyjne

Szukaj

Instrukcja $𝐫 𝐞 𝐩 𝐞 𝐚 𝐭$

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

Instrukcja $𝐟 𝐨 𝐫$