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 20: Linia 20:


==== Rozwiązanie ====
==== Rozwiązanie ====
<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
Linia 55: Linia 57:
Chcemy, aby tranzycje wyrażen wyglądały następująco:
Chcemy, aby tranzycje wyrażen wyglądały następująco:


<math>
<math>
e, s \longrightarrow n   
e, s \longrightarrow n   
\quad \quad \quad
\quad \quad \quad
Linia 78: Linia 80:
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>
\frac{b, s \,\longrightarrow\, \mathbf{true}  \quad \quad  I; \mathbf{while}\, b \,\mathbf{do}\, I, s \,\longrightarrow\, s'}
\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'}
       {\mathbf{while}\, b \,\mathbf{do}\, I, s \,\longrightarrow\, s'}
</math>
</math>


<math>
<math>
\frac{b, s \,\longrightarrow\, \mathbf{true}}
\frac{b, s \,\longrightarrow\, \mathbf{true}}
     {\mathbf{while}\, b \,\mathbf{do}\, I, s \,\longrightarrow\, s}
     {\mathbf{while}\, b \,\mathbf{do}\, I, s \,\longrightarrow\, s}
Linia 92: Linia 94:
Zacznijmy od stalych arytmetycznych i boolowskich:
Zacznijmy od stalych arytmetycznych i boolowskich:


<math>
<math>
n, s \,\longrightarrow\, n
n, s \,\longrightarrow\, n
\quad \quad
\quad \quad
Linia 100: Linia 102:
Operatory arytmetyczne definiujemy następująco:
Operatory arytmetyczne definiujemy następująco:


<math>
<math>
\frac{e_1, s \,\longrightarrow\, n_1  \quad \quad   
\frac{e_1, s \,\longrightarrow\, n_1  \quad \quad   
       e_2, s \,\longrightarrow\, n_2 \quad \quad
       e_2, s \,\longrightarrow\, n_2 \quad \quad
Linia 119: Linia 121:
arytmnetycznych, oraz dla spójników logicznych:
arytmnetycznych, oraz dla spójników logicznych:


<math>
<math>
\frac{b_1, s \,\longrightarrow\, l_1  \quad \quad
\frac{b_1, s \,\longrightarrow\, l_1  \quad \quad
       b_2, s \,\longrightarrow\, l_2  \quad \quad   
       b_2, s \,\longrightarrow\, l_2  \quad \quad   
Linia 128: Linia 130:
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>
\frac{b_1, s \,\longrightarrow\, \mathbf{true}}
\frac{b_1, s \,\longrightarrow\, \mathbf{true}}
     {b_1 \land b_2, s \,\longrightarrow\, \mathbf{true}}
     {b_1 \land b_2, s \,\longrightarrow\, \mathbf{true}}
Linia 141: Linia 143:
Wreszcie rozważmy kombinację obydwu semantyk (reguły ''równoległe''):
Wreszcie rozważmy kombinację obydwu semantyk (reguły ''równoległe''):


<math>
<math>
\frac{b_1, s \,\longrightarrow\, \mathbf{true}}
\frac{b_1, s \,\longrightarrow\, \mathbf{true}}
     {b_1 \land b_2, s \,\longrightarrow\, \mathbf{true}}
     {b_1 \land b_2, s \,\longrightarrow\, \mathbf{true}}
Linia 162: Linia 164:
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 ćwiczenie.
negacji oraz dla instrukcji przypisania pozostawiamy jako proste
ćwiczenie.
 
</div></div>




Linia 221: Linia 226:
jest wstrzymame.
jest wstrzymame.


<math>
<math>
\frac{e_1, s \,\longrightarrow\, \mathtt{Blad}}
\frac{e_1, s \,\longrightarrow\, \mathtt{Blad}}
     {e_1 \leq e_2, s \,\longrightarrow\, \mathtt{Blad}}
     {e_1 \leq e_2, s \,\longrightarrow\, \mathtt{Blad}}
Linia 231: Linia 236:
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>
\frac{b \,\longrightarrow\, \mathtt{Blad}}
\frac{b \,\longrightarrow\, \mathtt{Blad}}
{\mathbf{if}\, b \,\mathbf{then}\, I_1 \,\mathbf{else}\, I_2, s \,\longrightarrow\, \mathtt{Blad}}
{\mathbf{if}\, b \,\mathbf{then}\, I_1 \,\mathbf{else}\, I_2, s \,\longrightarrow\, \mathtt{Blad}}
</math>
</math>


<math>
<math>
\frac{b \,\longrightarrow\, \mathtt{Blad}}
\frac{b \,\longrightarrow\, \mathtt{Blad}}
{\mathbf{while}\, b \,\mathbf{do}\, I, s \,\longrightarrow\, \mathtt{Blad}}
{\mathbf{while}\, b \,\mathbf{do}\, I, s \,\longrightarrow\, \mathtt{Blad}}
</math>
</math>


<math>
<math>
\frac{e, s \,\longrightarrow\, \mathtt{Blad}}
\frac{e, s \,\longrightarrow\, \mathtt{Blad}}
     {x := e, s \,\longrightarrow\, \mathtt{Blad}}
     {x := e, s \,\longrightarrow\, \mathtt{Blad}}
Linia 248: Linia 253:
I wreszcie błąd powinien propagować się do kolejnych instrukcji:
I wreszcie błąd powinien propagować się do kolejnych instrukcji:


<math>
<math>
\frac{I_1, s \,\longrightarrow\, \mathtt{Blad}}
\frac{I_1, s \,\longrightarrow\, \mathtt{Blad}}
     {I_1;\, I_2, s \,\longrightarrow\, \mathtt{Blad}}
     {I_1;\, I_2, s \,\longrightarrow\, \mathtt{Blad}}
</math>
</math>


<math>
<math>
\frac{b, s \,\longrightarrow\, \mathbf{true} \quad \quad I_1, 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}}
     {\mathbf{if}\, b \,\mathbf{then}\, I_1 \,\mathbf{else}\, I_2, s \,\longrightarrow\, \mathtt{Blad}}
Linia 261: Linia 266:
</math>
</math>


<math>
<math>
\frac{b, s \,\longrightarrow\, \mathbf{true} \quad \quad I, 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}}
     {\mathbf{while}\, b \,\mathbf{do}\, I, s \,\longrightarrow\, \mathtt{Blad}}
Linia 302: Linia 307:
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
Linia 329: Linia 334:
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'}
Linia 348: Linia 353:
wywołania <math> \mathbf{continue} </math>:
wywołania <math> \mathbf{continue} </math>:


<math>
<math>
\frac{I, s \,\longrightarrow\, s' \quad \quad \mathbf{loop}\, I, s' \,\longrightarrow\, s''}
\frac{I, s \,\longrightarrow\, s' \quad \quad \mathbf{loop}\, I, s' \,\longrightarrow\, s''}
     {\mathbf{loop}\, I, s \,\longrightarrow\, s''}
     {\mathbf{loop}\, I, s \,\longrightarrow\, s''}
Linia 355: Linia 360:
'''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}}
Linia 375: Linia 380:
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}}
Linia 383: Linia 388:
</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}}
Linia 391: Linia 396:
</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}}
Linia 429: Linia 434:
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
Linia 439: Linia 444:
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}}
Linia 453: Linia 458:
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'}
Linia 466: Linia 471:
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> CONT\,\mathbf{in}\,IE </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>!


Linia 478: Linia 483:
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>
\mathbf{loop}\, I, s \,\Longrightarrow\, I \,\mathbf{then}\, \mathbf{loop}\, I, s.
\mathbf{loop}\, I, s \,\Longrightarrow\, I \,\mathbf{then}\, \mathbf{loop}\, I, s.
</math>
</math>
Linia 487: Linia 492:
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'}
Linia 498: Linia 503:
<math> \mathbf{loop}\, </math> potrzebujemy dodatkowej reguły:
<math> \mathbf{loop}\, </math> potrzebujemy dodatkowej reguły:


<math>
<math>
\frac{I', s \,\Longrightarrow\, I'', s'}
\frac{I', s \,\Longrightarrow\, I'', s'}
     {I' \,\mathbf{then}\, \mathbf{loop}\, I, s \,\Longrightarrow\, I'' \,\mathbf{then}\, \mathbf{loop}\, I, s'}
     {I' \,\mathbf{then}\, \mathbf{loop}\, I, s \,\Longrightarrow\, I'' \,\mathbf{then}\, \mathbf{loop}\, I, s'}
Linia 512: Linia 517:
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
Linia 518: Linia 523:
</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}}
Linia 526: Linia 531:
</math>
</math>


<math>
<math>
\mathbf{loop}\, I, s \,\Longrightarrow\, I \,\mathbf{then}\, \mathbf{loop}\, I, s.
\mathbf{loop}\, I, s \,\Longrightarrow\, I \,\mathbf{then}\, \mathbf{loop}\, I, s.
</math>
</math>


<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}
Linia 538: Linia 543:
</math>
</math>


<math>
<math>
\frac{I', s \,\Longrightarrow\, I'', s'}
\frac{I', s \,\Longrightarrow\, I'', s'}
     {I' \,\mathbf{then}\, \mathbf{loop}\, I, s \,\Longrightarrow\, I'' \,\mathbf{then}\, \mathbf{loop}\, I, s'}
     {I' \,\mathbf{then}\, \mathbf{loop}\, I, s \,\Longrightarrow\, I'' \,\mathbf{then}\, \mathbf{loop}\, I, s'}

Wersja z 08:27, 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


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 𝐜𝐨𝐧𝐭𝐢𝐧𝐮𝐞 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=10171”