Semantyka i weryfikacja programów/Ćwiczenia 2: Różnice pomiędzy wersjami
Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
Nie podano opisu zmian |
Nie podano opisu zmian |
||
| Linia 1: | Linia 1: | ||
== Zawartość == | == Zawartość == | ||
| Linia 13: | Linia 12: | ||
{{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 | ||
| Linia 22: | Linia 21: | ||
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"><div class="mw-collapsible-content" style="display:none"> | |||
Przypomnijmy składnię wyrażeń boolowskich i arytmetycznych: | Przypomnijmy składnię wyrażeń boolowskich i arytmetycznych: | ||
| Linia 41: | Linia 41: | ||
l \, ::= \,\, | l \, ::= \,\, | ||
\mathbf{true} \,\,|\,\, | \mathbf{true} \,\,|\,\, | ||
\mathbf{ | \mathbf{false} | ||
</math> | </math> | ||
| Linia 59: | Linia 59: | ||
</math> | </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: | ||
| Linia 73: | Linia 73: | ||
</math> | </math> | ||
gdzie <math> s \in \mathbf{State} </math>. | gdzie <math>s \in \mathbf{State}</math>. | ||
Dodatkowo będziemy potrzebować również tranzycji postaci: | Dodatkowo będziemy potrzebować również tranzycji postaci: | ||
| Linia 83: | Linia 83: | ||
b, s \,\Longrightarrow\, l | b, s \,\Longrightarrow\, l | ||
</math> | </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{ | <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 | ||
| Linia 92: | Linia 92: | ||
</math> | </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ę | 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 | dla wyrażeń arytmetycznych i boolowskich jako konfiguracje końcowe dla | ||
instrukcji. | instrukcji. | ||
Przypomnijmy, że <math> \mathbf{Stmt} </math> oznacza zbiór instrukcji, <math> I \in \mathbf{Stmt} </math>. | 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: | ||
| Linia 107: | Linia 107: | ||
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 | Pozwala nam to nie odróżniać stałych występujących w wyrażeniach | ||
a zatem pojawiających się po lewej stonie tranzycji | a zatem pojawiających się po lewej stonie tranzycji | ||
od wartości im odpowiadających pojawiających się po prawej stronie. | 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ę | 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: | obliczać <math>b_1</math> i <math>b_2</math>. Zacznijmy od strategii lewostronnej: | ||
<math> | <math> | ||
| Linia 129: | Linia 129: | ||
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: | ||
| Linia 136: | Linia 136: | ||
{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 | \quad \quad | ||
\mathbf{ | \mathbf{false} \land b_2, s \,\Longrightarrow\, \mathbf{false}, s | ||
\quad \quad | \quad \quad | ||
\mathbf{true} \land b_2, s \,\Longrightarrow\, b_2, s | \mathbf{true} \land b_2, s \,\Longrightarrow\, b_2, s | ||
| Linia 147: | Linia 147: | ||
{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 | \quad \quad | ||
b_1 \land \mathbf{ | b_1 \land \mathbf{false}, s \,\Longrightarrow\, \mathbf{false}, s | ||
\quad \quad | \quad \quad | ||
b_1 \land \mathbf{true}, s \,\Longrightarrow\, b_1, s | b_1 \land \mathbf{true}, s \,\Longrightarrow\, b_1, s | ||
| Linia 154: | Linia 154: | ||
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 | prawostronnych (w sumie 6 reguł). Zauważmy, że obliczanie | ||
wyrażeń <math> b_1 </math> i <math> b_2 </math> odbywa się teraz | wyrażeń <math>b_1</math> i <math>b_2</math> odbywa się teraz | ||
w twz. ''przeplocie | w twz. \''przeplocie": Pojedynczy krok polega na wykonaniu | ||
jednego kroku obliczenia <math> b_1 </math> albo jednego kroku | jednego kroku obliczenia <math>b_1</math> albo jednego kroku | ||
obliczenia <math> b_2 </math>. | obliczenia <math>b_2</math>. | ||
Zwróćmy też uwagę, że nasze tranzycje nie posiadają teraz | Zwróćmy też uwagę, że nasze tranzycje nie posiadają teraz | ||
własności ''determinizmu'': wyrażenie <math> b_1 \land b_2 </math> | własności ''determinizmu'': wyrażenie <math>b_1 \land b_2</math> | ||
może wyewoluować w pojedyńczym kroku albo do | 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>. | <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 | Na szczęście, końcowy wynik, do jakiego oblicza się wyrażenie | ||
jest zawsze taki sam, niezależnie od przeplotu. | jest zawsze taki sam, niezależnie od przeplotu. | ||
| Linia 168: | Linia 168: | ||
<math> | <math> | ||
\neg \mathbf{true}, s \,\Longrightarrow\, \mathbf{ | \neg \mathbf{true}, s \,\Longrightarrow\, \mathbf{false}, s | ||
\quad \quad \quad | \quad \quad \quad | ||
\neg \mathbf{ | \neg \mathbf{false}, s \,\Longrightarrow\, \mathbf{true}, s | ||
\quad \quad \quad | \quad \quad \quad | ||
\frac{b, s \,\Longrightarrow\, b', s} | \frac{b, s \,\Longrightarrow\, b', s} | ||
| Linia 176: | Linia 176: | ||
</math> | </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> | <math> | ||
| Linia 188: | Linia 188: | ||
n_1 \leq n_2 | n_1 \leq n_2 | ||
\quad \quad | \quad \quad | ||
n_1 \leq n_2, s \,\Longrightarrow\, \mathbf{ | n_1 \leq n_2, s \,\Longrightarrow\, \mathbf{false}, s \quad \mbox{ o ile } | ||
n_1 > n_2 | n_1 > n_2 | ||
</math> | </math> | ||
| Linia 194: | Linia 194: | ||
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. | ||
| Linia 226: | Linia 226: | ||
\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 | \quad \quad | ||
\mathbf{if}\, \mathbf{ | \mathbf{if}\, \mathbf{false} \,\mathbf{then}\, I_1 \,\mathbf{else}\, I_2, s \,\Longrightarrow\, I_2, s | ||
</math> | </math> | ||
| Linia 237: | Linia 237: | ||
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 | Możemy odwołać się do tranzytywnego domknięcia relacji | ||
<math> \,\Longrightarrow\, </math> (czyli w zadadzie do semantyki dużych kroków): | <math>\,\Longrightarrow\,</math> (czyli w zadadzie do semantyki dużych kroków): | ||
<math> | <math> | ||
| Linia 246: | Linia 246: | ||
I;\, \mathbf{while}\, b \,\mathbf{do}\, I, s} | I;\, \mathbf{while}\, b \,\mathbf{do}\, I, s} | ||
\quad \quad | \quad \quad | ||
\frac{b, s \,\Longrightarrow\,^{*} \mathbf{ | \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> | </math> | ||
| Linia 254: | Linia 254: | ||
Istnieją inne możliwe rozwiązania w stylu małych kroków. | Istnieją inne możliwe rozwiązania w stylu małych kroków. | ||
Jedno z nich oparte jest na pomyśle, aby ''rozwinąc'' pętlę | Jedno z nich oparte jest na pomyśle, aby ''rozwinąc'' pętlę | ||
<math> \mathbf{while}\, </math>, zanim obliczymy wartość dozoru <math> b </math>. | <math>\mathbf{while}\,</math>, zanim obliczymy wartość dozoru <math>b</math>. | ||
Jedyną reguła dla pętli <math> \mathbf{while}\, </math> byłaby wtedy reguła: | Jedyną reguła dla pętli <math>\mathbf{while}\,</math> byłaby wtedy reguła: | ||
<math> | <math> | ||
| Linia 261: | Linia 261: | ||
</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, | Znalezienie innych rozwiązań, np. opartych na rozszerzeniu składni, | ||
| Linia 268: | Linia 268: | ||
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: | ||
| Linia 284: | Linia 285: | ||
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"> | ||
'''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: | ||
| Linia 303: | Linia 305: | ||
</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> | <math> | ||
| Linia 311: | Linia 313: | ||
<math> | <math> | ||
\frac{I, s \,\Longrightarrow\, s' \quad b, s \,\Longrightarrow\,^{*} \mathbf{ | \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 | \quad \quad | ||
| Linia 318: | Linia 320: | ||
</math> | </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> | |||
'''Instrukcja <math>\,\mathbf{do}\, e \,\mathbf{times}\, I</math>''' | |||
<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 wykonianie instrukcji <math>I</math> | ||
<math> n </math> razy, gdzie <math> n </math> to wartość, do której oblicza się | <math>n</math> razy, gdzie <math>n</math> to wartość, do której oblicza się | ||
<math> e </math> w stanie <math> s </math>. | <math>e</math> w stanie <math>s</math>. | ||
Czyli najpierw obliczmy <math> e </math> przy pomocy reguły: | Czyli najpierw obliczmy <math>e</math> przy pomocy reguły: | ||
<math> | <math> | ||
| Linia 344: | Linia 349: | ||
<math> | <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 | \quad \mbox{ o ile } n > 0 | ||
</math> | </math> | ||
| Linia 354: | Linia 359: | ||
<br> | |||
'''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ą | <math>e_1</math> i <math>e_2</math> obliczane są przed pierwszą iteracją | ||
pętli. | pętli. | ||
Dodatkowo ustalmy, że <math> e_1 </math> będzie obliczone jako pierwsze. | Dodatkowo ustalmy, że <math>e_1</math> będzie obliczone jako pierwsze. | ||
Czyli: | Czyli: | ||
| Linia 372: | Linia 380: | ||
</math> | </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 | ||
| Linia 379: | Linia 387: | ||
</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> | <math> | ||
\mathbf{for}\, x = n_1 \,\mathbf{to}\, n_2 \,\mathbf{do}\, I, s \,\Longrightarrow\, | \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 | \quad \mbox{ o ile } n_1 \leq n_2 | ||
</math> | </math> | ||
<math> | <math> | ||
\mathbf{for}\, x = n_1 \,\mathbf{to}\, n_2 \,\mathbf{do}\, I, s \,\Longrightarrow\ | \mathbf{for}\, x = n_1 \,\mathbf{to}\, n_2 \,\mathbf{do}\, I, s \,\Longrightarrow\, s | ||
\quad \mbox{ o ile } n_1 > n_2 | \quad \mbox{ o ile } n_1 > n_2 | ||
</math> | </math> | ||
Zauważmy, wartość zmiennej <math> x </math> po zakończeniu pętli | Zauważmy, wartość zmiennej <math>x</math> po zakończeniu pętli | ||
wynosi <math> n_2 </math>. Ponieważ nie zostało wyspecyfikowane jaka | wynosi albo <math>n_2</math> albo pozostaje niezmieniona. | ||
powinna być wartość tej zmiennej, taką semantykę | Ponieważ nie zostało wyspecyfikowane jaka | ||
powinna być wartość tej zmiennej, możemy taką semantykę uznać | |||
za poprawną. | za poprawną. | ||
'''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 | |||
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 | ||
| Linia 406: | Linia 420: | ||
</math> | </math> | ||
</div></div> | |||
}} | |||
| Linia 412: | Linia 427: | ||
{{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): | ||
| Linia 424: | Linia 439: | ||
</math> | </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"> | |||
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 | ||
| Linia 462: | Linia 478: | ||
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 | i bitów <math>0, 1</math>. Tę dowolność wykorzystaliśmy właśnie w regułach | ||
powyżej. Gdyby nasz język ograniczyć tylko do składni | powyżej. Gdyby nasz język ograniczyć tylko do składni | ||
| Linia 534: | Linia 550: | ||
</math> | </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'': | ||
| Linia 551: | Linia 568: | ||
</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 | </math>, ale z dodatkową informacją, że podczas jej obliczania nastąpiło | ||
''przepełnienie''. | ''przepełnienie''. | ||
| Linia 562: | Linia 579: | ||
Wynik powinien byc poprawny przynajmniej dla wyrażeń w składni | Wynik powinien byc poprawny przynajmniej dla wyrażeń w składni | ||
ograniczonej. | ograniczonej. | ||
}} | |||
{{rozwiazanie||roz4| | |||
<div class="mw-collapsible mw-made=collapsible mw-collapsed"><div class="mw-collapsible-content" style="display:none"> | |||
Zadanie dotyczy w zasadzie składni ograniczonej, ale jako konfiguracji | Zadanie dotyczy w zasadzie składni ograniczonej, ale jako konfiguracji | ||
pośrednich będziemy zapewne potrzebować wyrażeń wykraczających poza | 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 | 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 | zadaniu. Zatem mamy tu do czynienia z typowym zabiegiem rozszerzania | ||
składni na użytek semantyki operacyjnej (z tym, że rozszerzenie jest | składni na użytek semantyki operacyjnej (z tym, że rozszerzenie jest | ||
| Linia 576: | Linia 595: | ||
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ć | końcowymi wyrażenia bez operatora dodawania (ale teraz mogą to być | ||
np. wyrażenia postaci <math> p 1 0 0 </math>). | np. wyrażenia postaci <math>p 1 0 0</math>). | ||
Spróbujmy pozostawić wszystkie reguły z poprzedniego zadania. | Spróbujmy pozostawić wszystkie reguły z poprzedniego zadania. | ||
Dodamy tylko kilka nowych reguł, odpowiedzialnych za przepełnienie. | Dodamy tylko kilka nowych reguł, odpowiedzialnych za przepełnienie. | ||
| Linia 620: | Linia 639: | ||
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ż | Oczywiście, w tej sytuacji żadnego przepełnienia nie ma, ponieważ | ||
drugi składnik ma wystarczająco dużo cyfr by je przesłonić. | drugi składnik ma wystarczająco dużo cyfr by je przesłonić. | ||
| Linia 644: | Linia 663: | ||
</math> | </math> | ||
Nowy sztuczny składnik <math> p 1 </math> zawiera jakby na wszelki wypadek | Nowy sztuczny składnik <math>p 1</math> zawiera jakby na wszelki wypadek | ||
informacje o potencjalnym przepełnieniu. | informacje o potencjalnym przepełnieniu. | ||
Jeśli którykolwiek z pozostałych składników <math> e_1 </math> i <math> e_2 </math> | Jeśli którykolwiek z pozostałych składników <math>e_1</math> i <math>e_2</math> | ||
ma przynajmniej jedną cyfrę, | ma przynajmniej jedną cyfrę, | ||
to <math> p </math> zostanie usunięte. W przeciwnym wypadku symbol <math> p </math> | to <math>p</math> zostanie usunięte. W przeciwnym wypadku symbol <math>p</math> | ||
i przetrwa i będzie poprawnie informował o sytuacji przepełnienia. | i przetrwa i będzie poprawnie informował o sytuacji przepełnienia. | ||
</div></div> | |||
}} | |||
| Linia 659: | Linia 680: | ||
==== Zadanie 1 ==== | ==== Zadanie 1 ==== | ||
Podaj przykład wyrażenia, 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 | ani przy użyciu strategii lewo- ani prawostronnej, a policzy się przy strategii | ||
równoległej. | równoległej. | ||
| Linia 666: | Linia 687: | ||
==== Zadanie 2 ==== | ==== Zadanie 2 ==== | ||
Rozważ inną semantykę pętli <math> \mathbf{for}\, x = e_1 \,\mathbf{to}\, e_2 do I </math>, | Zmodyfikuj semantykę wyrażeń następująco: dla każdego podwyrażenia niedeterministycznie | ||
w której wyrażenie <math> e_2 </math> jest obliczane na nowo | wybierana jest albo strategia lewo- albo prawostronna, ale | ||
niedozwolony jest ,,przeplot\''. | |||
==== Zadanie 3 ==== | |||
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. | przed każdą iteracją pętli. | ||
Napisz reguły semantyczne dla tej instrukcji, nie odwołując | Napisz reguły semantyczne dla tej instrukcji, nie odwołując | ||
się do innych istrukcji pętli. | się do innych istrukcji pętli. | ||
==== Zadanie | |||
==== Zadanie 4 ==== | |||
Dodaj do wyrażeń binarnych operację odejmowania. | Dodaj do wyrażeń binarnych operację odejmowania. | ||
| Linia 678: | Linia 707: | ||
==== Zadanie | ==== Zadanie 5 ==== | ||
Zaproponuj semantykę przypisania równoległego | Zaproponuj semantykę przypisania równoległego | ||
| Linia 687: | Linia 716: | ||
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 | <math>e_1, \ldots, e_n</math> a następnie na podstawieniu | ||
nowych wartości na zmienne <math> x_1, \ldots, x_n </math>. | nowych wartości na zmienne <math>x_1, \ldots, x_n</math>. | ||
Wersja z 08:10, 8 sie 2006
Zawartość
Ćwiczymy dalej semantykę małych kroków. Uzupełnimy semantykę języka Tiny o semantykę operacyjną wyrażeń boolowskich i arytmetycznych. Następnie rozszerzymy nasz język o róznorodne konstrukcje iteracji. Na koniec zdefiniujemy operacje arytmetyczne liczb binarnych.
Rozszerzenia semantyki języka Tiny
Ćwiczenie 1
Semantyka języka Tiny z wykładu używała funkcji semantycznych dla określenia znaczenia wyrażeń boolowskich i arytmetycznych. Zdefiniuj znaczenie wyrażeń za pomocą semantyki operacyjnej, w stylu małych kroków.
Rozwiązanie
{{{3}}}
Ćwiczenie 2
Rozszerzmy język Tiny o następujące dobrze znane konstrukcje iteracji:
Napisz semantykę małych kroków dla powyższych konstrukcji.
Rozwiązanie
{{{3}}}
Kalkulator binarny
Ćwiczenie 3
Rozważmy następujący język wyrażeń (liczby binarne z dodawaniem):
oznacza słowo puste, czyli np. oznacza binarną liczbę 1011. Napisz semantykę operacyjną obliczającą wartość wyrażeń.
Rozwiązanie
{{{3}}}
Ćwiczenie 4
Rozszerzmy składnię o jeden symbol oznaczający przepełnienie:
Na przykład oznacza tę samą liczbę co , 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
{{{3}}}
Zadania domowe
Zadanie 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.
Zadanie 2
Zmodyfikuj semantykę wyrażeń następująco: dla każdego podwyrażenia niedeterministycznie wybierana jest albo strategia lewo- albo prawostronna, ale niedozwolony jest ,,przeplot\.
Zadanie 3
Rozważ inną semantykę pętli , w której wyrażenie 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 4
Dodaj do wyrażeń binarnych operację odejmowania.
Zadanie 5
Zaproponuj semantykę przypisania równoległego
polegającego na obliczeniu najpierw wartości wyrażeń a następnie na podstawieniu nowych wartości na zmienne .
