Semantyka i weryfikacja programów/Ćwiczenia 3

From Studia Informatyczne

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 (semantyka naturalna)

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 (małe kroki)

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.