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ść ==
Kończymy semantykę małych kroków i rozpoczynamy semantykę naturalną (duże kroki).
Uzupełnimy semantykę naturalną języka Tiny o semantykę naturalną dla
wyrażeń boolowskich i arytmetycznych i semantykę dla
błędów wykonania.
Wreszcie dodamy instrukcję pętli <math> \mathbf{loop}\, </math> i instrukcje
niestrukturalnego zakończenia pętli (instrukcje <math> \mathbf{exit}</math> i <math> \mathbf{continue} </math>).
== Rozszerzenia semantyki języka Tiny ==
==== Zadanie 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
jezyka Tiny:
<math>
b \, ::= \,\,
        l \,\,|\,\,
        e_1 \leq e_2  \,\,|\,\,
        \neg b  \,\,|\,\,
        b_1  \land  b_2  \,\,|\,\, \ldots 
</math>
<math>
l \, ::= \,\,
        \mathbf{true}    \,\,|\,\,
        \mathbf{true}       
</math>
<math>
e \,  ::= \,\, 
        n  \,\,|\,\,
        x  \,\,|\,\,
        e_1 + e_2  \,\,|\,\, \ldots
</math>
<math>
n \, ::= \,\, 0 \,\,|\,\, 1 \,\,|\,\, \ldots
</math>
<math>
x \, ::= \,\, \ldots \, (identyfikatory) \, \ldots
</math>
Chcemy, aby tranzycje wyrażen wyglądały następująco:
<math>
e, s \longrightarrow n 
\quad \quad \quad
b, s \longrightarrow l,
</math>
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{true} \} </math>.
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
stanie <math> s </math> wylicza się do <math> l </math>.
Zatem zbiór konfiguracji dla semantyki całego języka Tiny to znów
<math>
( (\mathbf{Exp} \, \cup \, \mathbf{BExp} \, \cup \, \mathbf{Stmt}) \times \mathbf{State} ) \, \bigcup \,
\mathbf{Num} \, \cup \, \mathbf{Bool} \, \cup \, \mathbf{State}
</math>
a konfiguracje końcowe to <math> \mathbf{State} </math> 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:
<math>
\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'}
</math>
<math>
\frac{b, s \,\longrightarrow\, \mathbf{true}}
    {\mathbf{while}\, b \,\mathbf{do}\, I, s \,\longrightarrow\, s}
</math>
Podobnie dla instrukcji warunkowej.
Teraz zajmiemy się tranzycjami dla wyrażeń.
Zacznijmy od stalych arytmetycznych i boolowskich:
<math>
n, s \,\longrightarrow\, n
\quad \quad
l, s \,\longrightarrow\, l.
</math>
Operatory arytmetyczne definiujemy następująco:
<math>
\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}
</math>
Czyli aby obliczyć sumę <math> e_1 + e_2 </math> w stanie
<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.
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
arytmnetycznych, oraz dla spójników logicznych:
<math>
\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}
</math>
Oto inny wariant, reguły lewo-stronne (ponieważ rozpoczynamy od ''lewego'' koniunktu):
<math>
\frac{b_1, s \,\longrightarrow\, \mathbf{true}}
    {b_1 \land b_2, s \,\longrightarrow\, \mathbf{true}}
\frac{b_1, s \,\longrightarrow\, \mathbf{true}  \quad \quad 
      b_2, s \,\longrightarrow\, l}
    {b_1 \land b_2, s \,\longrightarrow\, l}
</math>
Inny wariant to wariant prawo-stronny (
najpierw <math> b_2 </math>, potem <math> b_1 </math>).
Wreszcie rozważmy kombinację obydwu semantyk (reguły ''równoległe''):
<math>
\frac{b_1, s \,\longrightarrow\, \mathbf{true}}
    {b_1 \land b_2, s \,\longrightarrow\, \mathbf{true}}
\quad \quad \quad
\frac{b_2, s \,\longrightarrow\, \mathbf{true}}
      {b_1 \land b_2, s \,\longrightarrow\, \mathbf{true}}
</math>
Czyli jeśli którekolwiek z podwyrażeń daje wynik <math> \mathbf{true} </math>,
to taki wynik zyskuje całe wyrażenie.
Dodatkowo potrzebujemy jeszcze reguły:
<math>
\frac{b_1, s \,\longrightarrow\, \mathbf{true}  \quad \quad
      b_2, s \,\longrightarrow\, \mathbf{true}}
    {b_1 \land b_2,s \,\longrightarrow\, \mathbf{true}}
</math>
W naszym prostym języku wszystkie cztery warianty
są równoważne.
Reguły dla pozostałych spójników logicznych, dla
negacji oraz dla instrukcji przypisania pozostawiamy jako proste ćwiczenie.
==== Zadanie 2 ====
Rozważ dodatkowo operację dzielenia:
<math>
e \, ::= \,\,  \ldots  \,\,|\,\,
        e_1 / e_2
</math>
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 (szkic) ====
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ą
<math> \mathtt{Blad} </math>.
Reguła opisująca powstanie błędu może wyglądać np. tak:
<math>
\frac{e_2, s \longrightarrow 0}
{e_1 / e_2, s \longrightarrow Blad}
</math>
Pomijamy tutaj reguły dla przypadku, gdy <math>e_2</math>
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:
<math>
e_1 / 0, s \Longrightarrow Blad, s
</math>
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>.
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.
<math>
\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}}
</math>
Następnie, błąd w wyrażeniu powinien wstrzymać normalne wykonanie instrukcji:
<math>
\frac{b \,\longrightarrow\, \mathtt{Blad}}
{\mathbf{if}\, b \,\mathbf{then}\, I_1 \,\mathbf{else}\, I_2, s \,\longrightarrow\, \mathtt{Blad}}
</math>
<math>
\frac{b \,\longrightarrow\, \mathtt{Blad}}
{\mathbf{while}\, b \,\mathbf{do}\, I, s \,\longrightarrow\, \mathtt{Blad}}
</math>
<math>
\frac{e, s \,\longrightarrow\, \mathtt{Blad}}
    {x := e, s \,\longrightarrow\, \mathtt{Blad}}
</math>
I wreszcie błąd powinien propagować się do kolejnych instrukcji:
<math>
\frac{I_1, s \,\longrightarrow\, \mathtt{Blad}}
    {I_1;\, I_2, s \,\longrightarrow\, \mathtt{Blad}}
</math>
<math>
\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{true} \quad \quad I_2, s \,\longrightarrow\, \mathtt{Blad}}
    {\mathbf{if}\, b \,\mathbf{then}\, I_1 \,\mathbf{else}\, I_2, s \,\longrightarrow\, \mathtt{Blad}}
</math>
<math>
\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}}
</math>
==== Zadanie 3 ====
Rozszerz język Tiny o następującą instrukcję pętli:
<math>
I \, ::= \,\,
      \mathbf{loop}\, I \,\,|\,\,
      \mathbf{exit} \,\,|\,\,
      \mathbf{continue}
</math>
<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>
i kontynuuje wykonanie programu od pierwszej instrukcji za tą pętlą.
Instrukcje <math> \mathbf{continue} </math> powraca na początek instrukcji wewnętrznej
najbliższej pętli.
Pozważ zarówno semantykę naturalną jak i semantykę małych kroków.
==== Rozwiązanie 1 (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 <math> \mathbf{exit} </math>
lub <math> \mathbf{continue} </math>. Oto odpowiednie reguły:
<math>
\mathbf{exit}, s \,\longrightarrow\, s, \mbox{było-}\mathbf{exit}
\quad \quad
\mathbf{continue}, s \,\longrightarrow\, s, \mbox{było-}\mathbf{continue}.
</math>
Czyli instrukcje <math> \mathbf{exit} </math> i <math> \mathbf{continue} </math> nie modyfikują
stanu <math> s </math>, ale zostawiają po sobie \''ślad".
Zauważmy, że taki ślad zostaje pozostawiony tylko wtedy, jesli
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>.
Oczywiście poszerzamy odpowiednio zbiór konfiguracji o:
</math>[
\mathbf{State} \times \{ \mbox{było-}\mathbf{exit}, \mbox{było-}\mathbf{continue} \}
</math>
,
'''Pytanie''': jakie powinno być zachowanie <math> \mathbf{exit} </math> i
<math> \mathbf{continue} </math> w konfiguracji <math> s, \mbox{było-}\mathbf{exit} </math>
lub <math> s, \mbox{było-}\mathbf{continue} </math>?
Czy instrukcje <math> \mathbf{exit} </math> i <math> \mathbf{continue} </math>
będą faktycznie wykonywane w takich konfiguracjach?
Zapiszmy teraz jak inne instrukcje korzystają z dodatkowej informacji
(śladu) zawartej w konfiguracjach.
Oczywiście beneficjentem tej informacji jest instrukcji <math> \mathbf{loop}\, </math>:
<math>
\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''}
</math>
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>,
albo rozpoczynamy kolejną iterację.
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
<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ę
''normalnie'', kontynuujemy wykonanie pętli podobnie jak w przypadku
wywołania <math> \mathbf{continue} </math>:
<math>
\frac{I, s \,\longrightarrow\, s' \quad \quad \mathbf{loop}\, I, s' \,\longrightarrow\, s''}
    {\mathbf{loop}\, I, s \,\longrightarrow\, s''}
</math>
'''Pytanie:''' czy potrzebujemy dodatkowo reguł postaci:
<math>
\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}}
</math>
Okazuje się że nie, ponieważ ślad powinien zostać zawsze
''wymazany'' przez pętlę <math> \mathbf{loop}\, </math>.
Poza tym reguły te wykraczałyby poza klasyczna podejście semantyki
naturalnej, w którym zwykle bezpośrednio definiujemy
tranzycje postaci <math> I, s \,\longrightarrow\, s' </math>.
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 <math> \mbox{było-}\mathbf{exit} </math>:
<math>
\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}}
</math>
<math>
\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{true} \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}}
</math>
<math>
\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}}
</math>
Pominęliśmy zupełnie analogiczne reguły dla konfiguracji
<math> s', \mbox{było-}\mathbf{continue} </math>.
Zwróćmy szczególnie uwagę na ostatnią regułę dla pętli <math> \mathbf{while}\, </math>:
wyraża ona przypadek, gdy ślad <math> \mathbf{exit} </math> 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.
Zauważmy też, że dla pętli <math> \mathbf{while}\, </math> nie rozpatrujemy przypadku,
gdy dozór <math> b </math> oblicza się do <math> \mathbf{true} </math>, gdyż w tym przypadku
nie ma możliwości wygenerowania śladu.
Zauważmy, że nasze reguły nie pozwalają na dodanie drugiego
(kolejnego) śladu!
==== Rozwiązanie 2 (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:
<math>
\mathbf{exit}, s \,\Longrightarrow\, s, \mbox{było-}\mathbf{exit}
\quad \quad
\mathbf{continue}, s \,\Longrightarrow\, s, \mbox{było-}\mathbf{continue}.
</math>
Ponadto musimy określić sposób, w jaki mały krok
mniejszej instrukcji zostaje zamieniony na mały krok
większej. Np.
<math>
\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}.
</math>
Zauważmy, że nie musimy zajmowac się przypadkiem, gdy ślad
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>,
ponieważ ślad nie może powstać podczas oblcizania dozoru!
Wreszcie zobaczmy jak zachowuje się pętla <math> \mathbf{loop}\, </math>:
<math>
\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'}
</math>
Reguły te są prawie identyczne do reguł semantyki naturalnej dla tej
sytuacji!
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
''natychmiast'' widoczna w instrukcji <math> \mathbf{loop}\, I </math>, nawet jeśli
<math> \mathbf{exit} </math> czy <math> CONT\,\mathbf{in}\,IE </math> zostało wywołane głęboko wewnątrz
<math> I </math>!
Niestety, powyzsze 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.
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>.
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>:
<math>
\mathbf{loop}\, I, s \,\Longrightarrow\, I \,\mathbf{then}\, \mathbf{loop}\, I, s.
</math>
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
<math> \mbox{było-}\mathbf{continue} </math> pojawią się nie w instrukcji wewnętrznej,
ale w jej ''kopii'' umieszczonej przed <math> \,\mathbf{then}\, </math>:
<math>
\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'}
</math>
A ponieważ wewnątrz kopii mogą być zagnieżdzone instrukcje
<math> \mathbf{loop}\, </math> potrzebujemy dodatkowej reguły:
<math>
\frac{I', s \,\Longrightarrow\, I'', s'}
    {I' \,\mathbf{then}\, \mathbf{loop}\, I, s \,\Longrightarrow\, I'' \,\mathbf{then}\, \mathbf{loop}\, I, s'}
</math>
Na koniec zauważmy, że stan <math> s' </math> w
pierwszych dwóch z powyższych trzech reguł nigdy nie jest różny
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 parze z <math> \mbox{było-}\mathbf{exit} </math> albo <math> \mbox{było-}\mathbf{continue} </math> jest nadmiarowe
i może zostać wyeliminowane.
Zatem ostatecznie nasze reguły mogą wyglądać tak:
<math>
\mathbf{exit}, s \,\Longrightarrow\, \mbox{było-}\mathbf{exit}
\quad \quad
\mathbf{continue}, s \,\Longrightarrow\, \mbox{było-}\mathbf{continue}
</math>
<math>
\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}}
</math>
<math>
\mathbf{loop}\, I, s \,\Longrightarrow\, I \,\mathbf{then}\, \mathbf{loop}\, I, s.
</math>
<math>
\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}
</math>
<math>
\frac{I', s \,\Longrightarrow\, I'', s'}
    {I' \,\mathbf{then}\, \mathbf{loop}\, I, s \,\Longrightarrow\, I'' \,\mathbf{then}\, \mathbf{loop}\, I, s'}
</math>
a zbiór konfiguracji poszerzamy tylko o
<math>
\{ \mbox{było-}\mathbf{exit}, \mbox{było-}\mathbf{continue} \}.
</math>
== Zadania domowe ==
==== Zadanie 1 ====
Zaproponuj semantykę mało-krokową języka z zdania 2.
Czy różni się ona istotnie od semantyki naturalnej?
==== Zadanie 2 ====
Napisz semantyję naturalną dla nieznacznie rozszerzonej wersji instrukcji <math> \mathbf{loop}\, </math>:
<math>
I \, ::= \,\,
      x: \mathbf{loop}\, I \,\,|\,\,
      \mathbf{exit} x \,\,|\,\,
      \mathbf{continue} x
</math>
Identyfikator <math> x </math> pełni tutaj rolę etykiety przypisanej
instrukcji <math> \mathbf{loop}\, </math>, jest też parametrem dwóch pozostałych
instrukcji. <math> \mathbf{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ą
pętlę o etykiecie <math> x </math>. Np. program
<math>
x: \mathbf{loop}\,\\
\quad \quad a := 1;
\quad \quad y: \mathbf{loop}\,
\quad \quad \quad \quad \mathbf{exit} x;
\quad \quad \quad \quad a := a-10;
\quad \quad a := a+1;
a := a+2;
</math>
kończy działanie z wartością zmiennej <math> a = 3 </math>.
Zauważmy, że musieliśmy jakoś określić, do wnętrza której pętli
<math> \mathbf{loop}\, </math> należą trzy ostatnie instrukcje. Użyliśmy to tego celu
wcięć a 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ę <math> \mathbf{loop}\, </math>,
np. <math> \mathbf{loop}\, I \,\mathbf{end}\mathbf{loop}\, </math>.
==== Zadanie 3 ====
Napisz semantykę naturalną i mało-krokową dla rozszerzenia
języka Tiny o wyrażenia z efektami ubocznymi:
<math>
e \,  ::= \,\, 
        \ldots  \,\,|\,\,
        \,\mathbf{do}\, I \,\mathbf{then}\, e  \,\,|\,\,
        x := e  \,\,|\,\,
        x++  \,\,|\,\,  \ldots
</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
jak wartość wyrażenia <math> e </math> a efektem ubocznym jest
podstawienie tej wartości na zmienną <math> x </math>.

Wersja z 08:21, 7 sie 2006


Zawartość

Kończymy semantykę małych kroków i rozpoczynamy semantykę naturalną (duże kroki). Uzupełnimy semantykę naturalną języka Tiny o semantykę naturalną dla wyrażeń boolowskich i arytmetycznych i semantykę dla błędów wykonania. Wreszcie dodamy instrukcję pętli 𝐥𝐨𝐨𝐩 i instrukcje niestrukturalnego zakończenia pętli (instrukcje 𝐞𝐱𝐢𝐭 i 𝐜𝐨𝐧𝐭𝐢𝐧𝐮𝐞).


Rozszerzenia semantyki języka Tiny

Zadanie 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 jezyka Tiny:

b::=l|e1≤e2|¬b|b1∧b2|…

l::=𝐭𝐫𝐮𝐞|𝐭𝐫𝐮𝐞

e::=n|x|e1+e2|…

n::=0|1|…

x::=…(identyfikatory)…

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

e,s⟶nb,s⟶l,

gdzie s∈𝐒𝐭𝐚𝐭𝐞, n∈ jest liczbą całkowitą, n∈𝐍𝐮𝐦, a l∈𝐁𝐨𝐨𝐥={𝐭𝐫𝐮𝐞,𝐭𝐫𝐮𝐞}. 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

((𝐄𝐱𝐩∪𝐁𝐄𝐱𝐩∪𝐒𝐭𝐦𝐭)×𝐒𝐭𝐚𝐭𝐞)⋃𝐍𝐮𝐦∪𝐁𝐨𝐨𝐥∪𝐒𝐭𝐚𝐭𝐞 a konfiguracje końcowe to 𝐒𝐭𝐚𝐭𝐞 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: 

b,s⟶𝐭𝐫𝐮𝐞I;𝐰𝐡𝐢𝐥𝐞b𝐝𝐨I,s⟶s′𝐰𝐡𝐢𝐥𝐞b𝐝𝐨I,s⟶s′

b,s⟶𝐭𝐫𝐮𝐞𝐰𝐡𝐢𝐥𝐞b𝐝𝐨I,s⟶s

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

n,s⟶nl,s⟶l.

Operatory arytmetyczne definiujemy następująco: 

e1,s⟶n1e2,s⟶n2n=n1+n2e1+e2,s⟶n

Czyli aby obliczyć sumę e1+e2 w stanie s, trzeba najpierw obliczyć e1 i e2 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 arytmnetycznych, oraz dla spójników logicznych: 

b1,s⟶l1b2,s⟶l2l=l1∧l2b1∧b2,s⟶l

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

b1,s⟶𝐭𝐫𝐮𝐞b1∧b2,s⟶𝐭𝐫𝐮𝐞b1,s⟶𝐭𝐫𝐮𝐞b2,s⟶lb1∧b2,s⟶l

Inny wariant to wariant prawo-stronny ( najpierw b2, potem b1). Wreszcie rozważmy kombinację obydwu semantyk (reguły równoległe): 

b1,s⟶𝐭𝐫𝐮𝐞b1∧b2,s⟶𝐭𝐫𝐮𝐞b2,s⟶𝐭𝐫𝐮𝐞b1∧b2,s⟶𝐭𝐫𝐮𝐞

Czyli jeśli którekolwiek z podwyrażeń daje wynik 𝐭𝐫𝐮𝐞, to taki wynik zyskuje całe wyrażenie. Dodatkowo potrzebujemy jeszcze reguły:

b1,s⟶𝐭𝐫𝐮𝐞b2,s⟶𝐭𝐫𝐮𝐞b1∧b2,s⟶𝐭𝐫𝐮𝐞

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


Zadanie 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 (szkic)

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ą Blad. Reguła opisująca powstanie błędu może wyglądać np. tak:

e2,s⟶0e1/e2,s⟶Blad

Pomijamy tutaj reguły dla przypadku, gdy e2 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:

e1/0,s⟹Blad,s

i zamiast pojedyńczej konfiguracji końcowej Blad potrzebowalibyśmy oczywiście całego zbioru {Blad}×𝐒𝐭𝐚𝐭𝐞.

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. 

e1,s⟶Blade1≤e2,s⟶Blade2,s⟶Blade1≤e2,s⟶Blad

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

b⟶Blad𝐢𝐟b𝐭𝐡𝐞𝐧I1𝐞𝐥𝐬𝐞I2,s⟶Blad

b⟶Blad𝐰𝐡𝐢𝐥𝐞b𝐝𝐨I,s⟶Blad

e,s⟶Bladx:=e,s⟶Blad

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

I1,s⟶BladI1;I2,s⟶Blad

b,s⟶𝐭𝐫𝐮𝐞I1,s⟶Blad𝐢𝐟b𝐭𝐡𝐞𝐧I1𝐞𝐥𝐬𝐞I2,s⟶Bladb,s⟶𝐭𝐫𝐮𝐞I2,s⟶Blad𝐢𝐟b𝐭𝐡𝐞𝐧I1𝐞𝐥𝐬𝐞I2,s⟶Blad

b,s⟶𝐭𝐫𝐮𝐞I,s⟶Blad𝐰𝐡𝐢𝐥𝐞b𝐝𝐨I,s⟶Bladb,s⟶𝐭𝐫𝐮𝐞I,s⟶s′𝐰𝐡𝐢𝐥𝐞b𝐝𝐨I,s′⟶Blad𝐰𝐡𝐢𝐥𝐞b𝐝𝐨I,s⟶Blad


Zadanie 3

Rozszerz 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 pętli 𝐥𝐨𝐨𝐩 i kontynuuje wykonanie programu od pierwszej instrukcji za tą pętlą. Instrukcje 𝐜𝐨𝐧𝐭𝐢𝐧𝐮𝐞 powraca na początek instrukcji wewnętrznej najbliższej pętli.

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


Rozwiązanie 1 (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 𝐞𝐱𝐢𝐭 lub 𝐜𝐨𝐧𝐭𝐢𝐧𝐮𝐞. Oto odpowiednie reguły: 

𝐞𝐱𝐢𝐭,s⟶s,było-𝐞𝐱𝐢𝐭𝐜𝐨𝐧𝐭𝐢𝐧𝐮𝐞,s⟶s,było-𝐜𝐨𝐧𝐭𝐢𝐧𝐮𝐞.

Czyli instrukcje 𝐞𝐱𝐢𝐭 i 𝐜𝐨𝐧𝐭𝐢𝐧𝐮𝐞 nie modyfikują stanu s, ale zostawiają po sobie \ślad". Zauważmy, że taki ślad zostaje pozostawiony tylko wtedy, jesli nie było dotychczas innego śladu, to znaczy jeśli 𝐞𝐱𝐢𝐭 (lub 𝐜𝐨𝐧𝐭𝐢𝐧𝐮𝐞) zostało wykonane w zwykłym stanie s. Oczywiście poszerzamy odpowiednio zbiór konfiguracji o:

</math>[ \mathbf{State} \times \{ \mbox{było-}\mathbf{exit}, \mbox{było-}\mathbf{continue} \} </math> , Pytanie: jakie powinno być zachowanie 𝐞𝐱𝐢𝐭 i 𝐜𝐨𝐧𝐭𝐢𝐧𝐮𝐞 w konfiguracji s,było-𝐞𝐱𝐢𝐭 lub s,było-𝐜𝐨𝐧𝐭𝐢𝐧𝐮𝐞? Czy instrukcje 𝐞𝐱𝐢𝐭 i 𝐜𝐨𝐧𝐭𝐢𝐧𝐮𝐞 będą faktycznie wykonywane w takich konfiguracjach?

Zapiszmy teraz jak inne instrukcje korzystają z dodatkowej informacji (śladu) zawartej w konfiguracjach. Oczywiście beneficjentem tej informacji jest instrukcji 𝐥𝐨𝐨𝐩: 

I,s⟶s′,było-𝐞𝐱𝐢𝐭𝐥𝐨𝐨𝐩I,s⟶s′I,s⟶s′,było-𝐜𝐨𝐧𝐭𝐢𝐧𝐮𝐞𝐥𝐨𝐨𝐩I,s′⟶s″𝐥𝐨𝐨𝐩I,s⟶s″

Czyli w zależności od tego, jaki ślad został zarejestrowany podczas wykonania I, albo kończymy wykonanie pętli 𝐥𝐨𝐨𝐩, albo rozpoczynamy kolejną iterację. Zauważmy, że stan s′ może być różny od s, ponieważ zanim wykonała się ktoraś z instrukcji 𝐞𝐱𝐢𝐭 lub 𝐜𝐨𝐧𝐭𝐢𝐧𝐮𝐞, 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 𝐜𝐨𝐧𝐭𝐢𝐧𝐮𝐞: 

I,s⟶s′𝐥𝐨𝐨𝐩I,s′⟶s″𝐥𝐨𝐨𝐩I,s⟶s″

Pytanie: czy potrzebujemy dodatkowo reguł postaci: 

I,s⟶s′𝐥𝐨𝐨𝐩I,s′⟶s″,było-𝐞𝐱𝐢𝐭𝐥𝐨𝐨𝐩I,s⟶s″,było-𝐞𝐱𝐢𝐭I,s⟶s′,było-𝐜𝐨𝐧𝐭𝐢𝐧𝐮𝐞𝐥𝐨𝐨𝐩I,s′⟶s″,było-𝐞𝐱𝐢𝐭𝐥𝐨𝐨𝐩I,s⟶s″,było-𝐞𝐱𝐢𝐭

Okazuje się że nie, ponieważ ślad powinien zostać zawsze wymazany przez pętlę 𝐥𝐨𝐨𝐩. Poza tym reguły te wykraczałyby poza klasyczna podejście semantyki naturalnej, w którym zwykle bezpośrednio definiujemy tranzycje postaci I,s⟶s′.

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 było-𝐞𝐱𝐢𝐭: 

I1,s⟶s′,było-𝐞𝐱𝐢𝐭I1;I2,s⟶s′,było-𝐞𝐱𝐢𝐭I1,s⟶s′I2,s′⟶s″,było-𝐞𝐱𝐢𝐭I1;I2,s⟶s″,było-𝐞𝐱𝐢𝐭

b,s⟶𝐭𝐫𝐮𝐞I1,s⟶s′,było-𝐞𝐱𝐢𝐭𝐢𝐟b𝐭𝐡𝐞𝐧I1𝐞𝐥𝐬𝐞I2,s⟶s′,było-𝐞𝐱𝐢𝐭b,s⟶𝐭𝐫𝐮𝐞I2,s⟶s′,było-𝐞𝐱𝐢𝐭𝐢𝐟b𝐭𝐡𝐞𝐧I1𝐞𝐥𝐬𝐞I2,s⟶s′,było-𝐞𝐱𝐢𝐭

b,s⟶𝐭𝐫𝐮𝐞I,s⟶s′,było-𝐞𝐱𝐢𝐭𝐰𝐡𝐢𝐥𝐞b𝐝𝐨I,s⟶s′,było-𝐞𝐱𝐢𝐭b,s⟶𝐭𝐫𝐮𝐞I,s⟶s′𝐰𝐡𝐢𝐥𝐞b𝐝𝐨I,s′⟶s″,było-𝐞𝐱𝐢𝐭𝐰𝐡𝐢𝐥𝐞b𝐝𝐨I,s⟶s′,było-𝐞𝐱𝐢𝐭

Pominęliśmy zupełnie analogiczne reguły dla konfiguracji s′,było-𝐜𝐨𝐧𝐭𝐢𝐧𝐮𝐞. Zwróćmy szczególnie uwagę na ostatnią regułę dla pętli 𝐰𝐡𝐢𝐥𝐞: wyraża ona przypadek, gdy ślad 𝐞𝐱𝐢𝐭 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. Zauważmy też, że dla pętli 𝐰𝐡𝐢𝐥𝐞 nie rozpatrujemy przypadku, gdy dozór b oblicza się do 𝐭𝐫𝐮𝐞, gdyż w tym przypadku nie ma możliwości wygenerowania śladu.

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


Rozwiązanie 2 (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: 

𝐞𝐱𝐢𝐭,s⟹s,było-𝐞𝐱𝐢𝐭𝐜𝐨𝐧𝐭𝐢𝐧𝐮𝐞,s⟹s,było-𝐜𝐨𝐧𝐭𝐢𝐧𝐮𝐞.

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

I1,s⟹s′,było-𝐞𝐱𝐢𝐭I1;I2,s⟹s′,było-𝐞𝐱𝐢𝐭 i analogicznie dla było-𝐜𝐨𝐧𝐭𝐢𝐧𝐮𝐞.

Zauważmy, że nie musimy zajmowac się przypadkiem, gdy ślad powstaje w I2, bo wybraliśmy podejście mało-krokowe. Ponadto, nie musimy opisywać instrukcji warunkowej i pętli 𝐰𝐡𝐢𝐥𝐞, ponieważ ślad nie może powstać podczas oblcizania dozoru!

Wreszcie zobaczmy jak zachowuje się pętla 𝐥𝐨𝐨𝐩: 

I,s⟹s′,było-𝐞𝐱𝐢𝐭𝐥𝐨𝐨𝐩I,s⟹s′I,s⟹s′,było-𝐜𝐨𝐧𝐭𝐢𝐧𝐮𝐞𝐥𝐨𝐨𝐩I,s⟹𝐥𝐨𝐨𝐩I,s′

Reguły te są prawie identyczne do reguł semantyki naturalnej dla tej sytuacji! Natomiast korzystamy z tego, że w podejściu mało-krokowym zmiana konfiguracji na s′,było-𝐞𝐱𝐢𝐭 czy s′,było-𝐜𝐨𝐧𝐭𝐢𝐧𝐮𝐞 jest natychmiast widoczna w instrukcji 𝐥𝐨𝐨𝐩I, nawet jeśli 𝐞𝐱𝐢𝐭 czy CONT𝐢𝐧IE zostało wywołane głęboko wewnątrz I!

Niestety, powyzsze 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. I w związku z tym nie potrafimy poprawnie powrócić do wykonywania pętli 𝐥𝐨𝐨𝐩 po wywołaniu 𝐜𝐨𝐧𝐭𝐢𝐧𝐮𝐞.

Prostym sposobem poprawienia naszego blędu jest rozszerzenie składni tak, aby możliwe było jednorazowe rozwinięcie pętli 𝐥𝐨𝐨𝐩: 

𝐥𝐨𝐨𝐩I,s⟹I𝐭𝐡𝐞𝐧𝐥𝐨𝐨𝐩I,s.

Teraz możemy zapisać dwie powyższe reguły dla 𝐥𝐨𝐨𝐩 w poprawnej wersji, pamiętając o tym, że było-𝐞𝐱𝐢𝐭 i było-𝐜𝐨𝐧𝐭𝐢𝐧𝐮𝐞 pojawią się nie w instrukcji wewnętrznej, ale w jej kopii umieszczonej przed 𝐭𝐡𝐞𝐧: 

I′,s⟹s′,było-𝐞𝐱𝐢𝐭I′𝐭𝐡𝐞𝐧𝐥𝐨𝐨𝐩I,s⟹s′I′,s⟹s′,było-𝐜𝐨𝐧𝐭𝐢𝐧𝐮𝐞I;𝐭𝐡𝐞𝐧𝐥𝐨𝐨𝐩I,s⟹𝐥𝐨𝐨𝐩I,s′

A ponieważ wewnątrz kopii mogą być zagnieżdzone instrukcje 𝐥𝐨𝐨𝐩 potrzebujemy dodatkowej reguły: 

I′,s⟹I″,s′I′𝐭𝐡𝐞𝐧𝐥𝐨𝐨𝐩I,s⟹I″𝐭𝐡𝐞𝐧𝐥𝐨𝐨𝐩I,s′

Na koniec zauważmy, że stan s′ w pierwszych dwóch z powyższych trzech 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 było-𝐞𝐱𝐢𝐭 albo było-𝐜𝐨𝐧𝐭𝐢𝐧𝐮𝐞 jest nadmiarowe i może zostać wyeliminowane.

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

𝐞𝐱𝐢𝐭,s⟹było-𝐞𝐱𝐢𝐭𝐜𝐨𝐧𝐭𝐢𝐧𝐮𝐞,s⟹było-𝐜𝐨𝐧𝐭𝐢𝐧𝐮𝐞

I1,s⟹było-𝐞𝐱𝐢𝐭I1;I2,s⟹było-𝐞𝐱𝐢𝐭I1,s⟹było-𝐜𝐨𝐧𝐭𝐢𝐧𝐮𝐞I1;I2,s⟹było-𝐜𝐨𝐧𝐭𝐢𝐧𝐮𝐞

𝐥𝐨𝐨𝐩I,s⟹I𝐭𝐡𝐞𝐧𝐥𝐨𝐨𝐩I,s.

I′,s⟹było-𝐞𝐱𝐢𝐭I′𝐭𝐡𝐞𝐧𝐥𝐨𝐨𝐩I,s⟹sI′,s⟹było-𝐜𝐨𝐧𝐭𝐢𝐧𝐮𝐞I;𝐭𝐡𝐞𝐧𝐥𝐨𝐨𝐩I,s⟹𝐥𝐨𝐨𝐩I,s

I′,s⟹I″,s′I′𝐭𝐡𝐞𝐧𝐥𝐨𝐨𝐩I,s⟹I″𝐭𝐡𝐞𝐧𝐥𝐨𝐨𝐩I,s′

a zbiór konfiguracji poszerzamy tylko o {było-𝐞𝐱𝐢𝐭,było-𝐜𝐨𝐧𝐭𝐢𝐧𝐮𝐞}.


Zadania domowe

Zadanie 1

Zaproponuj semantykę mało-krokową języka z zdania 2. Czy różni się ona istotnie od semantyki naturalnej?


Zadanie 2

Napisz semantyję naturalną dla nieznacznie rozszerzonej wersji instrukcji 𝐥𝐨𝐨𝐩:

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

Identyfikator x pełni tutaj rolę etykiety przypisanej instrukcji 𝐥𝐨𝐨𝐩, 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ą pętlę o etykiecie x. Np. program

Parser nie mógł rozpoznać (błąd składni): {\displaystyle x: \mathbf{loop}\,\\ \quad \quad a := 1; \quad \quad y: \mathbf{loop}\, \quad \quad \quad \quad \mathbf{exit} x; \quad \quad \quad \quad a := a-10; \quad \quad a := a+1; a := a+2; }

kończy działanie z wartością zmiennej a=3. Zauważmy, że musieliśmy jakoś określić, do wnętrza której pętli 𝐥𝐨𝐨𝐩 należą trzy ostatnie instrukcje. Użyliśmy to tego celu wcięć a 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𝐞𝐧𝐝𝐥𝐨𝐨𝐩.


Zadanie 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=10170”