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

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
← poprzednia edycjanastępna edycja →
WizualnieWikikod
Sl (dyskusja | edycje)
101 edycji
Nie podano opisu zmian
Sl (dyskusja | edycje)
101 edycji
Nie podano opisu zmian
Linia 1: Linia 1:




== Zawartość ==
== Zawarto¶æ ==


Kończymy semantykę małych kroków i rozpoczynamy semantykę naturalną (duże kroki).
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
Uzupe³nimy semantykê naturaln± jêzyka Tiny o semantykê naturaln±
wyrażeń boolowskich i arytmetycznych i semantykę dla
wyra¿eñ boolowskich i arytmetycznych oraz semantykê b³êdów wykonania.
błędów wykonania.
Wreszcie dodamy now± instrukcjê pêtli <math>\mathbf{loop}\,</math> pozwalaj±c± na   
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>).
niestrukturalne przerwanie lub wznowienie iteracji (instrukcje <math>\mathbf{exit}</math> i <math>\mathbf{continue}</math>).




== Rozszerzenia semantyki języka Tiny ==
== Rozszerzenia semantyki jêzyka Tiny ==




{{cwiczenie|1|cw1|
{{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).
}}
}}


Linia 25: Linia 24:
<div class="mw-collapsible mw-made=collapsible mw-collapsed"><div class="mw-collapsible-content" style="display:none">
<div class="mw-collapsible mw-made=collapsible mw-collapsed"><div class="mw-collapsible-content" style="display:none">


Przypomnijmy składnię wyrażeń boolowskich i arytmetycznych
Przypomnijmy sk³adniê wyra¿eñ boolowskich i arytmetycznych
jezyka Tiny:
jezyka Tiny:


Linia 57: Linia 56:
</math>
</math>


Chcemy, aby tranzycje wyrażeń wyglądały następująco:
Chcemy, aby tranzycje wyra¿eñ wygl±da³y nastêpuj±co:


<math>
<math>
Linia 65: Linia 64:
</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{false} \}</math>.
<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


<math>
<math>
Linia 76: Linia 75:
\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
przez odpowiednie tranzycje.
przez odpowiednie tranzycje.
Np. dla instrukcji pętli będziemy mieć następujące reguły:
Np. dla instrukcji pêtli bêdziemy mieæ nastêpuj±ce regu³y:


<math>
<math>
Linia 93: Linia 92:


Podobnie dla instrukcji warunkowej.
Podobnie dla instrukcji warunkowej.
Teraz zajmiemy się tranzycjami dla wyrażeń.
Teraz zajmiemy siê tranzycjami dla wyra¿eñ.
Zacznijmy od stalych arytmetycznych i boolowskich:
Zacznijmy od stalych arytmetycznych i boolowskich:


Linia 102: Linia 101:
</math>
</math>


Operatory arytmetyczne definiujemy następująco:
Operatory arytmetyczne definiujemy nastêpuj±co:


<math>
<math>
Linia 111: Linia 110:
</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.
I choć tutaj nie ma to żadnego znaczenia, w przyszłości
I choæ tutaj nie ma to ¿adnego znaczenia, w przysz³o¶ci
będzie inaczej, gdy jezyk będzie umożliwiał efekty uboczne  
bêdzie inaczej, gdy jezyk bêdzie umo¿liwia³ efekty uboczne  
podczas obliczania wyrażeń.
podczas obliczania wyra¿eñ.


Podobne reguły można napisać dla pozostałych operacji
Podobne regu³y mo¿na napisaæ dla pozosta³ych operacji
arytmnetycznych, oraz dla spójników logicznych:
arytmnetycznych, oraz dla spójników logicznych:


Linia 130: Linia 129:
</math>
</math>


Oto inny wariant, reguły lewo-stronne (ponieważ rozpoczynamy od ''lewego'' koniunktu):
Oto inny wariant, regu³y lewo-stronne (poniewa¿ rozpoczynamy od ''lewego'' koniunktu):


<math>
<math>
Linia 143: 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>
Linia 153: Linia 152:
</math>
</math>


Czyli jeśli którekolwiek z podwyrażeń daje wynik <math>\mathbf{false}</math>,
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:


<math>
<math>
Linia 163: Linia 162:
</math>
</math>


W naszym prostym języku wszystkie cztery warianty  
W naszym prostym jêzyku wszystkie cztery warianty  
są równoważne.  
s± równowa¿ne.  
Reguły dla pozostałych spójników logicznych, dla
Regu³y dla pozosta³ych spójników logicznych, dla
negacji oraz dla instrukcji przypisania pozostawiamy jako proste
negacji oraz dla instrukcji przypisania pozostawiamy jako proste
ćwiczenie.
æwiczenie.


</div></div>
</div></div>
Linia 175: Linia 174:
{{cwiczenie|2|cw2|
{{cwiczenie|2|cw2|


Rozważ dodatkowo operację dzielenia:
Rozwa¿ dodatkowo operacjê dzielenia:


<math>
<math>
Linia 182: Linia 181:
</math>
</math>


i rozszerz semantykę z poprzedniego zadania.
i rozszerz semantykê z poprzedniego zadania.
Dzielenie przez zero jest błądem i  kończy natychmiast wykonanie
Dzielenie przez zero jest b³±dem i  koñczy natychmiast wykonanie
programu.
programu.
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³.
}}
}}


Linia 194: Linia 193:
<div class="mw-collapsible mw-made=collapsible mw-collapsed"><div class="mw-collapsible-content" style="display:none">
<div class="mw-collapsible mw-made=collapsible mw-collapsed"><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
powinna być identyczna jak w poprzednim zadaniu. Zatem pozostawiamy
powinna byæ identyczna jak w poprzednim zadaniu. Zatem pozostawiamy
wszystkie reguły z poprzedniego zadania.
wszystkie regu³y z poprzedniego zadania.
Dodatkowo potrzebujemy reguł, które opiszą
Dodatkowo potrzebujemy regu³, które opisz±


* kiedy powstaje błąd oraz
* kiedy powstaje b³±d oraz
* jak zachowuje się program po wystąpieniu błędu
* jak zachowuje siê program po wyst±pieniu b³êdu


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):
(du¿e i ma³e kroki):


<math>
<math>
Linia 215: Linia 214:
</math>
</math>


Pomijamy tutaj reguły dla przypadku, gdy <math>e_2</math>
Pomijamy tutaj regu³y dla przypadku, gdy <math>e_2</math>
oblicza się do wartości różnej od zera.
oblicza siê do warto¶ci ró¿nej od zera.
Ponadto dla czytelności przyjęliśmy, że wynikiem tranzycji jest
Ponadto dla czytelno¶ci przyjêli¶my, ¿e wynikiem tranzycji jest
wyłącznie informacja o błędzie, a stan jest zapominany.
wy³±cznie informacja o b³êdzie, a stan jest zapominany.
Bez trudu możnaby wszystkie reguły (zarówno te powyżej jak i te
Bez trudu mo¿naby wszystkie regu³y (zarówno te powy¿ej jak i te
poniżej) zmodyfikować tak, by wraz z
poni¿ej) zmodyfikowaæ tak, by wraz z
informacją o błędzie zwracany był też stan, w którym błąd się
informacj± o b³êdzie zwracany by³ te¿ stan, w którym b³±d siê
pojawił. Np. ostatnia reguła wyglądałaby następująco:
pojawi³. Np. ostatnia regu³a wygl±da³aby nastêpuj±co:


<math>
<math>
Linia 231: Linia 230:
</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³,
które zagwarantują, że błąd, raz pojawiwszy się, propaguje się przez
które zagwarantuj±, ¿e b³±d, raz pojawiwszy siê, propaguje siê przez
wszystkie konstrukcje składniowe, a normalne obliczenie wyrażenia
wszystkie konstrukcje sk³adniowe, a normalne obliczenie wyra¿enia
jest wstrzymame.
jest wstrzymame.


Linia 247: Linia 246:
</math>
</math>


Następnie, błąd w wyrażeniu powinien wstrzymać normalne wykonanie instrukcji:
Nastêpnie, b³±d w wyra¿eniu powinien wstrzymaæ normalne wykonanie instrukcji:


<math>
<math>
Linia 264: Linia 263:
</math>
</math>


I wreszcie błąd powinien propagować się do kolejnych instrukcji:
I wreszcie b³±d powinien propagowaæ siê do kolejnych instrukcji:


<math>
<math>
Linia 288: Linia 287:
</math>
</math>


Zwróćmy szczególnie uwagę na ostatnią regułę dla pętli <math>\mathbf{while}\,</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
wyra¿a ona przypadek, gdy b³±d zosta³ wygenerowany
nie w pierwszym obiegu pętli, ale w którymś z kolejnych.
nie w pierwszym obiegu pêtli, ale w którym¶ z kolejnych.
Musieliśmy rozważyc również ten przypadek, ponieważ wybraliśmy
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
podej¶cie du¿ych kroków; w podej¶ciu ma³ych kroków nie by³oby
to zapewne konieczne.
to zapewne konieczne.


Linia 301: Linia 300:
{{cwiczenie|3|cw3|
{{cwiczenie|3|cw3|


Rozszerz język Tiny o następującą instrukcję pętli:
Rozszerzmy jêzyk Tiny o nastêpuj±c± instrukcjê pêtli:


<math>
<math>
Linia 310: Linia 309:
</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 otaczaj±cej 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
Instrukcja <math>\mathbf{continue}</math> powraca na pocz±tek instrukcji wewnêtrznej
najbliższej pętli.
najbli¿szej otaczaj±cej pêtli <math>\mathbf{loop}\,</math>.


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)
{{rozwiazanie|(semantyka naturalna)|roz3.1|


<div class="mw-collapsible mw-made=collapsible mw-collapsed"><div class="mw-collapsible-content" style="display:none">
<div class="mw-collapsible mw-made=collapsible mw-collapsed"><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 ,,interakcję\'' z pozostałymi konstrukcjami.
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>
\mathbf{exit}, s \,\longrightarrow\, s, \mbox{było-}\mathbf{exit}
\mathbf{exit}, s \,\longrightarrow\, s, \mbox{by³o-}\mathbf{exit}
\quad \quad
\quad \quad
\mathbf{continue}, s \,\longrightarrow\, s, \mbox{było-}\mathbf{continue}.
\mathbf{continue}, s \,\longrightarrow\, s, \mbox{by³o-}\mathbf{continue}.
</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 ,,ślad".  
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>
<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>
\frac{I, s \,\longrightarrow\, s', \mbox{było-}\mathbf{exit}}
\frac{I, s \,\longrightarrow\, s', \mbox{by³o-}\mathbf{exit}}
     {\mathbf{loop}\, I, s \,\longrightarrow\, s'}
     {\mathbf{loop}\, I, s \,\longrightarrow\, s'}
\quad \quad
\quad \quad
\frac{I, s \,\longrightarrow\, s', \mbox{było-}\mathbf{continue} \quad \quad \mathbf{loop}\, I, s' \,\longrightarrow\, s''}
\frac{I, s \,\longrightarrow\, s', \mbox{by³o-}\mathbf{continue} \quad \quad \mathbf{loop}\, I, s' \,\longrightarrow\, s''}
     {\mathbf{loop}\, I, s \,\longrightarrow\, s''}
     {\mathbf{loop}\, I, s \,\longrightarrow\, s''}
</math>
</math>


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 383: Linia 382:
</math>
</math>


'''Pytanie:''' czy potrzebujemy dodatkowo reguł postaci:
'''Pytanie:''' czy potrzebujemy dodatkowo regu³ postaci:


<math>
<math>
\frac{I, s \,\longrightarrow\, s' \quad \quad \mathbf{loop}\, I, s' \,\longrightarrow\, s'', \mbox{było-}\mathbf{exit}}
\frac{I, s \,\longrightarrow\, s' \quad \quad \mathbf{loop}\, I, s' \,\longrightarrow\, s'', \mbox{by³o-}\mathbf{exit}}
     {\mathbf{loop}\, I, s \,\longrightarrow\, s'', \mbox{było-}\mathbf{exit}}
     {\mathbf{loop}\, I, s \,\longrightarrow\, s'', \mbox{by³o-}\mathbf{exit}}
\quad \quad
\quad \quad
\frac{I, s \,\longrightarrow\, s', \mbox{było-}\mathbf{continue} \quad \quad \mathbf{loop}\, I, s' \,\longrightarrow\, s'', \mbox{było-}\mathbf{exit}}
\frac{I, s \,\longrightarrow\, s', \mbox{by³o-}\mathbf{continue} \quad \quad \mathbf{loop}\, I, s' \,\longrightarrow\, s'', \mbox{by³o-}\mathbf{exit}}
     {\mathbf{loop}\, I, s \,\longrightarrow\, s'', \mbox{było-}\mathbf{exit}}
     {\mathbf{loop}\, I, s \,\longrightarrow\, s'', \mbox{by³o-}\mathbf{exit}}
</math>
</math>


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>.
,,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,
gdy bieżąca konfiguracja zawiera już ślad. Zasadniczo, powinniśmy
gdy bie¿±ca konfiguracja zawiera ju¿ ¶lad. Zasadniczo, powinni¶my
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>
\frac{I_1, s \,\longrightarrow\, s', \mbox{było-}\mathbf{exit}}
\frac{I_1, s \,\longrightarrow\, s', \mbox{by³o-}\mathbf{exit}}
     {I_1;\, I_2, s \,\longrightarrow\, s', \mbox{było-}\mathbf{exit}}
     {I_1;\, I_2, s \,\longrightarrow\, s', \mbox{by³o-}\mathbf{exit}}
\quad \quad
\quad \quad
\frac{I_1, s \,\longrightarrow\, s' \quad \quad I_2, s' \,\longrightarrow\, s'', \mbox{było-}\mathbf{exit}}
\frac{I_1, s \,\longrightarrow\, s' \quad \quad I_2, s' \,\longrightarrow\, s'', \mbox{by³o-}\mathbf{exit}}
     {I_1;\, I_2, s \,\longrightarrow\, s'', \mbox{było-}\mathbf{exit}}
     {I_1;\, I_2, s \,\longrightarrow\, s'', \mbox{by³o-}\mathbf{exit}}
</math>
</math>


<math>
<math>
\frac{b, s \,\longrightarrow\, \mathbf{true} \quad \quad I_1, s \,\longrightarrow\, s', \mbox{było-}\mathbf{exit}}
\frac{b, s \,\longrightarrow\, \mathbf{true} \quad \quad I_1, 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}}
\quad \quad
\quad \quad
\frac{b, s \,\longrightarrow\, \mathbf{false} \quad \quad I_2, s \,\longrightarrow\, s', \mbox{było-}\mathbf{exit}}
\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>


<math>
<math>
\frac{b, s \,\longrightarrow\, \mathbf{true} \quad \quad I, s \,\longrightarrow\, s', \mbox{było-}\mathbf{exit}}
\frac{b, s \,\longrightarrow\, \mathbf{true} \quad \quad I, s \,\longrightarrow\, s', \mbox{by³o-}\mathbf{exit}}
     {\mathbf{while}\, b \,\mathbf{do}\, I, s \,\longrightarrow\, s', \mbox{było-}\mathbf{exit}}
     {\mathbf{while}\, b \,\mathbf{do}\, I, s \,\longrightarrow\, s', \mbox{by³o-}\mathbf{exit}}
\quad \quad
\quad \quad
\frac{b, s \,\longrightarrow\, \mathbf{true} \quad \quad I, s \,\longrightarrow\, s' \quad \quad
\frac{b, s \,\longrightarrow\, \mathbf{true} \quad \quad I, s \,\longrightarrow\, s' \quad \quad
       \mathbf{while}\, b \,\mathbf{do}\, I, s' \,\longrightarrow\, s'', \mbox{było-}\mathbf{exit}}
       \mathbf{while}\, b \,\mathbf{do}\, I, s' \,\longrightarrow\, s'', \mbox{by³o-}\mathbf{exit}}
     {\mathbf{while}\, b \,\mathbf{do}\, I, s \,\longrightarrow\, s', \mbox{było-}\mathbf{exit}}
     {\mathbf{while}\, b \,\mathbf{do}\, I, s \,\longrightarrow\, s', \mbox{by³o-}\mathbf{exit}}
</math>
</math>


Pominęliśmy zupełnie analogiczne reguły dla <math>\mbox{było-}\mathbf{continue}</math>.
Pominêli¶my zupe³nie analogiczne regu³y dla <math>\mbox{by³o-}\mathbf{continue}</math>.
Zauważmy, że dla pętli <math>\mathbf{while}\,</math> nie rozpatrujemy przypadku,
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
gdy dozór <math>b</math> oblicza siê do <math>\mathbf{false}</math>, gdy¿ w tym przypadku
nie ma możliwości wygenerowania śladu.
nie ma mo¿liwo¶ci wygenerowania ¶ladu.


Zauważmy, że nasze reguły nie pozwalają na dodanie drugiego (kolejnego) śladu!
Zauwa¿my, ¿e nasze regu³y nie pozwalaj± na dodanie drugiego (kolejnego) ¶ladu!




Linia 444: Linia 443:




{{rozwiazanie||roz3.2|(małe kroki)
{{rozwiazanie|(ma³e kroki)|roz3.2|


<div class="mw-collapsible mw-made=collapsible mw-collapsed"><div class="mw-collapsible-content" style="display:none">
<div class="mw-collapsible mw-made=collapsible mw-collapsed"><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  
zapewnić pomijanie instrukcji w sytuacji, gdy został juz
zapewniæ pomijanie instrukcji w sytuacji, gdy zosta³ juz
zarejestrowany jakiś ślad. Było to dość uciążliwe.
zarejestrowany jaki¶ ¶lad. By³o to do¶æ uci±¿liwe.
Okazuje się, że podejście mało-krokowe oferuje możliwość
Okazuje siê, ¿e podej¶cie ma³o-krokowe oferuje mo¿liwo¶æ
bardziej eleganckiego rozwiązania.
bardziej eleganckiego rozwi±zania.


Punktem startowym sę teraz reguły mało-krokowe dla języka Tiny.
Punktem startowym sê teraz regu³y ma³o-krokowe dla jêzyka Tiny.


Podobnie jak poprzednio rozszerzymy zbiór konfiguracji i podobnie
Podobnie jak poprzednio rozszerzymy zbiór konfiguracji i podobnie
opiszemy, jak powstaje ślad:
opiszemy, jak powstaje ¶lad:


<math>
<math>
\mathbf{exit}, s \,\Longrightarrow\, s, \mbox{było-}\mathbf{exit}
\mathbf{exit}, s \,\Longrightarrow\, s, \mbox{by³o-}\mathbf{exit}
\quad \quad
\quad \quad
\mathbf{continue}, s \,\Longrightarrow\, s, \mbox{było-}\mathbf{continue}.
\mathbf{continue}, s \,\Longrightarrow\, s, \mbox{by³o-}\mathbf{continue}.
</math>
</math>


Ponadto musimy określić sposób, w jaki mały krok  
Ponadto musimy okre¶liæ sposób, w jaki ma³y krok  
mniejszej instrukcji zostaje zamieniony na mały krok
mniejszej instrukcji zostaje zamieniony na ma³y krok
większej. Np.
wiêkszej. Np.


<math>
<math>
\frac{I_1, s \,\Longrightarrow\, s', \mbox{było-}\mathbf{exit}}
\frac{I_1, s \,\Longrightarrow\, s', \mbox{by³o-}\mathbf{exit}}
     {I_1;\, I_2, s \,\Longrightarrow\, s', \mbox{było-}\mathbf{exit}}
     {I_1;\, I_2, s \,\Longrightarrow\, s', \mbox{by³o-}\mathbf{exit}}
\quad \quad
\quad \quad
\mbox{ i analogicznie dla } \mbox{było-}\mathbf{continue}.
\mbox{ i analogicznie dla } \mbox{by³o-}\mathbf{continue}.
</math>
</math>


Nie musimy zajmowac się przypadkiem, gdy ślad
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 obliczania dozoru!
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>
\frac{I, s \,\Longrightarrow\, s', \mbox{było-}\mathbf{exit}}
\frac{I, s \,\Longrightarrow\, s', \mbox{by³o-}\mathbf{exit}}
     {\mathbf{loop}\, I, s \,\Longrightarrow\, s'}
     {\mathbf{loop}\, I, s \,\Longrightarrow\, s'}
\quad \quad
\quad \quad
\frac{I, s \,\Longrightarrow\, s', \mbox{było-}\mathbf{continue}}
\frac{I, s \,\Longrightarrow\, s', \mbox{by³o-}\mathbf{continue}}
     {\mathbf{loop}\, I, s \,\Longrightarrow\, \mathbf{loop}\, I, s'}
     {\mathbf{loop}\, I, s \,\Longrightarrow\, \mathbf{loop}\, I, s'}
</math>
</math>


Reguły te są prawie identyczne do reguł semantyki naturalnej dla tej
Regu³y te s± prawie identyczne do regu³ semantyki naturalnej dla tej
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 powyższe reguły '''nie są poprawne'''!
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 512: Linia 511:
</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>
\frac{I', s \,\Longrightarrow\, s', \mbox{było-}\mathbf{exit}}
\frac{I', s \,\Longrightarrow\, s', \mbox{by³o-}\mathbf{exit}}
     {I' \,\mathbf{then}\, \mathbf{loop}\, I, s \,\Longrightarrow\, s'}
     {I' \,\mathbf{then}\, \mathbf{loop}\, I, s \,\Longrightarrow\, s'}
\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'}
     {I; \,\mathbf{then}\, \mathbf{loop}\, I, s \,\Longrightarrow\, \mathbf{loop}\, I, s'}
\quad \quad
\quad \quad
Linia 528: Linia 527:
</math>
</math>


Potrzebujemy też dodatkowej reguły dla obliczeń wewnątrz instrukcji
Potrzebujemy te¿ dodatkowej regu³y dla obliczeñ wewn±trz instrukcji
stojącej przed <math>\,\mathbf{then}\,</math> (w szczególności może ona zawierać
stoj±cej przed <math>\,\mathbf{then}\,</math> (w szczególno¶ci mo¿e ona zawieraæ
zagnieżdzone pętle <math>\mathbf{loop}\,</math> :
zagnie¿dzone pêtle <math>\mathbf{loop}\,</math> :


<math>
<math>
Linia 537: Linia 536:
</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 reguł nigdy nie jest różny
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.


Zatem ostatecznie nasze reguły mogą wyglądać tak:
Zatem ostatecznie nasze regu³y mog± wygl±daæ tak:


<math>
<math>
\mathbf{exit}, s \,\Longrightarrow\, \mbox{było-}\mathbf{exit}
\mathbf{exit}, s \,\Longrightarrow\, \mbox{by³o-}\mathbf{exit}
\quad \quad
\quad \quad
\mathbf{continue}, s \,\Longrightarrow\, \mbox{było-}\mathbf{continue}
\mathbf{continue}, s \,\Longrightarrow\, \mbox{by³o-}\mathbf{continue}
</math>
</math>


<math>
<math>
\frac{I_1, s \,\Longrightarrow\, \mbox{było-}\mathbf{exit}}
\frac{I_1, s \,\Longrightarrow\, \mbox{by³o-}\mathbf{exit}}
     {I_1;\, I_2, s \,\Longrightarrow\, \mbox{było-}\mathbf{exit}}
     {I_1;\, I_2, s \,\Longrightarrow\, \mbox{by³o-}\mathbf{exit}}
\quad \quad
\quad \quad
\frac{I_1, s \,\Longrightarrow\, \mbox{było-}\mathbf{continue}}
\frac{I_1, s \,\Longrightarrow\, \mbox{by³o-}\mathbf{continue}}
     {I_1;\, I_2, s \,\Longrightarrow\, \mbox{było-}\mathbf{continue}}
     {I_1;\, I_2, s \,\Longrightarrow\, \mbox{by³o-}\mathbf{continue}}
</math>
</math>


Linia 565: Linia 564:


<math>
<math>
\frac{I', s \,\Longrightarrow\, \mbox{było-}\mathbf{exit}}
\frac{I', s \,\Longrightarrow\, \mbox{by³o-}\mathbf{exit}}
     {I' \,\mathbf{then}\, \mathbf{loop}\, I, s \,\Longrightarrow\, s}
     {I' \,\mathbf{then}\, \mathbf{loop}\, I, s \,\Longrightarrow\, s}
\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}
     {I; \,\mathbf{then}\, \mathbf{loop}\, I, s \,\Longrightarrow\, \mathbf{loop}\, I, s}
\quad \quad
\quad \quad
Linia 581: Linia 580:


a zbiór konfiguracji poszerzamy tylko o dwie nowe konfiguracje
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>
</div></div>
Linia 590: Linia 589:




==== Zadanie 1 ====
{{cwiczenie|1|cw1.dom|


Zaproponuj semantykę mało-krokową dla rozszerzeń języka Tiny, które
Zaproponuj semantykê ma³o-krokow± dla rozszerzeñ jêzyka Tiny, które
studiowaliśmy powyżej.
studiowali¶my powy¿ej.
}}




==== Zadanie 2 ====
{{cwiczenie|2|cw2.dom|


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>
Linia 607: Linia 607:
</math>
</math>


Identyfikator <math>x</math> pełni tutaj rolę etykiety przypisanej
Identyfikator <math>x</math> pe³ni tutaj rolê etykiety zwi±zanej z
instrukcji <math>\mathbf{loop}\,</math>, jest też parametrem dwóch pozostałych
instrukcj± <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±
otaczającą pętlę o etykiecie <math>x</math>.  
otaczaj±c± pêtlê o etykiecie <math>x</math>.  


===== Przykład =====
{{przyklad|||


Program


  x: <math>\mathbf{loop}\,</math>
  x: <math>\mathbf{loop}\,</math>
Linia 624: Linia 625:
  a := a+2;
  a := a+2;


}}


Program kończy działanie z wartością zmiennej <math>a = 3</math>.
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
Za pomoc± wciêæ okre¶lili¶my, do wnêtrza której pêtli
<math>\mathbf{loop}\,</math> należy każda z trzech ostatnich instrukcji przypisania.  
<math>\mathbf{loop}\,</math> nale¿y ka¿da z trzech ostatnich instrukcji przypisania.  
Niejednoznaczność bierze się oczywiście stąd, że
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>.
}}




==== Zadanie 3 ====
{{cwiczenie|3|cw3.dom|


Napisz semantykę naturalną i mało-krokową dla rozszerzenia
Napisz semantykê naturaln± i ma³o-krokow± dla rozszerzenia
języka Tiny o wyrażenia z efektami ubocznymi:
jêzyka Tiny o wyra¿enia z efektami ubocznymi:


<math>
<math>
Linia 647: Linia 650:
</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 07:59, 9 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± wyra¿eñ boolowskich i arytmetycznych oraz semantykê 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:

e::=…|e1/e2

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

Rozszerzmy jêzyk Tiny o nastêpuj±c± instrukcjê pêtli:

I::=𝐥𝐨𝐨𝐩I|𝐞𝐱𝐢𝐭|𝐜𝐨𝐧𝐭𝐢𝐧𝐮𝐞

𝐥𝐨𝐨𝐩I to instrukcja pêtli, I stanowi instrukcjê wewnêtrzn±. Instrukcja 𝐞𝐱𝐢𝐭 wychodzi z nabli¿szej otaczaj±cej pêtli 𝐥𝐨𝐨𝐩 i kontynuuje wykonanie programu od pierwszej instrukcji za t± pêtl±. Instrukcja 𝐜𝐨𝐧𝐭𝐢𝐧𝐮𝐞 powraca na pocz±tek instrukcji wewnêtrznej najbli¿szej otaczaj±cej pêtli 𝐥𝐨𝐨𝐩.

Pozwa¿ zarówno semantykê naturaln± jak i semantykê ma³ych kroków.


Rozwiązanie (semantyka naturalna)

{{{3}}}


Rozwiązanie (ma³e kroki)

{{{3}}}


Zadania domowe

Ćwiczenie 1

Zaproponuj semantykê ma³o-krokow± dla rozszerzeñ jêzyka Tiny, które studiowali¶my powy¿ej.


Ćwiczenie 2

Napisz semantyjê naturaln± dla nieznacznie rozszerzonej wersji instrukcji 𝐥𝐨𝐨𝐩:

I::=x:𝐥𝐨𝐨𝐩I|𝐞𝐱𝐢𝐭x|𝐜𝐨𝐧𝐭𝐢𝐧𝐮𝐞x

Identyfikator x pe³ni tutaj rolê etykiety zwi±zanej z instrukcj± 𝐥𝐨𝐨𝐩, jest te¿ parametrem dwóch pozosta³ych instrukcji. 𝐞𝐱𝐢𝐭x koñczy teraz najbli¿sz± otaczaj±c± pêtlê 𝐥𝐨𝐨𝐩 o etykiecie x. Podobnie 𝐜𝐨𝐧𝐭𝐢𝐧𝐮𝐞x wznawia najbli¿sz± otaczaj±c± pêtlê o etykiecie x.

Przykład

{{{3}}}

koñczy dzia³anie z warto¶ci± zmiennej a=3. 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. 𝐥𝐨𝐨𝐩I𝐞𝐧𝐝𝐥𝐨𝐨𝐩.


Ćwiczenie 3

Napisz semantykê naturaln± i ma³o-krokow± dla rozszerzenia jêzyka Tiny o wyra¿enia z efektami ubocznymi:

e::=…|𝐝𝐨I𝐭𝐡𝐞𝐧e|x:=e|x++|…

Obliczenie wyra¿enia 𝐝𝐨I𝐭𝐡𝐞𝐧e polega na wykonaniu I a potem na obliczeniu e. Warto¶æ wyra¿enia x:=e jest taka jak warto¶æ wyra¿enia e a efektem ubocznym jest podstawienie tej warto¶ci na zmienn± x.

Źródło: „https://wazniak.mimuw.edu.pl/index.php?title=Semantyka_i_weryfikacja_programów/Ćwiczenia_3&oldid=11339”