Semantyka i weryfikacja programów/Ćwiczenia 3: Różnice pomiędzy wersjami
Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
Nie podano opisu zmian |
Nie podano opisu zmian |
||
| Linia 7: | Linia 7: | ||
wyrażeń boolowskich i arytmetycznych i semantykę dla | wyrażeń boolowskich i arytmetycznych i semantykę dla | ||
błędów wykonania. | błędów wykonania. | ||
Wreszcie dodamy instrukcję pętli <math> \mathbf{loop}\, </math> | Wreszcie dodamy nową instrukcję pętli <math>\mathbf{loop}\,</math> pozwalającą na | ||
niestrukturalne przerwanie lub wznowienie iteracji (instrukcje <math>\mathbf{exit}</math> i <math>\mathbf{continue}</math>). | |||
| Linia 14: | Linia 14: | ||
{{cwiczenie|1|cw1| | |||
Zdefiniuj znaczenie wyrażeń boolowskich i arytmetycznych | Zdefiniuj znaczenie wyrażeń boolowskich i arytmetycznych | ||
w języku Tiny, w stylu dużych kroków (semantyka naturalna). | w języku Tiny, w stylu dużych kroków (semantyka naturalna). | ||
}} | |||
{{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 37: | Linia 39: | ||
l \, ::= \,\, | l \, ::= \,\, | ||
\mathbf{true} \,\,|\,\, | \mathbf{true} \,\,|\,\, | ||
\mathbf{ | \mathbf{false} | ||
</math> | </math> | ||
| Linia 55: | Linia 57: | ||
</math> | </math> | ||
Chcemy, aby tranzycje | Chcemy, aby tranzycje wyrażeń wyglądały następująco: | ||
<math> | <math> | ||
| Linia 63: | Linia 65: | ||
</math> | </math> | ||
gdzie <math> s \in \mathbf{State} </math>, <math> n \in </math> jest liczbą całkowitą, | gdzie <math>s \in \mathbf{State}</math>, <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>. | ||
Tranzycja taka oznacza, że wyrażenie <math> e </math> w stanie <math> s </math> wylicza się do | Tranzycja taka oznacza, że wyrażenie <math>e</math> w stanie <math>s</math> wylicza się do | ||
wartości <math> n </math> oraz analogicznie, wyrażenie logiczne <math> b </math> w | wartości <math>n</math> oraz analogicznie, wyrażenie logiczne <math>b</math> w | ||
stanie <math> s </math> wylicza się do <math> l </math>. | stanie <math>s</math> wylicza się do <math>l</math>. | ||
Zatem zbiór konfiguracji dla semantyki całego języka Tiny to znów | Zatem zbiór konfiguracji dla semantyki całego języka Tiny to znów | ||
| Linia 74: | Linia 76: | ||
\mathbf{Num} \, \cup \, \mathbf{Bool} \, \cup \, \mathbf{State} | \mathbf{Num} \, \cup \, \mathbf{Bool} \, \cup \, \mathbf{State} | ||
</math> | </math> | ||
a konfiguracje końcowe to <math> \mathbf{State} </math> tak jak poprzednio. | a konfiguracje końcowe to <math>\mathbf{State}</math> tak jak poprzednio. | ||
Tranzycje dla instrukcji pozostają zasadniczo bez zmian, z tym, | Tranzycje dla instrukcji pozostają zasadniczo bez zmian, z tym, | ||
że odwołania do funkcji semantycznych dla wyrażen zastępujemy | że odwołania do funkcji semantycznych dla wyrażen zastępujemy | ||
| Linia 86: | Linia 88: | ||
<math> | <math> | ||
\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 109: | Linia 111: | ||
</math> | </math> | ||
Czyli aby obliczyć sumę <math> e_1 + e_2 </math> w stanie | Czyli aby obliczyć sumę <math>e_1 + e_2</math> w stanie | ||
<math> s </math>, trzeba najpierw obliczyć <math> e_1 </math> i | <math>s</math>, trzeba najpierw obliczyć <math>e_1</math> i | ||
<math> e_2 </math> w tym stanie, a następnie dodać obliczone wartości. | <math>e_2</math> w tym stanie, a następnie dodać obliczone wartości. | ||
Zauważmy, że nie specyfikujemy kolejności, w jakiej mają się | Zauważmy, że nie specyfikujemy kolejności, w jakiej mają się | ||
obliczać obydwa podwyrażenia. | obliczać obydwa podwyrażenia. | ||
| Linia 131: | Linia 133: | ||
<math> | <math> | ||
\frac{b_1, s \,\longrightarrow\, \mathbf{ | \frac{b_1, s \,\longrightarrow\, \mathbf{false}} | ||
{b_1 \land b_2, s \,\longrightarrow\, \mathbf{ | {b_1 \land b_2, s \,\longrightarrow\, \mathbf{false}} | ||
\quad \quad | |||
\frac{b_1, s \,\longrightarrow\, \mathbf{true} \quad \quad | \frac{b_1, s \,\longrightarrow\, \mathbf{true} \quad \quad | ||
b_2, s \,\longrightarrow\, l} | b_2, s \,\longrightarrow\, l} | ||
| Linia 140: | Linia 142: | ||
Inny wariant to wariant prawo-stronny ( | Inny wariant to wariant prawo-stronny ( | ||
najpierw <math> b_2 </math>, potem <math> b_1 </math>). | najpierw <math>b_2</math>, potem <math>b_1</math>). | ||
Wreszcie rozważmy kombinację obydwu semantyk (reguły ''równoległe''): | Wreszcie rozważmy kombinację obydwu semantyk (reguły ''równoległe''): | ||
<math> | <math> | ||
\frac{b_1, s \,\longrightarrow\, \mathbf{ | \frac{b_1, s \,\longrightarrow\, \mathbf{false}} | ||
{b_1 \land b_2, s \,\longrightarrow\, \mathbf{ | {b_1 \land b_2, s \,\longrightarrow\, \mathbf{false}} | ||
\quad \quad \quad | \quad \quad \quad | ||
\frac{b_2, s \,\longrightarrow\, \mathbf{ | \frac{b_2, s \,\longrightarrow\, \mathbf{false}} | ||
{b_1 \land b_2, s \,\longrightarrow\, \mathbf{ | {b_1 \land b_2, s \,\longrightarrow\, \mathbf{false}} | ||
</math> | </math> | ||
Czyli jeśli którekolwiek z podwyrażeń daje wynik <math> \mathbf{ | Czyli jeśli którekolwiek z podwyrażeń daje wynik <math>\mathbf{false}</math>, | ||
to taki wynik zyskuje całe wyrażenie. | to taki wynik zyskuje całe wyrażenie. | ||
Dodatkowo potrzebujemy jeszcze reguły: | Dodatkowo potrzebujemy jeszcze reguły: | ||
| Linia 167: | Linia 169: | ||
ćwiczenie. | ćwiczenie. | ||
</div></div> | |||
}} | |||
{{cwiczenie|2|cw2| | |||
Rozważ dodatkowo operację dzielenia: | Rozważ dodatkowo operację dzielenia: | ||
| Linia 184: | Linia 187: | ||
Oprócz stanu wynikiem programu powinna byc informacja o błędzie, | Oprócz stanu wynikiem programu powinna byc informacja o błędzie, | ||
jeśli błąd wystąpił. | jeśli błąd wystąpił. | ||
}} | |||
{{rozwiazanie||roz2| | |||
<div class="mw-collapsible mw-made=collapsible mw-collapsed"><div class="mw-collapsible-content" style="display:none"> | |||
Dopóki nie wystąpi błąd dzielenia przez zero, semantyka programu | Dopóki nie wystąpi błąd dzielenia przez zero, semantyka programu | ||
| Linia 199: | Linia 204: | ||
Zaczynamy od pierwszego punktu. | Zaczynamy od pierwszego punktu. | ||
W tym celu dodajemy do konfiguracji jedną konfigurację końcową | W tym celu dodajemy do konfiguracji jedną konfigurację końcową | ||
<math> \mathtt{Blad} </math>. | <math>\mathtt{Blad}</math>. | ||
Reguła opisująca powstanie błędu może wyglądać np. tak: | Reguła opisująca powstanie błędu może wyglądać np. tak | ||
(duże i małe kroki): | |||
<math> | <math> | ||
\frac{e_2, s \longrightarrow 0} | \frac{e_2, s \,\longrightarrow\, 0} | ||
{e_1 / e_2, s \longrightarrow Blad} | {e_1 / e_2, s \,\longrightarrow\, \mathtt{Blad}} | ||
\quad \quad | |||
e_1 / 0, s \,\Longrightarrow\, \mathtt{Blad}. | |||
</math> | </math> | ||
| Linia 217: | Linia 225: | ||
<math> | <math> | ||
e_1 / 0, s \Longrightarrow Blad, s | \frac{e_2, s \,\longrightarrow\, 0} | ||
{e_1 / e_2, s \,\longrightarrow\, \mathtt{Blad}, s} | |||
\quad \quad | |||
e_1 / 0, s \,\Longrightarrow\, \mathtt{Blad}, s | |||
</math> | </math> | ||
i zamiast pojedyńczej konfiguracji końcowej <math> \mathtt{Blad} </math> potrzebowalibyśmy | i zamiast pojedyńczej konfiguracji końcowej <math>\mathtt{Blad}</math> potrzebowalibyśmy | ||
oczywiście całego zbioru <math> \{ \mathtt{Blad} \} \times \mathbf{State} </math>. | oczywiście całego zbioru <math>\{ \mathtt{Blad} \} \times \mathbf{State}</math>. | ||
Przejdźmy teraz do drugiego punktu. Potrzebujemy dodatkowych reguł, | Przejdźmy teraz do drugiego punktu. Potrzebujemy dodatkowych reguł, | ||
| Linia 264: | Linia 275: | ||
{\mathbf{if}\, b \,\mathbf{then}\, I_1 \,\mathbf{else}\, I_2, s \,\longrightarrow\, \mathtt{Blad}} | {\mathbf{if}\, b \,\mathbf{then}\, I_1 \,\mathbf{else}\, I_2, s \,\longrightarrow\, \mathtt{Blad}} | ||
\quad \quad \quad | \quad \quad \quad | ||
\frac{b, s \,\longrightarrow\, \mathbf{ | \frac{b, s \,\longrightarrow\, \mathbf{false} \quad \quad I_2, s \,\longrightarrow\, \mathtt{Blad}} | ||
{\mathbf{if}\, b \,\mathbf{then}\, I_1 \,\mathbf{else}\, I_2, s \,\longrightarrow\, \mathtt{Blad}} | {\mathbf{if}\, b \,\mathbf{then}\, I_1 \,\mathbf{else}\, I_2, s \,\longrightarrow\, \mathtt{Blad}} | ||
</math> | </math> | ||
| Linia 277: | Linia 288: | ||
</math> | </math> | ||
Zwróćmy szczególnie uwagę na ostatnią regułę dla pętli <math>\mathbf{while}\,</math>: | |||
wyraża ona przypadek, gdy błąd został wygenerowany | |||
nie w pierwszym obiegu pętli, ale w którymś z kolejnych. | |||
Musieliśmy rozważyc również ten przypadek, ponieważ wybraliśmy | |||
podejście dużych kroków; w podejściu małych kroków nie byłoby | |||
to zapewne konieczne. | |||
</div></div> | |||
}} | |||
{{cwiczenie|3|cw3| | |||
Rozszerz język Tiny o następującą instrukcję pętli: | Rozszerz język Tiny o następującą instrukcję pętli: | ||
| Linia 291: | Linia 310: | ||
</math> | </math> | ||
<math> \mathbf{loop}\, I </math> to instrukcja pętli, <math> I </math> stanowi instrukcję wewnętrzną. | <math>\mathbf{loop}\, I</math> to instrukcja pętli, <math>I</math> stanowi instrukcję wewnętrzną. | ||
Instrukcja <math> \mathbf{exit} </math> wychodzi z nabliższej pętli <math> \mathbf{loop}\, </math> | Instrukcja <math>\mathbf{exit}</math> wychodzi z nabliższej pętli <math>\mathbf{loop}\,</math> | ||
i kontynuuje wykonanie programu od pierwszej instrukcji za tą pętlą. | i kontynuuje wykonanie programu od pierwszej instrukcji za tą pętlą. | ||
Instrukcje <math> \mathbf{continue} </math> powraca na początek instrukcji wewnętrznej | Instrukcje <math>\mathbf{continue}</math> powraca na początek instrukcji wewnętrznej | ||
najbliższej pętli. | najbliższej pętli. | ||
Pozważ zarówno semantykę naturalną jak i semantykę małych kroków. | Pozważ zarówno semantykę naturalną jak i semantykę małych kroków. | ||
}} | |||
{{rozwiazanie||roz3.1|(semantyka naturalna) | |||
<div class="mw-collapsible mw-made=collapsible mw-collapsed"><div class="mw-collapsible-content" style="display:none"> | |||
Dodamy do reguł semantyki naturalnej dla języka Tiny | Dodamy do reguł semantyki naturalnej dla języka Tiny | ||
kilka nowych reguł opisujących nową konstrukcję języka | kilka nowych reguł opisujących nową konstrukcję języka | ||
i jej | i jej ,,interakcję\'' z pozostałymi konstrukcjami. | ||
Pomysł polega na dodaniu specjalnych konfiguracji zawierających | Pomysł polega na dodaniu specjalnych konfiguracji zawierających | ||
informację o tym, że została wykonana instrukcja <math> \mathbf{exit} </math> | informację o tym, że została wykonana instrukcja <math>\mathbf{exit}</math> | ||
lub <math> \mathbf{continue} </math>. Oto odpowiednie reguły: | lub <math>\mathbf{continue}</math>. Oto odpowiednie reguły: | ||
<math> | <math> | ||
| Linia 318: | Linia 338: | ||
</math> | </math> | ||
Czyli instrukcje <math> \mathbf{exit} </math> i <math> \mathbf{continue} </math> nie modyfikują | Czyli instrukcje <math>\mathbf{exit}</math> i <math>\mathbf{continue}</math> nie modyfikują | ||
stanu <math> s </math>, ale zostawiają po sobie | stanu <math>s</math>, ale zostawiają po sobie ,,ślad". | ||
Zauważmy, że taki ślad zostaje pozostawiony tylko wtedy, jesli | Zauważmy, że taki ślad zostaje pozostawiony tylko wtedy, jesli | ||
nie było dotychczas innego śladu, to znaczy jeśli <math> \mathbf{exit} </math> | nie było dotychczas innego śladu, to znaczy jeśli <math>\mathbf{exit}</math> | ||
(lub <math> \mathbf{continue} </math>) zostało wykonane w zwykłym stanie <math> s </math>. | (lub <math>\mathbf{continue}</math>) zostało wykonane w zwykłym stanie <math>s</math>. | ||
Oczywiście poszerzamy odpowiednio zbiór konfiguracji o: | Oczywiście poszerzamy odpowiednio zbiór konfiguracji o: | ||
< | <math> | ||
\mathbf{State} \times \{ \mbox{było-}\mathbf{exit}, \mbox{było-}\mathbf{continue} \} | \mathbf{State} \times \{ \mbox{było-}\mathbf{exit}, \mbox{było-}\mathbf{continue} \} | ||
</math> | </math> | ||
'''Pytanie''': jakie powinno być zachowanie <math> \mathbf{exit} </math> i | '''Pytanie''': jakie powinno być zachowanie <math>\mathbf{exit}</math> i | ||
<math> \mathbf{continue} </math> w konfiguracji <math> s, \mbox{było-}\mathbf{exit} </math> | <math>\mathbf{continue}</math> w konfiguracji <math>s, \mbox{było-}\mathbf{exit}</math> | ||
lub <math> s, \mbox{było-}\mathbf{continue} </math>? | lub <math>s, \mbox{było-}\mathbf{continue}</math>? | ||
Czy instrukcje <math> \mathbf{exit} </math> i <math> \mathbf{continue} </math> | Czy instrukcje <math>\mathbf{exit}</math> i <math>\mathbf{continue}</math> | ||
będą faktycznie wykonywane w takich konfiguracjach? | będą faktycznie wykonywane w takich konfiguracjach? | ||
Zapiszmy teraz jak inne instrukcje korzystają z dodatkowej informacji | Zapiszmy teraz jak inne instrukcje korzystają z dodatkowej informacji | ||
(śladu) zawartej w konfiguracjach. | (śladu) zawartej w konfiguracjach. | ||
Oczywiście beneficjentem tej informacji jest instrukcji <math> \mathbf{loop}\, </math>: | Oczywiście beneficjentem tej informacji jest instrukcji <math>\mathbf{loop}\,</math>: | ||
<math> | <math> | ||
| Linia 348: | Linia 368: | ||
Czyli w zależności od tego, jaki ślad został zarejestrowany | Czyli w zależności od tego, jaki ślad został zarejestrowany | ||
podczas wykonania <math> I </math>, albo kończymy wykonanie pętli <math> \mathbf{loop}\, </math>, | podczas wykonania <math>I</math>, albo kończymy wykonanie pętli <math>\mathbf{loop}\,</math>, | ||
albo rozpoczynamy kolejną iterację. | albo rozpoczynamy kolejną iterację. | ||
Zauważmy, że stan <math> s' </math> może być różny od <math> s </math>, ponieważ | Zauważmy, że stan <math>s'</math> może być różny od <math>s</math>, ponieważ | ||
zanim wykonała się ktoraś z instrukcji <math> \mathbf{exit} </math> lub | zanim wykonała się ktoraś z instrukcji <math>\mathbf{exit}</math> lub | ||
<math> \mathbf{continue} </math>, mogły zostać zmienione wartości niektórych zmiennych. | <math>\mathbf{continue}</math>, mogły zostać zmienione wartości niektórych zmiennych. | ||
Oczywiście, jeśli instrukcja wewnętrzna <math> I </math> zakończyła się | Oczywiście, jeśli instrukcja wewnętrzna <math>I</math> zakończyła się | ||
''normalnie'', kontynuujemy wykonanie pętli podobnie jak w przypadku | ''normalnie'', kontynuujemy wykonanie pętli podobnie jak w przypadku | ||
wywołania <math> \mathbf{continue} </math>: | wywołania <math>\mathbf{continue}</math>: | ||
<math> | <math> | ||
| Linia 374: | Linia 394: | ||
Okazuje się że nie, ponieważ ślad powinien zostać zawsze | Okazuje się że nie, ponieważ ślad powinien zostać zawsze | ||
,,wymazany" przez pętlę <math>\mathbf{loop}\,</math>. | |||
<!-- | |||
Poza tym reguły te wykraczałyby poza klasyczna podejście semantyki | Poza tym reguły te wykraczałyby poza klasyczna podejście semantyki | ||
naturalnej, w którym zwykle bezpośrednio definiujemy | naturalnej, w którym zwykle bezpośrednio definiujemy | ||
tranzycje postaci <math> I, s \,\longrightarrow\, s' </math>. | tranzycje postaci <math>I, s \,\longrightarrow\, s'</math>. | ||
--> | |||
Teraz musimy określić zachowanie wszystkich instrukcji w sytuacji, | Teraz musimy określić zachowanie wszystkich instrukcji w sytuacji, | ||
| Linia 383: | Linia 405: | ||
zaniechać wykonania instrukcji (w przypadku pętli, powinniśmy | zaniechać wykonania instrukcji (w przypadku pętli, powinniśmy | ||
zaniechać dalszego iterowania tej pętli). | zaniechać dalszego iterowania tej pętli). | ||
Oto odpowiednie reguły dla <math> \mbox{było-}\mathbf{exit} </math>: | Oto odpowiednie reguły dla <math>\mbox{było-}\mathbf{exit}</math>: | ||
<math> | <math> | ||
| Linia 397: | Linia 419: | ||
{\mathbf{if}\, b \,\mathbf{then}\, I_1 \,\mathbf{else}\, I_2, s \,\longrightarrow\, s', \mbox{było-}\mathbf{exit}} | {\mathbf{if}\, b \,\mathbf{then}\, I_1 \,\mathbf{else}\, I_2, s \,\longrightarrow\, s', \mbox{było-}\mathbf{exit}} | ||
\quad \quad | \quad \quad | ||
\frac{b, s \,\longrightarrow\, \mathbf{ | \frac{b, s \,\longrightarrow\, \mathbf{false} \quad \quad I_2, s \,\longrightarrow\, s', \mbox{było-}\mathbf{exit}} | ||
{\mathbf{if}\, b \,\mathbf{then}\, I_1 \,\mathbf{else}\, I_2, s \,\longrightarrow\, s', \mbox{było-}\mathbf{exit}} | {\mathbf{if}\, b \,\mathbf{then}\, I_1 \,\mathbf{else}\, I_2, s \,\longrightarrow\, s', \mbox{było-}\mathbf{exit}} | ||
</math> | </math> | ||
| Linia 410: | Linia 432: | ||
</math> | </math> | ||
Pominęliśmy zupełnie analogiczne reguły dla | Pominęliśmy zupełnie analogiczne reguły dla <math>\mbox{było-}\mathbf{continue}</math>. | ||
<math> | Zauważmy, że dla pętli <math>\mathbf{while}\,</math> nie rozpatrujemy przypadku, | ||
gdy dozór <math>b</math> oblicza się do <math>\mathbf{false}</math>, gdyż w tym przypadku | |||
Zauważmy | |||
gdy dozór <math> b </math> oblicza się do <math> \mathbf{ | |||
nie ma możliwości wygenerowania śladu. | nie ma możliwości wygenerowania śladu. | ||
| Linia 425: | Linia 440: | ||
</div></div> | |||
}} | |||
{{rozwiazanie||roz3.2|(małe kroki) | |||
==== | <div class="mw-collapsible mw-made=collapsible mw-collapsed"><div class="mw-collapsible-content" style="display:none"> | ||
W semantyce naturalnej musieliśmy napisać wiele reguł aby | W semantyce naturalnej musieliśmy napisać wiele reguł aby | ||
| Linia 460: | Linia 476: | ||
</math> | </math> | ||
Nie musimy zajmowac się przypadkiem, gdy ślad | |||
powstaje w <math> I_2 </math>, bo wybraliśmy podejście mało-krokowe. | powstaje w <math>I_2</math>, bo wybraliśmy podejście mało-krokowe. | ||
Ponadto, nie musimy opisywać instrukcji warunkowej i pętli <math> \mathbf{while}\, </math>, | Ponadto, nie musimy opisywać instrukcji warunkowej i pętli <math>\mathbf{while}\,</math>, | ||
ponieważ ślad nie może powstać podczas | ponieważ ślad nie może powstać podczas obliczania dozoru! | ||
Wreszcie zobaczmy jak zachowuje się pętla <math> \mathbf{loop}\, </math>: | Wreszcie zobaczmy jak zachowuje się pętla <math>\mathbf{loop}\,</math>: | ||
<math> | <math> | ||
| Linia 478: | Linia 494: | ||
sytuacji! | sytuacji! | ||
Natomiast korzystamy z tego, że w podejściu mało-krokowym zmiana konfiguracji | Natomiast korzystamy z tego, że w podejściu mało-krokowym zmiana konfiguracji | ||
na <math> s', \mbox{było-}\mathbf{exit} </math> czy <math> s', \mbox{było-}\mathbf{continue} </math> jest | na <math>s', \mbox{było-}\mathbf{exit}</math> czy <math>s', \mbox{było-}\mathbf{continue}</math> jest | ||
''natychmiast'' widoczna w instrukcji <math> \mathbf{loop}\, I </math>, nawet jeśli | ''natychmiast'' widoczna w instrukcji <math>\mathbf{loop}\, I</math>, nawet jeśli | ||
<math> \mathbf{exit} </math> czy <math> \mathbf{continue} </math> zostało wywołane głęboko wewnątrz | <math>\mathbf{exit}</math> czy <math>\mathbf{continue}</math> zostało wywołane głęboko wewnątrz | ||
<math> I </math>! | <math>I</math>! | ||
Niestety | Niestety powyższe reguły '''nie są poprawne'''! | ||
Dlaczego? Jak zwykle w semantyce małych kroków, wykonując instrukcję | Dlaczego? Jak zwykle w semantyce małych kroków, wykonując instrukcję | ||
wewnętrzną ''zapominamy'' stopniowo jaka była ona na początku. | wewnętrzną ''zapominamy'' stopniowo jaka była ona na początku. | ||
I w związku z tym nie potrafimy poprawnie powrócić do wykonywania | I w związku z tym nie potrafimy poprawnie powrócić do wykonywania | ||
pętli <math> \mathbf{loop}\, </math> po wywołaniu <math> \mathbf{continue} </math>. | pętli <math>\mathbf{loop}\,</math> po wywołaniu <math>\mathbf{continue}</math>. | ||
Prostym sposobem poprawienia naszego blędu jest rozszerzenie składni | Prostym sposobem poprawienia naszego blędu jest rozszerzenie składni | ||
tak, aby możliwe było jednorazowe rozwinięcie pętli <math> \mathbf{loop}\, </math>: | tak, aby możliwe było jednorazowe rozwinięcie pętli <math>\mathbf{loop}\,</math>: | ||
<math> | <math> | ||
| Linia 496: | Linia 512: | ||
</math> | </math> | ||
Teraz możemy zapisać dwie powyższe reguły dla <math> \mathbf{loop}\, </math> w poprawnej | Teraz możemy zapisać dwie powyższe reguły dla <math>\mathbf{loop}\,</math> w poprawnej | ||
wersji, pamiętając o tym, że <math> \mbox{było-}\mathbf{exit} </math> i | wersji, pamiętając o tym, że <math>\mbox{było-}\mathbf{exit}</math> i | ||
<math> \mbox{było-}\mathbf{continue} </math> pojawią się nie w instrukcji wewnętrznej, | <math>\mbox{było-}\mathbf{continue}</math> pojawią się nie w instrukcji wewnętrznej, | ||
ale w jej ''kopii'' umieszczonej przed <math> \,\mathbf{then}\, </math>: | ale w jej ''kopii'' umieszczonej przed <math>\,\mathbf{then}\,</math>: | ||
<math> | <math> | ||
| Linia 506: | Linia 522: | ||
\quad \quad | \quad \quad | ||
\frac{I', s \,\Longrightarrow\, s', \mbox{było-}\mathbf{continue}} | \frac{I', s \,\Longrightarrow\, s', \mbox{było-}\mathbf{continue}} | ||
{I; \,\mathbf{then}\, \mathbf{loop}\, I, s \,\Longrightarrow\, \mathbf{loop}\, I, s'} | |||
\quad \quad | |||
\frac{I', s \,\Longrightarrow\, s'} | |||
{I; \,\mathbf{then}\, \mathbf{loop}\, I, s \,\Longrightarrow\, \mathbf{loop}\, I, s'} | {I; \,\mathbf{then}\, \mathbf{loop}\, I, s \,\Longrightarrow\, \mathbf{loop}\, I, s'} | ||
</math> | </math> | ||
Potrzebujemy też dodatkowej reguły dla obliczeń wewnątrz instrukcji | |||
<math> \mathbf{loop}\, </math> | stojącej przed <math>\,\mathbf{then}\,</math> (w szczególności może ona zawierać | ||
zagnieżdzone pętle <math>\mathbf{loop}\,</math> : | |||
<math> | <math> | ||
| Linia 517: | Linia 537: | ||
</math> | </math> | ||
Na koniec zauważmy, że stan <math> s' </math> w | Na koniec zauważmy, że stan <math>s'</math> w | ||
pierwszych dwóch z powyższych | pierwszych dwóch z powyższych reguł nigdy nie jest różny | ||
od <math> s </math>. Zatem równoważnie moglibyśmy zamienić <math> s' </math> na <math> s </math> | od <math>s</math>. Zatem równoważnie moglibyśmy zamienić <math>s'</math> na <math>s</math> | ||
w powyższych dwóch regułach. Ale wtedy okazuje się , <math> s </math> | w powyższych dwóch regułach. Ale wtedy okazuje się , <math>s</math> | ||
w parze z <math> \mbox{było-}\mathbf{exit} </math> albo <math> \mbox{było-}\mathbf{continue} </math> jest nadmiarowe | w parze z <math>\mbox{było-}\mathbf{exit}</math> albo <math>\mbox{było-}\mathbf{continue}</math> jest nadmiarowe | ||
i może zostać wyeliminowane. | i może zostać wyeliminowane. | ||
| Linia 549: | Linia 569: | ||
\quad \quad | \quad \quad | ||
\frac{I', s \,\Longrightarrow\, \mbox{było-}\mathbf{continue}} | \frac{I', s \,\Longrightarrow\, \mbox{było-}\mathbf{continue}} | ||
{I; \,\mathbf{then}\, \mathbf{loop}\, I, s \,\Longrightarrow\, \mathbf{loop}\, I, s} | |||
\quad \quad | |||
\frac{I', s \,\Longrightarrow\, s'} | |||
{I; \,\mathbf{then}\, \mathbf{loop}\, I, s \,\Longrightarrow\, \mathbf{loop}\, I, s} | {I; \,\mathbf{then}\, \mathbf{loop}\, I, s \,\Longrightarrow\, \mathbf{loop}\, I, s} | ||
</math> | </math> | ||
| Linia 557: | Linia 580: | ||
</math> | </math> | ||
a zbiór konfiguracji poszerzamy tylko o | a zbiór konfiguracji poszerzamy tylko o dwie nowe konfiguracje | ||
<math> \{ \mbox{było-}\mathbf{exit}, \mbox{było-}\mathbf{continue} \} </math>. | <math>\{ \mbox{było-}\mathbf{exit}, \mbox{było-}\mathbf{continue} \}</math>. | ||
</div></div> | |||
}} | |||
| Linia 568: | Linia 592: | ||
==== Zadanie 1 ==== | ==== Zadanie 1 ==== | ||
Zaproponuj semantykę mało-krokową języka | Zaproponuj semantykę mało-krokową dla rozszerzeń języka Tiny, które | ||
studiowaliśmy powyżej. | |||
==== Zadanie 2 ==== | ==== Zadanie 2 ==== | ||
Napisz semantyję naturalną dla nieznacznie rozszerzonej wersji instrukcji <math> \mathbf{loop}\, </math>: | Napisz semantyję naturalną dla nieznacznie rozszerzonej wersji instrukcji <math>\mathbf{loop}\,</math>: | ||
<math> | <math> | ||
I \, ::= \,\, | I \, ::= \,\, | ||
x: \mathbf{loop}\, I \,\,|\,\, | x: \mathbf{loop}\, I \,\,|\,\, | ||
\mathbf{exit} x \,\,|\,\, | \mathbf{exit}\, x \,\,|\,\, | ||
\mathbf{continue} x | \mathbf{continue}\, x | ||
</math> | </math> | ||
Identyfikator <math> x </math> pełni tutaj rolę etykiety przypisanej | Identyfikator <math>x</math> pełni tutaj rolę etykiety przypisanej | ||
instrukcji <math> \mathbf{loop}\, </math>, jest też parametrem dwóch pozostałych | instrukcji <math>\mathbf{loop}\,</math>, jest też parametrem dwóch pozostałych | ||
instrukcji. <math> \mathbf{exit} x </math> kończy teraz najbliższą otaczającą pętlę <math> \mathbf{loop}\, </math> | instrukcji. <math>\mathbf{exit} x</math> kończy teraz najbliższą otaczającą pętlę <math>\mathbf{loop}\,</math> | ||
o etykiecie <math> x </math>. Podobnie <math> \mathbf{continue} x </math> wznawia najbliższą | o etykiecie <math>x</math>. Podobnie <math>\mathbf{continue} x</math> wznawia najbliższą | ||
pętlę o etykiecie <math> x </math>. | otaczającą pętlę o etykiecie <math>x</math>. | ||
===== Przykład ===== | |||
x: <math>\mathbf{loop}\,</math> | |||
a := 1; | |||
y: <math>\mathbf{loop}\,</math> | |||
<math>\mathbf{exit}</math> x; | |||
a := a-10; | |||
a := a+1; | |||
a := a+2; | |||
kończy działanie z wartością zmiennej <math> a = 3 </math>. | Program kończy działanie z wartością zmiennej <math>a = 3</math>. | ||
Za pomocą wcięć określiliśmy, do wnętrza której pętli | |||
<math> \mathbf{loop}\, </math> | <math>\mathbf{loop}\,</math> należy każda z trzech ostatnich instrukcji przypisania. | ||
Niejednoznaczność bierze się oczywiście stąd, że | |||
pracujemy ze składnią abstrakcyjną. Składnia konkretna zawierałaby | pracujemy ze składnią abstrakcyjną. Składnia konkretna zawierałaby | ||
prawdopodobnie jakąś konstukcję ''zamykającą'' pętlę <math> \mathbf{loop}\, </math>, | prawdopodobnie jakąś konstukcję ''zamykającą'' pętlę <math>\mathbf{loop}\,</math>, | ||
np. <math> \mathbf{loop}\, I \,\mathbf{end}\mathbf{loop}\, </math>. | np. <math>\mathbf{loop}\, I \,\mathbf{end}\mathbf{loop}\,</math>. | ||
| Linia 621: | Linia 647: | ||
</math> | </math> | ||
Obliczenie wyrażenia <math> \,\mathbf{do}\, I \,\mathbf{then}\, e </math> polega na wykonaniu <math> I </math> | Obliczenie wyrażenia <math>\,\mathbf{do}\, I \,\mathbf{then}\, e</math> polega na wykonaniu <math>I</math> | ||
a potem na obliczeniu <math> e </math>. Wartość wyrażenia <math> x:= e </math> jest taka | a potem na obliczeniu <math>e</math>. Wartość wyrażenia <math>x:= e</math> jest taka | ||
jak wartość wyrażenia <math> e </math> a efektem ubocznym jest | jak wartość wyrażenia <math>e</math> a efektem ubocznym jest | ||
podstawienie tej wartości na zmienną <math> x </math>. | podstawienie tej wartości na zmienną <math>x</math>. | ||
Wersja z 08:12, 8 sie 2006
Zawartość
Kończymy semantykę małych kroków i rozpoczynamy semantykę naturalną (duże kroki). Uzupełnimy semantykę naturalną języka Tiny o semantykę naturalną dla wyrażeń boolowskich i arytmetycznych i semantykę dla błędów wykonania. Wreszcie dodamy nową instrukcję pętli pozwalającą na niestrukturalne przerwanie lub wznowienie iteracji (instrukcje i ).
Rozszerzenia semantyki języka Tiny
Ćwiczenie 1
Zdefiniuj znaczenie wyrażeń boolowskich i arytmetycznych w języku Tiny, w stylu dużych kroków (semantyka naturalna).
Rozwiązanie
{{{3}}}
Ćwiczenie 2
Rozważ dodatkowo operację dzielenia:
i rozszerz semantykę z poprzedniego zadania. Dzielenie przez zero jest błądem i kończy natychmiast wykonanie programu. Oprócz stanu wynikiem programu powinna byc informacja o błędzie, jeśli błąd wystąpił.
Rozwiązanie
{{{3}}}
Ćwiczenie 3
Rozszerz język Tiny o następującą instrukcję pętli:
to instrukcja pętli, stanowi instrukcję wewnętrzną. Instrukcja wychodzi z nabliższej pętli i kontynuuje wykonanie programu od pierwszej instrukcji za tą pętlą. Instrukcje powraca na początek instrukcji wewnętrznej najbliższej pętli.
Pozważ zarówno semantykę naturalną jak i semantykę małych kroków.
Rozwiązanie
{{{3}}}
Rozwiązanie
{{{3}}}
Zadania domowe
Zadanie 1
Zaproponuj semantykę mało-krokową dla rozszerzeń języka Tiny, które studiowaliśmy powyżej.
Zadanie 2
Napisz semantyję naturalną dla nieznacznie rozszerzonej wersji instrukcji :
Identyfikator pełni tutaj rolę etykiety przypisanej instrukcji , jest też parametrem dwóch pozostałych instrukcji. kończy teraz najbliższą otaczającą pętlę o etykiecie . Podobnie wznawia najbliższą otaczającą pętlę o etykiecie .
Przykład
x:
a := 1;
y:
x;
a := a-10;
a := a+1;
a := a+2;
Program kończy działanie z wartością zmiennej .
Za pomocą wcięć określiliśmy, do wnętrza której pętli
należy każda z trzech ostatnich instrukcji przypisania.
Niejednoznaczność bierze się oczywiście stąd, że
pracujemy ze składnią abstrakcyjną. Składnia konkretna zawierałaby
prawdopodobnie jakąś konstukcję zamykającą pętlę ,
np. .
Zadanie 3
Napisz semantykę naturalną i mało-krokową dla rozszerzenia języka Tiny o wyrażenia z efektami ubocznymi:
Obliczenie wyrażenia polega na wykonaniu a potem na obliczeniu . Wartość wyrażenia jest taka jak wartość wyrażenia a efektem ubocznym jest podstawienie tej wartości na zmienną .
