Semantyka i weryfikacja programów/Ćwiczenia 3: Różnice pomiędzy wersjami

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
← poprzednia edycja
WizualnieWikikod
Sl (dyskusja | edycje)
101 edycji
Nie podano opisu zmian
m Zastępowanie tekstu – „,↵</math>” na „</math>,”
 
(Nie pokazano 17 wersji utworzonych przez 3 użytkowników)
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ą wyrażeń boolowskich i arytmetycznych oraz semantykę błędów wykonania.
Wreszcie dodamy nową instrukcję pętli <math>\mathbf{loop}\ </math>,, pozwalającą na niestrukturalne przerwanie lub wznowienie iteracji (instrukcje <math>\mathbf{exit}</math> i <math>\mathbf{continue}</math>).
== Rozszerzenia semantyki języka Tiny ==
{{cwiczenie|1|cw1|
Zdefiniuj znaczenie wyrażeń boolowskich i arytmetycznych w języku TINY w stylu dużych kroków (semantyka naturalna).
}}
<div class="mw-collapsible mw-made=collapsible mw-collapsed">
<span class="mw-collapsible-toogle mw-collapsible-toogle-default style="font-variant:small-caps">Rozwiązanie</span>
<div class="mw-collapsible-content" style="display:none">
Przypomnijmy składnię wyrażeń boolowskich i arytmetycznych języka TINY:
<math>
b \, ::= \,\,
        l \,\,|\,\,
        e_1 \leq e_2  \,\,|\,\,
        \neg b  \,\,|\,\,
        b_1  \land  b_2  \,\,|\,\, \ldots 
</math>
<math>
l \, ::= \,\,
        \mathbf{true}    \,\,|\,\,
        \mathbf{false}       
</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żeń 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{false} \}</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{false}}
    {\mathbf{while}\, b \,\mathbf{do}\, I, s \,\longrightarrow\, s}
</math>
Podobnie dla instrukcji warunkowej.
Teraz zajmiemy się tranzycjami dla wyrażeń.
Zacznijmy od stałych 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 arytmetycznych, 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>
(strategia gorliwa).
Reguły dla <math>\leq</math> są następujące:
<math>
\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}}
</math>
Oto inny wariant semantyki spójnika <math>\land</math>, tzw. strategia lewostronna (ponieważ rozpoczynamy od ''lewego'' koniunktu):
<math>
\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}
</math>
Inny wariant to strategia prawostronna (najpierw <math>b_2</math>, potem <math>b_1</math>).
Wreszcie rozważmy kombinację obydwu semantyk (strategia ''równoległa'' lub ''leniwa''):
<math>
\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}}
</math>
Czyli jeśli którekolwiek z podwyrażeń daje wynik <math>\mathbf{false}</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>
'''Pytanie:''' czy w naszym prostym języku wszystkie cztery strategie obliczania spójnika <math>\land</math> są równoważne?
Reguły dla negacji oraz dla instrukcji przypisania pozostawiamy jako proste ćwiczenie.
</div></div>
{{cwiczenie|2|cw2|
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ł.
}}
<div class="mw-collapsible mw-made=collapsible mw-collapsed">
<span class="mw-collapsible-toogle mw-collapsible-toogle-default style="font-variant:small-caps">Rozwiązanie</span>
<div class="mw-collapsible-content" style="display:none">
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 (duże i małe kroki):
<math>
\frac{e_2, s \,\longrightarrow\, 0}
{e_1 / e_2, s \,\longrightarrow\, \mathtt{Blad}}
\quad \quad
e_1 / 0, s \,\Longrightarrow, \mathtt{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>
\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
</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{false} \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>
Zwróćmy szczególnie uwagę na ostatnią regułę dla pętli <math>\mathbf{while}\ </math>,: 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.
</div></div>
{{cwiczenie|3|cw3|
Rozszerzmy 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 otaczającej pętli <math>\mathbf{loop}\ </math>, i kontynuuje wykonanie programu od pierwszej instrukcji za tą pętlą.
Instrukcja <math>\mathbf{continue}</math> powraca na początek instrukcji wewnętrznej najbliższej otaczającej pętli <math>\mathbf{loop}\ </math>,.
Pozważ zarówno semantykę naturalną, jak i semantykę małych kroków.
}}
<div class="mw-collapsible mw-made=collapsible mw-collapsed">
<span class="mw-collapsible-toogle mw-collapsible-toogle-default style="font-variant:small-caps">Rozwiązanie</span>
<div class="mw-collapsible-content" style="display:none">
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, jeśli 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" korzystającym z tej informacji jest instrukcja <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>,.
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{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}}
</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 <math>\mbox{było-}\mathbf{continue}</math>.
Zauważmy, że dla pętli <math>\mathbf{while}\ </math>, nie rozpatrujemy przypadku, gdy dozór <math>b</math> oblicza się do <math>\mathbf{false}</math>, gdyż w tym przypadku nie ma możliwości wygenerowania śladu.
Zauważmy też, że nasze reguły nie pozwalają na dodanie drugiego (kolejnego) śladu!
</div></div>
<div class="mw-collapsible mw-made=collapsible mw-collapsed">
<span class="mw-collapsible-toogle mw-collapsible-toogle-default style="font-variant:small-caps">Rozwiązanie</span>
<div class="mw-collapsible-content" style="display:none">
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>
Nie musimy zajmowac się przypadkiem, gdy ślad powstaje w <math>I_2</math>, bo wybraliśmy podejście małokrokowe.
Ponadto, nie musimy opisywać instrukcji warunkowej i pętli <math>\mathbf{while}\ </math>,, ponieważ ślad nie może powstać podczas obliczania 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 z regułami semantyki naturalnej dla tej sytuacji!
Natomiast korzystamy z tego, że w podejściu małokrokowym 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>\mathbf{continue}</math> zostało wywołane głęboko wewnątrz <math>I</math>!
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 <math>\mathbf{loop}\ </math>, po wywołaniu <math>\mathbf{continue}</math>.
Prostym sposobem poprawienia naszego błę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'}
\quad \quad
\frac{I', s \,\Longrightarrow, s'}
    {I' \,\mathbf{then}\, \mathbf{loop}\, I, s \,\Longrightarrow, \mathbf{loop}\, I, s'}
</math>
Potrzebujemy też dodatkowej reguły dla obliczeń wewnątrz instrukcji stojącej przed <math>\,\mathbf{then}\ </math>, (w szczególności może ona zawierać zagnieżdzone pętle <math>\mathbf{loop}\ </math>,):
<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 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}
\quad \quad
\frac{I', s \,\Longrightarrow, s'}
    {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 dwie nowe konfiguracje <math>\{ \mbox{było-}\mathbf{exit}, \mbox{było-}\mathbf{continue} \}</math>.
</div></div>
== Zadania domowe ==
{{cwiczenie|1|cw1.dom|
Zaproponuj semantykę małokrokową dla rozszerzeń języka Tiny, które
studiowaliśmy powyżej.
}}
{{cwiczenie|2|cw2.dom|
Napisz semantykę 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 związanej z instrukcją <math>\mathbf{loop}\ </math>,, jest też parametrem dwóch pozostałych instrukcji.
<math>\mathbf{exit} x</math> kończy teraz najbliższą otaczającą pętlę <math>\mathbf{loop}\ </math>, o etykiecie <math>x</math>. Podobnie <math>\mathbf{continue} x</math> wznawia najbliższą otaczającą pętlę o etykiecie <math>x</math>.
}}
{{przyklad|||
}}
Program
x: <math>\mathbf{loop}\ </math>,
  a := 1;
  y: <math>\mathbf{loop}\ </math>,
    <math>\mathbf{exit}</math> x;
    a := a-10;
  a := a+1;
a := a+2;
kończy działanie z wartością zmiennej <math>a = 3</math>.
Za pomocą wcięć określiliśmy, do wnętrza której pętli <math>\mathbf{loop}\ </math>, 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ę <math>\mathbf{loop}\ </math>,, np. <math>\mathbf{loop}\, I \,\mathbf{end}\mathbf{loop}\ </math>,.
{{cwiczenie|3|cw3.dom|
Napisz semantykę naturalną i małokrokową 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>.
}}

Aktualna wersja na dzień 21:43, 11 wrz 2023

Zawartość

Kończymy semantykę małych kroków i rozpoczynamy semantykę naturalną (duże kroki). Uzupełnimy semantykę naturalną języka TINY o semantykę naturalną wyrażeń boolowskich i arytmetycznych oraz semantykę błędów wykonania. Wreszcie dodamy nową instrukcję pętli 𝐥𝐨𝐨𝐩 ,, pozwalającą na niestrukturalne przerwanie lub wznowienie iteracji (instrukcje 𝐞𝐱𝐢𝐭 i 𝐜𝐨𝐧𝐭𝐢𝐧𝐮𝐞).


Rozszerzenia semantyki języka Tiny

Ćwiczenie 1

Zdefiniuj znaczenie wyrażeń boolowskich i arytmetycznych w języku TINY w stylu dużych kroków (semantyka naturalna).


Rozwiązanie


Ćwiczenie 2

Rozważ dodatkowo operację dzielenia:

e::=…|e1/e2

i rozszerz semantykę z poprzedniego zadania. Dzielenie przez zero jest błędem i kończy natychmiast wykonanie programu. Oprócz stanu wynikiem programu powinna byc informacja o błędzie, jeśli błąd wystąpił.


Rozwiązanie


Ćwiczenie 3

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

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

𝐥𝐨𝐨𝐩I to instrukcja pętli, I stanowi instrukcję wewnętrzną. Instrukcja 𝐞𝐱𝐢𝐭 wychodzi z nabliższej otaczającej pętli 𝐥𝐨𝐨𝐩 , i kontynuuje wykonanie programu od pierwszej instrukcji za tą pętlą. Instrukcja 𝐜𝐨𝐧𝐭𝐢𝐧𝐮𝐞 powraca na początek instrukcji wewnętrznej najbliższej otaczającej pętli 𝐥𝐨𝐨𝐩 ,.

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



Rozwiązanie


Rozwiązanie

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 𝐥𝐨𝐨𝐩 ,:

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

Identyfikator x pełni tutaj rolę etykiety związanej z instrukcją 𝐥𝐨𝐨𝐩 ,, jest też parametrem dwóch pozostałych instrukcji. 𝐞𝐱𝐢𝐭x kończy teraz najbliższą otaczającą pętlę 𝐥𝐨𝐨𝐩 , o etykiecie x. Podobnie 𝐜𝐨𝐧𝐭𝐢𝐧𝐮𝐞x wznawia najbliższą otaczającą pętlę o etykiecie x.

Przykład

Program 

x: 𝐥𝐨𝐨𝐩 ,
  a := 1; 
  y: 𝐥𝐨𝐨𝐩 ,
    𝐞𝐱𝐢𝐭 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 𝐥𝐨𝐨𝐩 , należy każda z trzech ostatnich instrukcji przypisania. Niejednoznaczność bierze się oczywiście stąd, że pracujemy ze składnią abstrakcyjną. Składnia konkretna zawierałaby prawdopodobnie jakąś konstukcję "zamykającą" pętlę 𝐥𝐨𝐨𝐩 ,, np. 𝐥𝐨𝐨𝐩I𝐞𝐧𝐝𝐥𝐨𝐨𝐩 ,.


Ćwiczenie 3

Napisz semantykę naturalną i małokrokową 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=82233”