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

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
 
m (Zastępowanie tekstu - "\Longrightarrow\" na "\Longrightarrow")
 
(Nie pokazano 15 wersji utworzonych przez 3 użytkowników)
Linia 1: Linia 1:
  
 +
== Zawartość ==
  
== Ćwiczenia 3: Dodawanie binarne (małe kroki) ==
+
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>).
  
  
== Zadania z rozwiązaniami ==
+
== Rozszerzenia semantyki języka Tiny ==
  
  
==== Zadanie 1 ====
+
{{cwiczenie|1|cw1|
  
Rozważmy następujący język wyrażeń (liczby binarne z dodawaniem):
+
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>
 
<math>
e \, ::= \,\,
+
\frac{I_1, s \,\longrightarrow\, \mathtt{Blad}}
      \epsilon  \,\,|\,\,
+
    {I_1;\, I_2, s \,\longrightarrow\, \mathtt{Blad}}
      e 0  \,\,|\,\,
 
      e 1  \,\,|\,\,
 
      e_1 + e_2
 
 
</math>
 
</math>
  
<math> \epsilon </math> oznacza słowo puste, czyli np. <math> \epsilon 1 0 1 </math>
+
<math>
oznacza binarną liczbę 101.
+
\frac{b, s \,\longrightarrow\, \mathbf{true} \quad \quad I_1, s \,\longrightarrow\, \mathtt{Blad}}
Napisz semantykę operacyjną obliczającą wartość wyrażeń.
+
    {\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>
  
==== Rozwiązanie ====
+
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.
  
Składnia wyrażeń pozwala na wygodny dostęp do najmniej znaczącego
+
</div></div>
bitu liczby. Spróbujmy zatem zastosować metodę dodawania
+
 
pisemnego:
+
 
 +
 
 +
{{cwiczenie|3|cw3|
 +
 
 +
Rozszerzmy język TINY o następującą instrukcję pętli:
  
 
<math>
 
<math>
e_1 0 + e_2 0 \,\Longrightarrow\, (e_1 + e_2) 0
+
I \, ::= \,\,
 +
      \mathbf{loop}\, I \,\,|\,\,
 +
      \mathbf{exit} \,\,|\,\,
 +
      \mathbf{continue}
 
</math>
 
</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>
 
<math>
e_1 0 + e_2 1 \,\Longrightarrow\, (e_1 + e_2) 1
+
\mathbf{exit}, s \,\longrightarrow\, s, \mbox{było-}\mathbf{exit}
 +
\quad \quad
 +
\mathbf{continue}, s \,\longrightarrow\, s, \mbox{było-}\mathbf{continue}.
 
</math>
 
</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>
 
<math>
e_1 1 + e_2 0 \,\Longrightarrow\, (e_1 + e_2) 1
+
\mathbf{State} \times \{ \mbox{było-}\mathbf{exit}, \mbox{było-}\mathbf{continue} \}.
 
</math>
 
</math>
  
Ale co zrobić z przeniesieniem?
+
'''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>
 
<math>
e_1 1 + e_2 1 \,\Longrightarrow\, ?
+
\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>
 
</math>
  
Podstawowy pomysł to potraktować przeniesienie jak dodatkowy składnik:
+
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>
 
<math>
e_1 1 + e_2 1 \,\Longrightarrow\, ((e_1 + e_2) + 1) 0
+
\frac{I, s \,\longrightarrow\, s' \quad \quad \mathbf{loop}\, I, s' \,\longrightarrow\, s''}
 +
    {\mathbf{loop}\, I, s \,\longrightarrow\, s''}
 
</math>
 
</math>
  
Zauważmy, że w składni dopuszcza się dowolne przeplatanie operatora dodawania
+
'''Pytanie:''' czy potrzebujemy dodatkowo reguł postaci:
i bitów <math> 0, 1 </math>. Tę dowolność wykorzystaliśmy właśnie w regułach
 
powyżej. Gdyby nasz język ograniczyć tylko do składni
 
  
 
<math>
 
<math>
e \, ::= \,\,
+
\frac{I, s \,\longrightarrow\, s' \quad \quad \mathbf{loop}\, I, s' \,\longrightarrow\, s'', \mbox{było-}\mathbf{exit}}
      b  \,\,|\,\,
+
    {\mathbf{loop}\, I, s \,\longrightarrow\, s'', \mbox{było-}\mathbf{exit}}
      e_1 + e_2
+
\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>
 
</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>
 
<math>
b \, ::= \,\,
+
\frac{I_1, s \,\longrightarrow\, s', \mbox{było-}\mathbf{exit}}
      \epsilon  \,\,|\,\,
+
    {I_1;\, I_2, s \,\longrightarrow\, s', \mbox{było-}\mathbf{exit}}
      b 0  \,\,|\,\,
+
\quad \quad
      b 1
+
\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>
 
</math>
  
(nazwijmy ją ''składnią ograniczoną'') to powyższe reguły byłyby niepoprawne.
+
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>.
 +
 
  
Zanim dopiszemy pozostałe reguły, określmy zbiór konfiguracji jako
 
zbiór wyrażeń. Konfiguracje końcowe to wyrażenia bez operatora dodawania
 
(liczby binarne). Nasz pomysł jest taki, że tranzycje stopniowo przesuwają
 
operator dodawania w lewo, aż się go ostatecznie ''pozbędą''.
 
  
 +
{{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>
  
==== Zadanie 2 ====
+
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ń 14:16, 9 cze 2020

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:

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:

to instrukcja pętli, 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 :

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

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 . 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. .


Ćwiczenie 3

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

Obliczenie wyrażenia polega na wykonaniu a potem na obliczeniu . Wartość wyrażenia jest taka, jak wartość wyrażenia a efektem ubocznym jest podstawienie tej wartości na zmienną .