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±
Uzupełnimy semantykę naturalną języka Tiny o semantykę naturalną
wyra¿eñ boolowskich i arytmetycznych oraz semantykê b³êdów wykonania.
wyrażeń boolowskich i arytmetycznych oraz semantykę 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 24: 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 56: 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 64: 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 75: 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 92: 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 101: Linia 101:
</math>
</math>


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


<math>
<math>
Linia 110: 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 129: 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 142: 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 152: 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 162: 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 174: Linia 174:
{{cwiczenie|2|cw2|
{{cwiczenie|2|cw2|


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


<math>
<math>
Linia 181: 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 193: 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 214: 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 230: 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 246: 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 263: 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 287: 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 300: Linia 300:
{{cwiczenie|3|cw3|
{{cwiczenie|3|cw3|


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


<math>
<math>
Linia 309: 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 otaczaj±cej 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ą.
Instrukcja <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 otaczaj±cej pêtli <math>\mathbf{loop}\,</math>.
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.
}}
}}


Linia 323: Linia 323:
<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 382: 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 443: Linia 443:




{{rozwiazanie|(ma³e kroki)|roz3.2|
{{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 511: 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 527: 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 536: 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 564: 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 580: 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 591: Linia 591:
{{cwiczenie|1|cw1.dom|
{{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.
}}
}}


Linia 598: Linia 598:
{{cwiczenie|2|cw2.dom|
{{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 zwi±zanej z
Identyfikator <math>x</math> pełni tutaj rolę etykiety związanej z
instrukcj± <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>.  


{{przyklad|||
{{przyklad|||
Linia 627: Linia 627:
}}
}}


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>.
}}
}}
Linia 639: Linia 639:
{{cwiczenie|3|cw3.dom|
{{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 650: 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 08:06, 10 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=12804”