Semantyka i weryfikacja programów/Ćwiczenia 3

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 $\mathbf {loop} \,$, pozwalającą na niestrukturalne przerwanie lub wznowienie iteracji (instrukcje $\mathbf {exit}$ i $\mathbf {continue}$).

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

Przypomnijmy składnię wyrażeń boolowskich i arytmetycznych języka TINY:

$b\,::=\,\,l\,\,|\,\,e_{1}\leq e_{2}\,\,|\,\,\neg b\,\,|\,\,b_{1}\land b_{2}\,\,|\,\,\ldots$

$l\,::=\,\,\mathbf {true} \,\,|\,\,\mathbf {false}$

$e\,::=\,\,n\,\,|\,\,x\,\,|\,\,e_{1}+e_{2}\,\,|\,\,\ldots$

$n\,::=\,\,0\,\,|\,\,1\,\,|\,\,\ldots$

$x\,::=\,\,\ldots \,(identyfikatory)\,\ldots$

Chcemy, aby tranzycje wyrażeń wyglądały następująco:

$e,s\longrightarrow n\quad \quad \quad b,s\longrightarrow l,$

gdzie $s\in \mathbf {State}$, $n\in$ jest liczbą całkowitą, $n\in \mathbf {Num}$, a $l\in \mathbf {Bool} =\{\mathbf {true} ,\mathbf {false} \}$. Tranzycja taka oznacza, że wyrażenie $e$ w stanie $s$ wylicza się do wartości $n$ oraz analogicznie, wyrażenie logiczne $b$ w stanie $s$ wylicza się do $l$. Zatem zbiór konfiguracji dla semantyki całego języka Tiny to znów

$((\mathbf {Exp} \,\cup \,\mathbf {BExp} \,\cup \,\mathbf {Stmt} )\times \mathbf {State} )\,\bigcup \,\mathbf {Num} \,\cup \,\mathbf {Bool} \,\cup \,\mathbf {State}$ a konfiguracje końcowe to $\mathbf {State}$ tak jak poprzednio. Tranzycje dla instrukcji pozostają zasadniczo bez zmian, z tym że odwołania do funkcji semantycznych dla wyrażen zastępujemy przez odpowiednie tranzycje. Np. dla instrukcji pętli będziemy mieć następujące reguły:

${\frac {b,s\,\longrightarrow \,\mathbf {true} \quad \quad I;\mathbf {while} \,b\,\mathbf {do} \,I,s\,\longrightarrow \,s'}{\mathbf {while} \,b\,\mathbf {do} \,I,s\,\longrightarrow \,s'}}$

${\frac {b,s\,\longrightarrow \,\mathbf {false} }{\mathbf {while} \,b\,\mathbf {do} \,I,s\,\longrightarrow \,s}}$

Podobnie dla instrukcji warunkowej. Teraz zajmiemy się tranzycjami dla wyrażeń. Zacznijmy od stałych arytmetycznych i boolowskich:

$n,s\,\longrightarrow \,n\quad \quad l,s\,\longrightarrow \,l.$

Operatory arytmetyczne definiujemy następująco:

${\frac {e_{1},s\,\longrightarrow \,n_{1}\quad \quad e_{2},s\,\longrightarrow \,n_{2}\quad \quad n=n_{1}+n_{2}}{e_{1}+e_{2},s\,\longrightarrow \,n}}$

Czyli aby obliczyć sumę $e_{1}+e_{2}$ w stanie $s$, trzeba najpierw obliczyć $e_{1}$ i $e_{2}$ w tym stanie, a następnie dodać obliczone wartości. Zauważmy, że nie specyfikujemy kolejności, w jakiej mają się obliczać obydwa podwyrażenia. I choć tutaj nie ma to żadnego znaczenia, w przyszłości będzie inaczej, gdy jezyk będzie umożliwiał efekty uboczne podczas obliczania wyrażeń.

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

${\frac {b_{1},s\,\longrightarrow \,l_{1}\quad \quad b_{2},s\,\longrightarrow \,l_{2}\quad \quad l=l_{1}\land l_{2}}{b_{1}\land b_{2},s\,\longrightarrow \,l}}$

(strategia gorliwa). Reguły dla $\leq$ są następujące:

${\frac {e_{1},s\,\longrightarrow \,n_{1}\quad \quad e_{2},s\,\longrightarrow \,n_{2}\quad \quad n_{1}\leq n_{2}}{e_{1}\leq e_{2},s\,\longrightarrow \,\mathbf {true} }}\quad \quad {\frac {e_{1},s\,\longrightarrow \,n_{1}\quad \quad e_{2},s\,\longrightarrow \,n_{2}\quad \quad n_{1}>n_{2}}{e_{1}\leq e_{2},s\,\longrightarrow \,\mathbf {false} }}$

Oto inny wariant semantyki spójnika $\land$, tzw. strategia lewostronna (ponieważ rozpoczynamy od lewego koniunktu):

${\frac {b_{1},s\,\longrightarrow \,\mathbf {false} }{b_{1}\land b_{2},s\,\longrightarrow \,\mathbf {false} }}\quad \quad {\frac {b_{1},s\,\longrightarrow \,\mathbf {true} \quad \quad b_{2},s\,\longrightarrow \,l}{b_{1}\land b_{2},s\,\longrightarrow \,l}}$

Inny wariant to strategia prawostronna (najpierw $b_{2}$, potem $b_{1}$). Wreszcie rozważmy kombinację obydwu semantyk (strategia równoległa lub leniwa):

${\frac {b_{1},s\,\longrightarrow \,\mathbf {false} }{b_{1}\land b_{2},s\,\longrightarrow \,\mathbf {false} }}\quad \quad \quad {\frac {b_{2},s\,\longrightarrow \,\mathbf {false} }{b_{1}\land b_{2},s\,\longrightarrow \,\mathbf {false} }}$

Czyli jeśli którekolwiek z podwyrażeń daje wynik $\mathbf {false}$, to taki wynik zyskuje całe wyrażenie. Dodatkowo potrzebujemy jeszcze reguły:

${\frac {b_{1},s\,\longrightarrow \,\mathbf {true} \quad \quad b_{2},s\,\longrightarrow \,\mathbf {true} }{b_{1}\land b_{2},s\,\longrightarrow \,\mathbf {true} }}$

Pytanie: czy w naszym prostym języku wszystkie cztery strategie obliczania spójnika $\land$ są równoważne?

Reguły dla negacji oraz dla instrukcji przypisania pozostawiamy jako proste ćwiczenie.

Ćwiczenie 2

Rozważ dodatkowo operację dzielenia:

$e\,::=\,\,\ldots \,\,|\,\,e_{1}/e_{2}$

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

Dopóki nie wystąpi błąd dzielenia przez zero, semantyka programu powinna być identyczna jak w poprzednim zadaniu. Zatem pozostawiamy wszystkie reguły z poprzedniego zadania. Dodatkowo potrzebujemy reguł, które opiszą

• kiedy powstaje błąd oraz
• jak zachowuje się program po wystąpieniu błędu

Zaczynamy od pierwszego punktu. W tym celu dodajemy do konfiguracji jedną konfigurację końcową ${\mathtt {Blad}}$. Reguła opisująca powstanie błędu może wyglądać np. tak (duże i małe kroki):

${\frac {e_{2},s\,\longrightarrow \,0}{e_{1}/e_{2},s\,\longrightarrow \,{\mathtt {Blad}}}}\quad \quad e_{1}/0,s\,\Longrightarrow ,{\mathtt {Blad}}.$

Pomijamy tutaj reguły dla przypadku, gdy $e_{2}$ oblicza się do wartości różnej od zera. Ponadto dla czytelności przyjęliśmy, że wynikiem tranzycji jest 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 poniżej) zmodyfikować tak, by wraz z 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:

${\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$

i zamiast pojedyńczej konfiguracji końcowej ${\mathtt {Blad}}$ potrzebowalibyśmy oczywiście całego zbioru $\{{\mathtt {Blad}}\}\times \mathbf {State}$.

Przejdźmy teraz do drugiego punktu. Potrzebujemy dodatkowych reguł, które zagwarantują, że błąd, raz pojawiwszy się, propaguje się przez wszystkie konstrukcje składniowe, a normalne obliczenie wyrażenia jest wstrzymame.

${\frac {e_{1},s\,\longrightarrow \,{\mathtt {Blad}}}{e_{1}\leq e_{2},s\,\longrightarrow \,{\mathtt {Blad}}}}\quad \quad \quad {\frac {e_{2},s\,\longrightarrow \,{\mathtt {Blad}}}{e_{1}\leq e_{2},s\,\longrightarrow \,{\mathtt {Blad}}}}$

Następnie, błąd w wyrażeniu powinien wstrzymać normalne wykonanie instrukcji:

${\frac {b\,\longrightarrow \,{\mathtt {Blad}}}{\mathbf {if} \,b\,\mathbf {then} \,I_{1}\,\mathbf {else} \,I_{2},s\,\longrightarrow \,{\mathtt {Blad}}}}$

${\frac {b\,\longrightarrow \,{\mathtt {Blad}}}{\mathbf {while} \,b\,\mathbf {do} \,I,s\,\longrightarrow \,{\mathtt {Blad}}}}$

${\frac {e,s\,\longrightarrow \,{\mathtt {Blad}}}{x:=e,s\,\longrightarrow \,{\mathtt {Blad}}}}$

I wreszcie błąd powinien propagować się do kolejnych instrukcji:

${\frac {I_{1},s\,\longrightarrow \,{\mathtt {Blad}}}{I_{1};\,I_{2},s\,\longrightarrow \,{\mathtt {Blad}}}}$

${\frac {b,s\,\longrightarrow \,\mathbf {true} \quad \quad I_{1},s\,\longrightarrow \,{\mathtt {Blad}}}{\mathbf {if} \,b\,\mathbf {then} \,I_{1}\,\mathbf {else} \,I_{2},s\,\longrightarrow \,{\mathtt {Blad}}}}\quad \quad \quad {\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}}}}$

${\frac {b,s\,\longrightarrow \,\mathbf {true} \quad \quad I,s\,\longrightarrow \,{\mathtt {Blad}}}{\mathbf {while} \,b\,\mathbf {do} \,I,s\,\longrightarrow \,{\mathtt {Blad}}}}\quad \quad {\frac {b,s\,\longrightarrow \,\mathbf {true} \quad \quad I,s\,\longrightarrow \,s'\quad \quad \mathbf {while} \,b\,\mathbf {do} \,I,s'\,\longrightarrow \,{\mathtt {Blad}}}{\mathbf {while} \,b\,\mathbf {do} \,I,s\,\longrightarrow \,{\mathtt {Blad}}}}$

Zwróćmy szczególnie uwagę na ostatnią regułę dla pętli $\mathbf {while} \,$: 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.

Ćwiczenie 3

Rozszerzmy język TINY o następującą instrukcję pętli:

$I\,::=\,\,\mathbf {loop} \,I\,\,|\,\,\mathbf {exit} \,\,|\,\,\mathbf {continue}$

$\mathbf {loop} \,I$ to instrukcja pętli, $I$ stanowi instrukcję wewnętrzną. Instrukcja $\mathbf {exit}$ wychodzi z nabliższej otaczającej pętli $\mathbf {loop} \,$ i kontynuuje wykonanie programu od pierwszej instrukcji za tą pętlą. Instrukcja $\mathbf {continue}$ powraca na początek instrukcji wewnętrznej najbliższej otaczającej pętli $\mathbf {loop} \,$.

Pozważ zarówno semantykę naturalną, jak i semantykę małych kroków.

Rozwiązanie

Dodamy do reguł semantyki naturalnej dla języka TINY kilka nowych reguł opisujących nową konstrukcję języka i jej "interakcję" z pozostałymi konstrukcjami.

Pomysł polega na dodaniu specjalnych konfiguracji zawierających informację o tym, że została wykonana instrukcja $\mathbf {exit}$ lub $\mathbf {continue}$. Oto odpowiednie reguły:

$\mathbf {exit} ,s\,\longrightarrow \,s,{\mbox{było-}}\mathbf {exit} \quad \quad \mathbf {continue} ,s\,\longrightarrow \,s,{\mbox{było-}}\mathbf {continue} .$

Czyli instrukcje $\mathbf {exit}$ i $\mathbf {continue}$ nie modyfikują stanu $s$, ale zostawiają po sobie "ślad". Zauważmy, że taki ślad zostaje pozostawiony tylko wtedy, jeśli nie było dotychczas innego śladu, to znaczy jeśli $\mathbf {exit}$ (lub $\mathbf {continue}$) zostało wykonane w zwykłym stanie $s$. Oczywiście poszerzamy odpowiednio zbiór konfiguracji o:

$\mathbf {State} \times \{{\mbox{było-}}\mathbf {exit} ,{\mbox{było-}}\mathbf {continue} \}.$

Pytanie: jakie powinno być zachowanie $\mathbf {exit}$ i $\mathbf {continue}$ w konfiguracji $s,{\mbox{było-}}\mathbf {exit}$ lub $s,{\mbox{było-}}\mathbf {continue}$? Czy instrukcje $\mathbf {exit}$ i $\mathbf {continue}$ będą faktycznie wykonywane w takich konfiguracjach?

Zapiszmy teraz, jak inne instrukcje korzystają z dodatkowej informacji (śladu) zawartej w konfiguracjach. Oczywiście "beneficjentem" korzystającym z tej informacji jest instrukcja $\mathbf {loop} \,$:

${\frac {I,s\,\longrightarrow \,s',{\mbox{było-}}\mathbf {exit} }{\mathbf {loop} \,I,s\,\longrightarrow \,s'}}\quad \quad {\frac {I,s\,\longrightarrow \,s',{\mbox{było-}}\mathbf {continue} \quad \quad \mathbf {loop} \,I,s'\,\longrightarrow \,s''}{\mathbf {loop} \,I,s\,\longrightarrow \,s''}}$

Czyli w zależności od tego, jaki ślad został zarejestrowany podczas wykonania $I$, albo kończymy wykonanie pętli $\mathbf {loop} \,$, albo rozpoczynamy kolejną iterację. Zauważmy, że stan $s'$ może być różny od $s$, ponieważ zanim wykonała się ktoraś z instrukcji $\mathbf {exit}$ lub $\mathbf {continue}$ mogły zostać zmienione wartości niektórych zmiennych.

Oczywiście, jeśli instrukcja wewnętrzna $I$ zakończyła się "normalnie", kontynuujemy wykonanie pętli podobnie jak w przypadku wywołania $\mathbf {continue}$:

${\frac {I,s\,\longrightarrow \,s'\quad \quad \mathbf {loop} \,I,s'\,\longrightarrow \,s''}{\mathbf {loop} \,I,s\,\longrightarrow \,s''}}$

Pytanie: czy potrzebujemy dodatkowo reguł postaci:

${\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} }}\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} }{\mathbf {loop} \,I,s\,\longrightarrow \,s'',{\mbox{było-}}\mathbf {exit} }}$

Okazuje się że nie, ponieważ ślad powinien zostać zawsze "wymazany" przez pętlę $\mathbf {loop} \,$.

Teraz musimy określić zachowanie wszystkich instrukcji w sytuacji, gdy bieżąca konfiguracja zawiera już ślad. Zasadniczo, powinniśmy zaniechać wykonania instrukcji (w przypadku pętli, powinniśmy zaniechać dalszego iterowania tej pętli). Oto odpowiednie reguły dla ${\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} }}\quad \quad {\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} }}$

${\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} }}\quad \quad {\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} }}$

${\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} }}\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} }}$

Pominęliśmy zupełnie analogiczne reguły dla ${\mbox{było-}}\mathbf {continue}$. Zauważmy, że dla pętli $\mathbf {while} \,$ nie rozpatrujemy przypadku, gdy dozór $b$ oblicza się do $\mathbf {false}$, gdyż w tym przypadku nie ma możliwości wygenerowania śladu.

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

Rozwiązanie

W semantyce naturalnej musieliśmy napisać wiele reguł, aby zapewnić pomijanie instrukcji w sytuacji, gdy został juz zarejestrowany jakiś ślad. Było to dość uciążliwe. Okazuje się, że podejście mało-krokowe oferuje możliwość bardziej eleganckiego rozwiązania.

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

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

$\mathbf {exit} ,s\,\Longrightarrow ,s,{\mbox{było-}}\mathbf {exit} \quad \quad \mathbf {continue} ,s\,\Longrightarrow ,s,{\mbox{było-}}\mathbf {continue} .$

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

${\frac {I_{1},s\,\Longrightarrow ,s',{\mbox{było-}}\mathbf {exit} }{I_{1};\,I_{2},s\,\Longrightarrow ,s',{\mbox{było-}}\mathbf {exit} }}\quad \quad {\mbox{ i analogicznie dla }}{\mbox{było-}}\mathbf {continue} .$

Nie musimy zajmowac się przypadkiem, gdy ślad powstaje w $I_{2}$, bo wybraliśmy podejście małokrokowe. Ponadto, nie musimy opisywać instrukcji warunkowej i pętli $\mathbf {while} \,$, ponieważ ślad nie może powstać podczas obliczania dozoru!

Wreszcie zobaczmy jak zachowuje się pętla $\mathbf {loop} \,$:

${\frac {I,s\,\Longrightarrow ,s',{\mbox{było-}}\mathbf {exit} }{\mathbf {loop} \,I,s\,\Longrightarrow ,s'}}\quad \quad {\frac {I,s\,\Longrightarrow ,s',{\mbox{było-}}\mathbf {continue} }{\mathbf {loop} \,I,s\,\Longrightarrow ,\mathbf {loop} \,I,s'}}$

Reguły te są prawie identyczne z regułami semantyki naturalnej dla tej sytuacji! Natomiast korzystamy z tego, że w podejściu małokrokowym zmiana konfiguracji na $s',{\mbox{było-}}\mathbf {exit}$ czy $s',{\mbox{było-}}\mathbf {continue}$ jest natychmiast widoczna w instrukcji $\mathbf {loop} \,I$, nawet jeśli $\mathbf {exit}$ czy $\mathbf {continue}$ zostało wywołane głęboko wewnątrz $I$!

Niestety powyższe reguły nie są poprawne! Dlaczego? Jak zwykle w semantyce małych kroków, wykonując instrukcję wewnętrzną "zapominamy" stopniowo, jaka była ona na początku. W związku z tym nie potrafimy poprawnie powrócić do wykonywania pętli $\mathbf {loop} \,$ po wywołaniu $\mathbf {continue}$.

Prostym sposobem poprawienia naszego błędu jest rozszerzenie składni tak, aby możliwe było jednorazowe rozwinięcie pętli $\mathbf {loop} \,$:

$\mathbf {loop} \,I,s\,\Longrightarrow ,I\,\mathbf {then} \,\mathbf {loop} \,I,s.$

Teraz możemy zapisać dwie powyższe reguły dla $\mathbf {loop} \,$ w poprawnej wersji, pamiętając o tym, że ${\mbox{było-}}\mathbf {exit}$ i ${\mbox{było-}}\mathbf {continue}$ pojawią się nie w instrukcji wewnętrznej, ale w jej kopii umieszczonej przed $\,\mathbf {then} \,$:

${\frac {I',s\,\Longrightarrow ,s',{\mbox{było-}}\mathbf {exit} }{I'\,\mathbf {then} \,\mathbf {loop} \,I,s\,\Longrightarrow ,s'}}\quad \quad {\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'}}$

Potrzebujemy też dodatkowej reguły dla obliczeń wewnątrz instrukcji stojącej przed $\,\mathbf {then} \,$ (w szczególności może ona zawierać zagnieżdzone pętle $\mathbf {loop} \,$):

${\frac {I',s\,\Longrightarrow ,I'',s'}{I'\,\mathbf {then} \,\mathbf {loop} \,I,s\,\Longrightarrow ,I''\,\mathbf {then} \,\mathbf {loop} \,I,s'}}$

Na koniec zauważmy, że stan $s'$ w pierwszych dwóch z powyższych reguł nigdy nie jest różny od $s$. Zatem równoważnie moglibyśmy zamienić $s'$ na $s$ w powyższych dwóch regułach. Ale wtedy okazuje się, $s$ w parze z ${\mbox{było-}}\mathbf {exit}$ albo ${\mbox{było-}}\mathbf {continue}$ jest nadmiarowe i może zostać wyeliminowane. Zatem ostatecznie nasze reguły mogą wyglądać tak:

$\mathbf {exit} ,s\,\Longrightarrow ,{\mbox{było-}}\mathbf {exit} \quad \quad \mathbf {continue} ,s\,\Longrightarrow ,{\mbox{było-}}\mathbf {continue}$

${\frac {I_{1},s\,\Longrightarrow ,{\mbox{było-}}\mathbf {exit} }{I_{1};\,I_{2},s\,\Longrightarrow ,{\mbox{było-}}\mathbf {exit} }}\quad \quad {\frac {I_{1},s\,\Longrightarrow ,{\mbox{było-}}\mathbf {continue} }{I_{1};\,I_{2},s\,\Longrightarrow ,{\mbox{było-}}\mathbf {continue} }}$

$\mathbf {loop} \,I,s\,\Longrightarrow ,I\,\mathbf {then} \,\mathbf {loop} \,I,s.$

${\frac {I',s\,\Longrightarrow ,{\mbox{było-}}\mathbf {exit} }{I'\,\mathbf {then} \,\mathbf {loop} \,I,s\,\Longrightarrow ,s}}\quad \quad {\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}}$

${\frac {I',s\,\Longrightarrow ,I'',s'}{I'\,\mathbf {then} \,\mathbf {loop} \,I,s\,\Longrightarrow ,I''\,\mathbf {then} \,\mathbf {loop} \,I,s'}}$

a zbiór konfiguracji poszerzamy tylko o dwie nowe konfiguracje $\{{\mbox{było-}}\mathbf {exit} ,{\mbox{było-}}\mathbf {continue} \}$.

Zadania domowe

Ćwiczenie 1

Zaproponuj semantykę małokrokową dla rozszerzeń języka Tiny, które studiowaliśmy powyżej.

Ćwiczenie 2

Napisz semantykę naturalną dla nieznacznie rozszerzonej wersji instrukcji $\mathbf {loop} \,$:

$I\,::=\,\,x:\mathbf {loop} \,I\,\,|\,\,\mathbf {exit} \,x\,\,|\,\,\mathbf {continue} \,x$

Identyfikator $x$ pełni tutaj rolę etykiety związanej z instrukcją $\mathbf {loop} \,$, jest też parametrem dwóch pozostałych instrukcji. $\mathbf {exit} x$ kończy teraz najbliższą otaczającą pętlę $\mathbf {loop} \,$ o etykiecie $x$. Podobnie $\mathbf {continue} x$ wznawia najbliższą otaczającą pętlę o etykiecie $x$.

Przykład

Program

x: $\mathbf {loop} \,$
  a := 1; 
  y: $\mathbf {loop} \,$
    $\mathbf {exit}$ x;
    a := a-10;
  a := a+1;
a := a+2;

kończy działanie z wartością zmiennej $a=3$. Za pomocą wcięć określiliśmy, do wnętrza której pętli $\mathbf {loop} \,$ 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ę $\mathbf {loop} \,$, np. $\mathbf {loop} \,I\,\mathbf {end} \mathbf {loop} \,$.

Ćwiczenie 3

Napisz semantykę naturalną i małokrokową dla rozszerzenia języka TINY o wyrażenia z efektami ubocznymi:

$e\,::=\,\,\ldots \,\,|\,\,\,\mathbf {do} \,I\,\mathbf {then} \,e\,\,|\,\,x:=e\,\,|\,\,x++\,\,|\,\,\ldots$

Obliczenie wyrażenia $\,\mathbf {do} \,I\,\mathbf {then} \,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$.