Semantyka i weryfikacja programów/Ćwiczenia 1: 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:
== Ćwiczenia 1: Semantyka operacyjna wyrażeń ==
== Ćwiczenia 1: Semantyka operacyjna wyrażeń ==


Linia 31: Linia 33:
         e_1 + e_2  \,\,|\,\,
         e_1 + e_2  \,\,|\,\,
         e_1 * e_2  \,\,|\,\,
         e_1 * e_2  \,\,|\,\,
         e_1 - e_2  
         e_1 - e_2 \,\,|\,\,  \ldots
</math>
</math>


Linia 46: Linia 48:
b, s \longrightarrow l,
b, s \longrightarrow l,
</math>
</math>
gdzie  
gdzie  
<math>s \in State</math>,
<math>s \in State</math>, <math>n</math> jest liczbą całkowitą,  
<math>n</math> jest liczbą całkowitą,  
<math>n \in Int</math>, a <math>l \in Bool = \{ true, false \}</math>.
<math>n \in Int</math>, a <math>l \in Bool = \{ true, false \}</math>.
Tranzycja taka oznacza, że wyrażenie e w stanie s wylicza się do
Tranzycja taka oznacza, że wyrażenie <math>e</math> w stanie <math>s<math> wylicza się do
wartości n, oraz że wyrażenie logiczne b w stanie s wylicza się do l.
wartości <math>n</math>, oraz że wyrażenie logiczne <math>b</math> w
stanie <math>s</math> wylicza się do <math>l</math>.
Zauważmy, że zakładamy tu, iż obliczenie wyrażenia nie zmienia
Zauważmy, że zakładamy tu, iż obliczenie wyrażenia nie zmienia
stanu (nie ma efektów ubocznych).
stanu (nie ma efektów ubocznych).
Linia 73: Linia 76:
<math>
<math>
\frac{b, s \longrightarrow true  \quad \quad   
\frac{b, s \longrightarrow true  \quad \quad   
       I; \mbox{ while } b \mbox{ do } I, s \longrightarrow s'}
       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 false}{while b do I, s \longrightarrow s}
\frac{b, s \longrightarrow false}
{\mathbf{while}\, b\, \mathbf{do}\, I, s \longrightarrow s}
</math>
</math>


Linia 89: Linia 93:
</math>
</math>


Zauważmy, iż celowo nie odróżniamy liczby n \in Int od  
Zauważmy, iż celowo nie odróżniamy liczby <math>n \in Int</math> od  
stałej reprezentującej tę liczbę, która może pojawić się
stałej reprezentującej tę liczbę, która może pojawić się
w wyrażeniach zgodnie z przyjętą przez nas składnią.
w wyrażeniach zgodnie z przyjętą przez nas składnią.
Czyli zakładamy, że Int jest podzbiorem zbioru wyrażeń.  
Czyli zakładamy, że Int jest podzbiorem zbioru wyrażeń.  
W powyższej tranzycji, n po lewej stronie to stała reprezentująca
W powyższej tranzycji, <math>n</math> po lewej stronie to stała reprezentująca
liczbę, która widnieje po prawej stronie.
liczbę, która widnieje po prawej stronie.


Analogiczne tranzycje dla stałych boolowskich to:
Analogiczne tranzycje dla stałych boolowskich to:
<math>
<math>
true, s \longrightarrow true
true, s \longrightarrow true
 
\quad \quad \quad
false, s \longrightarrow false
false, s \longrightarrow false
</math>
</math>
Czynimy tu analogiczne założenie, że Bool jest podbiorem
 
Analogicznie, czynimy tu założenie, że Bool jest podbiorem
wyrażen boolowskich.
wyrażen boolowskich.


Operatory arytmetyczne definiujemy następująco:
Operatory arytmetyczne definiujemy następująco:
<math>
<math>
\frac{e_1, s \longrightarrow n_1    
\frac{e_1, s \longrightarrow n_1   \quad \quad 
         e_2, s \longrightarrow n_2
         e_2, s \longrightarrow n_2 \quad \quad
         n = n_1 + n_2    }
         n = n_1 + n_2    }
{e_1 + e_2,s \longrightarrow n}
{e_1 + e_2,s \longrightarrow n}
</math>
</math>
Czyli aby obliczyć sumę e_1 + e_2 w stanie s, trzeba
 
najpierw obliczyć e_1 i e_2 w stanie s,
Czyli aby obliczyć sumę <math>e_1 + e_2</math> w stanie  
a następnie dodać obliczone wartości.
<math>s</math>, trzeba najpierw obliczyć <math>e_1</math> i  
<math>e_2</math> w stanie <math>s</math>, a następnie dodać obliczone wartości.
Zauważmy, że nie specyfikujemy kolejności, w jakiej mają się
Zauważmy, że nie specyfikujemy kolejności, w jakiej mają się
obliczać e_1 i e_2.
obliczać <math>e_1</math> i <math>e_2</math>.
I choć tutaj nie ma to żadnego znaczenia, w przyszłości  
I choć tutaj nie ma to żadnego znaczenia, w przyszłości  
będzie inaczej, gdy jezyk będzie dopuszczał efekty uboczne wyrażeń.
będzie inaczej, gdy jezyk będzie umożliwiał efekty uboczne  
podzas obliczania wyrażeń.


Podobne reguły można napisać dla pozostałych operacji
Podobne reguły można napisać dla pozostałych operacji
Linia 124: Linia 133:


<math>
<math>
\frac{b_1, s \longrightarrow l_1   b_2, s
\frac{b_1, s \longrightarrow l_1 \quad \quad
\longrightarrow l_2   l = l_1 \land l_2}
      b_2, s \longrightarrow l_2 \quad \quad  l = l_1 \land l_2}
{b_1  \land  b_2, s \longrightarrow l}
{b_1  \land  b_2, s \longrightarrow l}
</math>
</math>
Oczywiście jeśli b_1 oblicza się do false, wartość
 
Oczywiście jeśli <math>b_1</math> oblicza się do false, wartość
całego wyrażenia jest false niezależnie od wartości wyrażenia
całego wyrażenia jest false niezależnie od wartości wyrażenia
b_2.
<math>b_2</math>.
 
Czyli jeśli zaczniemy od obliczenia <math>b_1</math> i wynikiem będzie
Czyli jeśli zaczniemy od obliczenia b_1 i wynikiem będzie
false, to nie ma wogóle potrzeby obliczania <math>b_2</math>.
false, to nie ma wogóle potrzeby obliczania b_2.
Oto odpowiednie reguły (nazwijmy je regułami lewo-stronnymi, ponieważ
Oto odpowiednie reguły (lewo-stronne):
rozpoczynamy od ''lewego'' koniunktu):


<math>
<math>
\frac{b_1, s \longrightarrow false}
\frac{b_1, s \longrightarrow false}
{b_1 \land b_2,s \longrightarrow false}
{b_1 \land b_2, s \longrightarrow false}


\frac{b_1, s \longrightarrow true    
\frac{b_1, s \longrightarrow true \quad \quad 
         b_2, s \longrightarrow l}
         b_2, s \longrightarrow l}
{b_1 + b_2,s \longrightarrow l}
{b_1 \land b_2,s \longrightarrow l}
</math>
</math>


Linia 151: Linia 161:


Rozważmy też następującą kombinację obydwu semantyk
Rozważmy też następującą kombinację obydwu semantyk
(reguły równoległe):
(reguły ''równoległe''):
 
<math>
<math>
\frac{b_1, s \longrightarrow false}
\frac{b_1, s \longrightarrow false}
{b_1 \land b_2,s \longrightarrow false}
{b_1 \land b_2,s \longrightarrow false}
 
\quad \quad \quad
\frac{b_2, s \longrightarrow false}
\frac{b_2, s \longrightarrow false}
{b_1 \land b_2,s \longrightarrow false}
{b_1 \land b_2,s \longrightarrow false}
</math>
</math>
Czyli jeśli którekolwiek z podwyrażeń daje wynik false,
Czyli jeśli którekolwiek z podwyrażeń daje wynik false,
to taki wynik zyskuje całe wyrażenie.
to taki wynik zyskuje całe wyrażenie.
Dodatkowo potrzebujemy jeszcze reguły:
Dodatkowo potrzebujemy jeszcze reguły:
<math>
<math>
\frac{b_1, s \longrightarrow true  
\frac{b_1, s \longrightarrow true \quad \quad
b_2, s \longrightarrow true}
b_2, s \longrightarrow true}
{b_1 \land b_2,s \longrightarrow true}
{b_1 \land b_2,s \longrightarrow true}
</math>
</math>
Zauważmy, że powyższych reguł nie da sie zaimplementować
Zauważmy, że powyższych reguł nie da sie zaimplementować
sekwencyjnie: nie wiadomo czy najpierw obliczać  
sekwencyjnie: nie wiadomo czy najpierw obliczać  
b_1 czy b_2.
<math>b_1</math> czy <math>b_2</math>.
Reguły te odpowiadają raczej strategii ,,równoległej'':
Reguły te odpowiadają raczej strategii ,,równoległej'':
obliczaj ,,jednocześnie'' b_1 i b_2
obliczaj ,,jednocześnie'' b_1 i b_2 do momentu, gdy
albo do pierwszego false, albo aż obydwa się zakończą
jedno z nich obliczy się do wynikiem false, albo aż obydwa się zakończą
z wynikiem true.
z wynikiem true.


W naszym prostym języku wszystkie czterech warianty  
W naszym prostym języku wszystkie cztery warianty  
są równoważne. Różnice pomiędzy nimi zobaczymy jednak już w
są równoważne. Różnice pomiędzy nimi zobaczymy jednak już w
następnym zadaniu, w którym pojawi się prosta
następnym zadaniu, w którym pojawi się prosta
Linia 183: Linia 197:
Reguły dla pozostałych spójników logicznych oraz dla
Reguły dla pozostałych spójników logicznych oraz dla
negacji pozostawiamy jako ćwiczenie.
negacji pozostawiamy jako ćwiczenie.
A teraz małe kroki.
A teraz małe kroki.


Linia 196: Linia 209:
b, s \longrightarrow b', s
b, s \longrightarrow b', s
</math>
</math>
gdzie s \in State.
gdzie <math>s \in State</math>.
Przyjmijmy na razie takie same konfiguracje i konfiguracje końcowe jak dla semantyki
Przyjmijmy na razie takie same konfiguracje i konfiguracje końcowe  
naturalnej.
jak dla semantyki naturalnej.


Zacznijmy od wyrażeń boolowskich.  
Zacznijmy od wyrażeń boolowskich.  
Linia 204: Linia 218:
<math>
<math>
true, s \Longrightarrow true
true, s \Longrightarrow true
 
\quad \quad
false, s \Longrightarrow false
false, s \Longrightarrow false
</math>
</math>


Przejdźmy do spójników logicznych, powiedzmy b_1 \land b_2.
Przejdźmy do spójników logicznych, powiedzmy <math>b_1 \land b_2</math>.
Ponieważ opisujemy teraz pojedyncze (małe) kroki składające się na
Ponieważ opisujemy teraz pojedyncze (małe) kroki składające się na
wykonanie programu, musimy podać w jakiej kolejności będą się
wykonanie programu, musimy podać w jakiej kolejności będą się
wykonywać. Zacznijmy od strategii lewostronnej:
obliczać <math>b_1</math> i <math>b_2</math>. Zacznijmy od strategii lewostronnej:


<math>
<math>
\frac{b_1, s \Longrightarrow b'_1, s}
\frac{b_1, s \Longrightarrow b'_1, s}
{b_1 \land b_2, s \Longrightarrow b'_1 \land b_2, s}
{b_1 \land b_2, s \Longrightarrow b'_1 \land b_2, s}
\quad
\quad \quad
\frac{b_2, s \Longrightarrow b'_2, s}
\frac{b_2, s \Longrightarrow b'_2, s}
{l_1 \land b_2, s \Longrightarrow l_1 \land b_2, s}
{l_1 \land b_2, s \Longrightarrow l_1 \land b_2, s}
\quad
\quad \quad
l_1 \land l_2 \Longrightarrow l,   
l_1 \land l_2 \Longrightarrow l,   
\mbox{ o ile } l = l_1 \land l_2  
\mbox{ o ile } l = l_1 \land l_2  
Linia 225: Linia 239:


Podobnie jak poprzednio, możemy zaniechać obliczania
Podobnie jak poprzednio, możemy zaniechać obliczania
b_2 jeśli b_1 oblicza się do false.
<math>b_2</math> jeśli <math>b_1</math> oblicza się do false.
Oto odpowiednio zmodyfikowane reguły:


<math>
<math>
\frac{b_1, s \Longrightarrow b'_1, s}
\frac{b_1, s \Longrightarrow b'_1, s}
{b_1 \land b_2, s \Longrightarrow b'_1 \land b_2, s}
{b_1 \land b_2, s \Longrightarrow b'_1 \land b_2, s}
 
\quad \quad
false \land b_2, s \Longrightarrow false
false \land b_2, s \Longrightarrow false
 
\quad \quad
true  \land b_2, s \Longrightarrow b_2,s  
true  \land b_2, s \Longrightarrow b_2, s  
</math>
</math>


Linia 241: Linia 256:
\frac{b_2, s \Longrightarrow b'_2, s}
\frac{b_2, s \Longrightarrow b'_2, s}
{b_1 \land b_2, s \Longrightarrow b_1 \land b'_2, s}
{b_1 \land b_2, s \Longrightarrow b_1 \land b'_2, s}
 
\quad \quad
b_1 \land false, s \Longrightarrow false
b_1 \land false, s \Longrightarrow false
 
\quad \quad
b_1 \land true, s \Longrightarrow b_1, s
b_1 \land true, s \Longrightarrow b_1, s
</math>
</math>


Reguły równoległe otrzymujemy jako sumę reguł lewo- i
Reguły ''równoległe'' otrzymujemy jako sumę reguł lewo- i
prawostronnych (w sumie 6 reguł).
prawostronnych (w sumie 6 reguł). Zauważmy, że obliczanie
wyrażeń <math>b_1</math> i <math>b_2</math> odbywa się teraz
w twz. ''przeplocie'': Pojedynczy krok polega na wykonaniu
jednego kroku obliczenia <math>b_1</math> albo jednego kroku
obliczenia <math>b_2</math>.
Zwróćmy też uwagę, że po raz pierwszy nasze tranzycje nie posiadają
własności ''determinizmu'': wyrażenie <math>b_1 \land b_2</math>
może wyewoluować w pojedyńczym kroku albo do
<math>b'_1 \land b_2</math> albo do <math>b_1 \land b'_2</math>.
Na szczęście, końcowy wynik, do jakiego oblicza się wyrażenie
jest zawsze taki sam, niezależnie od przeplotu.


Oto reguła dla negacji:
Oto reguła dla negacji:
<math>
<math>
\neg true, s \Longrightarrow false, s
\neg true, s \Longrightarrow false, s
 
\quad \quad \quad
\neg false, s \Longrightarrow true, s  
\neg false, s \Longrightarrow true, s  
\quad \quad \quad
\frac{b, s \Longrightarrow b', s}
    {\neg b, s \Longrightarrow \neg b', s}
</math>
</math>


Reguły dla e_1 \leq e_2 są następujące:
Reguły dla <math>e_1 \leq e_2</math> są następujące:


<math>
<math>
Linia 266: Linia 295:
{e_1 \leq e_2, s \Longrightarrow e_1 \leq e'_2, s}
{e_1 \leq e_2, s \Longrightarrow e_1 \leq e'_2, s}


n_1 \leq n_2, s \Longrightarrow true, s   o ile  
n_1 \leq n_2, s \Longrightarrow true, s   \quad \mbox{ o ile }
n_1 \leq n_2
n_1 \leq n_2


n_1 \leq n_2, s \Longrightarrow false, s   o ile  
n_1 \leq n_2, s \Longrightarrow false, s \quad  \mbox{ o ile }
n_1 > n_2
n_1 > n_2
</math>
</math>
Linia 282: Linia 311:
<math>
<math>
\frac{b, s \Longrightarrow b', s}
\frac{b, s \Longrightarrow b', s}
{if b then I_1 else I_2, s \Longrightarrow  
{\mathbf{if}\, b\, \mathbf{then}\, I_1\, \mathbf{else}\, I_2, s \Longrightarrow  
if b' then I_1 else I_2, s}
\mathbf{if}\, b'\, \mathbf{then}\, I_1\, \mathbf{else}\, I_2, s}
 
\quad \quad
\frac{b, s \Longrightarrow b', s}
\frac{b, s \Longrightarrow b', s}
{while b do I, s \Longrightarrow while b' do I, s}
{\mathbf{while}\, b\, \mathbf{do}\, I, s \Longrightarrow \mathbf{while}\, b'\, \mathbf{do}\, I, s}
</math>
</math>


Linia 293: Linia 322:


<math>
<math>
if true then I_1 else I_2, s \Longrightarrow
\mathbf{if}\, true\, \mathbf{then}\, I_1\, \mathbf{else}\, I_2, s \Longrightarrow I_1, s
I_1, s
\quad \quad \quad
 
\mathbf{if}\, false\, \mathbf{then}\, I_1\, \mathbf{else}\, I_2, s \Longrightarrow I_2, s
if false then I_1 else I_2, s \Longrightarrow
I_2, s
</math>
</math>


Linia 303: Linia 330:


<math>
<math>
while true do I, s \Longrightarrow I; while ? do I, s
\mathbf{while}\, true\, \mathbf{do}\, I, s \Longrightarrow  
I;\, \mathbf{while}\, ?\, \mathbf{do}\, I, s
</math>
</math>


ale nie wiemy już, jaki był dozór pętli (widzimy tylko wynik
ale nie wiemy już, jaki był dozór pętli (widzimy tylko wynik
obliczenia tego dozoru w stanie s, true).
obliczenia tego dozoru w stanie s, true).
Możemy odwołać się więc do tranzycji dużych kroków:
Możemy odwołać się do tranzycji dużych kroków:


<math>
<math>
\frac{b, s \longrightarrow true}
\frac{b, s \longrightarrow true}
{while b do I, s \Longrightarrow I; while b do I, s}
{\mathbf{while}\, b\, \mathbf{do}\' I, s \Longrightarrow  
 
I;\, \mathbf{while}\, b\, \mathbf{do}\, I, s}
\quad \quad \quad
\frac{b, s \longrightarrow false}
\frac{b, s \longrightarrow false}
{while b do I, s \Longrightarrow s}
{\mathbf{while}\, b\, \mathbf{do}\, I, s \Longrightarrow s}
</math>
</math>


Takie rozwiązanie nie jest zatem ,,czystą'' semantyką
Takie rozwiązanie nie jest zatem ''czystą'' semantyką
małych kroków.
małych kroków.
Istnieją inne możliwe rozwiązania, w stylu małych kroków,
Istnieją inne możliwe rozwiązania, w stylu małych kroków,
Linia 334: Linia 363:
{n + e_2, s \Longrightarrow n + e'_2, s}  
{n + e_2, s \Longrightarrow n + e'_2, s}  


n_1 + n_2, s \Longrightarrow n, s   o ile
n_1 + n_2, s \Longrightarrow n, s \quad \mbox{ o ile }
n = n_1 + n_2
n = n_1 + n_2
</math>
</math>


Niektóre konfiguracje nie były wogóle przez nas używane. Które?


==== Zadanie: ====
==== Zadanie: ====
Linia 345: Linia 375:
         e_1 / e_2  
         e_1 / e_2  
</math>
</math>
i rozszerz semantyki z poprzedniego zadania tak, by dzielenie przez
i rozszerz semantyki z poprzedniego zadania.
zero kończyło program.
Dzielenie przez zero jest błądem i  kończy natychmiast wykonanie
Oprócz stanu wynikiem programu powinna byc informacja
programu.
o błędzie.
Oprócz stanu wynikiem programu powinna byc informacja o błędzie,
jeśli błąd wystąpił.


==== Rozwiązanie: ====
==== 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, tak w semantyce naturalnej
jak i w semantyce małych kroków.
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>Blad</math>.
Reguła opisująca powstanie błędu może wyglądać np. tak
w semantyce naturalnej:
 
<math>
\frac{e_2, s \longrightarrow 0}
{e_1 / e_2, s \longrightarrow Blad}
</math>
 
a tak w semantyce małych kroków:
 
<math>
e_1 / 0, 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>Blad</math>, potrzebowalibyśmy
oczywiście całego zbioru <math>\{Blad\} \times 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.
Zacznijmy od sementyki naturalnej:
 
<math>
\frac{e_1, s \dkrok Blad}
{e_1 \leq e_2, s \dkrok Blad}
\quad \quad \quad
\frac{e_2, s \dkrok Blad}
{e_1 \leq e_2, s \dkrok Blad}
</math>
 
Następnie, błąd w wyrażeniu powinien wstrzymać normalne wykonanie
instrukcji:
 
<math>
\frac{b \dkrok Blad}
{\mathbf{if}\, b\, \mathbf{then}\, I_1\, \mathbf{else}\, I_2, s \dkrok Blad}
\quad \quad \quad
\frac{b \dkrok Blad}
{\mathbf{while}\, b\, \mathbf{do}\, I, s \dkrok Blad}
</math>
 
I wreszcie błąd powinien propagować się do kolejnych instrukcji:
 
<math>
\frac{I_1, s \dkrok Blad}
{I_1;\, I_2, s \dkrok Blad}
\quad \quad \quad
\frac{I_1, s \dkrok Blad}
{\mathbf{if}\, b\, \mathbf{then}\, I_1\, \mathbf{else}\, I_2, s \dkrok Blad}
\quad \quad \quad
\frac{I_2, s \dkrok Blad}
{\mathbf{if}\, b\, \mathbf{then}\, I_1\, \mathbf{else}\, I_2, s \dkrok Blad}
\quad \quad \quad
\frac{I, s \dkrok Blad}
{\mathbf{while}\, b\, \mathbf{do}\, I, s \dkrok Blad}
</math>
 
I tak dalej.
 
Pytanie dla Czytelnika: jak napisać tę semantykę w podejściu mało-krokowym?


....
(Powyżej traktowaliśmy tranzycję
<math> I, s \dkrok Blad </math> jak ''duży krok''.
Ale tak naprawdę pojawienie się błędu powinno spowodować
''natychmiastowe'' zatrzymanie programu, więc może tranzycję taką
można również traktować jak ''mały krok'',
<math> I, s \mkrok Blad </math>?)

Wersja z 07:02, 24 lip 2006


Ćwiczenia 1: Semantyka operacyjna wyrażeń

Zadanie:

Semantyka języka Tiny z wykładu używała funkcji semantycznych B,E:State→State dla określenie znaczenia wyrażeń boolowskich i arytmetycznych. Zdefiniuj znaczenie wyrażeń za pomocą semantyki operacyjnej, w stylu dużych kroków (semantyka naturalna) i małych kroków.

Rozwiązanie:

Przypomnijmy składnię wyrażeń boolowskich i arytmetycznych:

b::=true|false|e1≤e2|¬b|b1∧b2|b1∨b2

e::=0|1|…|x|e1+e2|e1*e2|e1−e2|…


Zacznijmy od dużych kroków.

Semantyka naturalna

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

e,s⟶nb,s⟶l,

gdzie s∈State, n jest liczbą całkowitą, n∈Int, a l∈Bool={true,false}. Tranzycja taka oznacza, że wyrażenie e w stanie Parser nie mógł rozpoznać (błąd składni): {\displaystyle s<math> wylicza się do wartości <math>n} , oraz że wyrażenie logiczne b w stanie s wylicza się do l. Zauważmy, że zakładamy tu, iż obliczenie wyrażenia nie zmienia stanu (nie ma efektów ubocznych).

W tym celu rozszerzamy zbiór konfiguracji Γ następująco:

Γ=(Instr×State)∪(Expr×State)∪(BExpr×State)∪State∪Int∪Bool

gdzie Instr oznacza zbiór instrukcji (jedna z kategorii syntaktycznych języka Tiny), Expr zbiór wyrażeń arytmetycznych a BExpr zbiór wyrażeń boolowskich. State=Var→Int. Konfiguracje końcowe pozostają bez zmian (State). Tranzycje dla instrukcji pozostają zasadniczo bez zmian, z tym, że odwołania do funkcji semantycznych dla wyrazżen zastępujemy przez odpowiednie tranzycje. Np. dla instrukcji pętli będziemy mieć następujące reguły:

b,s⟶trueI;𝐰𝐡𝐢𝐥𝐞b𝐝𝐨I,s⟶s′𝐰𝐡𝐢𝐥𝐞b𝐝𝐨I,s⟶s′

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

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

n,s⟶n,dla n∈Int

Zauważmy, iż celowo nie odróżniamy liczby n∈Int od stałej reprezentującej tę liczbę, która może pojawić się w wyrażeniach zgodnie z przyjętą przez nas składnią. Czyli zakładamy, że Int jest podzbiorem zbioru wyrażeń. W powyższej tranzycji, n po lewej stronie to stała reprezentująca liczbę, która widnieje po prawej stronie.

Analogiczne tranzycje dla stałych boolowskich to:

true,s⟶truefalse,s⟶false

Analogicznie, czynimy tu założenie, że Bool jest podbiorem wyrażen boolowskich.

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 stanie s, a następnie dodać obliczone wartości. Zauważmy, że nie specyfikujemy kolejności, w jakiej mają się obliczać e1 i e2. I choć tutaj nie ma to żadnego znaczenia, w przyszłości będzie inaczej, gdy jezyk będzie umożliwiał efekty uboczne podzas 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

Oczywiście jeśli b1 oblicza się do false, wartość całego wyrażenia jest false niezależnie od wartości wyrażenia b2. Czyli jeśli zaczniemy od obliczenia b1 i wynikiem będzie false, to nie ma wogóle potrzeby obliczania b2. Oto odpowiednie reguły (nazwijmy je regułami lewo-stronnymi, ponieważ rozpoczynamy od lewego koniunktu):

b1,s⟶falseb1∧b2,s⟶falseb1,s⟶trueb2,s⟶lb1∧b2,s⟶l

Wybraliśmy następującą kolejność obliczania wyrażeń: najpierw b_1, potem b_2. Pozostawiamy Czytelnikowi napisanie analogicznych reguł dla kolejności odwrotnej (reguły prawo-stronne).

Rozważmy też następującą kombinację obydwu semantyk (reguły równoległe):

b1,s⟶falseb1∧b2,s⟶falseb2,s⟶falseb1∧b2,s⟶false

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

b1,s⟶trueb2,s⟶trueb1∧b2,s⟶true

Zauważmy, że powyższych reguł nie da sie zaimplementować sekwencyjnie: nie wiadomo czy najpierw obliczać b1 czy b2. Reguły te odpowiadają raczej strategii ,,równoległej: obliczaj ,,jednocześnie b_1 i b_2 do momentu, gdy jedno z nich obliczy się do wynikiem false, albo aż obydwa się zakończą z wynikiem true.

W naszym prostym języku wszystkie cztery warianty są równoważne. Różnice pomiędzy nimi zobaczymy jednak już w następnym zadaniu, w którym pojawi się prosta odmiana efektów ubocznych (błąd wykonania).


Reguły dla pozostałych spójników logicznych oraz dla negacji pozostawiamy jako ćwiczenie. A teraz małe kroki.

Strukturalna semantyka operacyjna (małe kroki)

Chcemy, aby tranzycje dla wyrażeń były postaci: e,s⟶e′,s i podobnie dla wyrażeń boolowskich: b,s⟶b′,s gdzie s∈State. Przyjmijmy na razie takie same konfiguracje i konfiguracje końcowe jak dla semantyki naturalnej.


Zacznijmy od wyrażeń boolowskich.

true,s⟹truefalse,s⟹false

Przejdźmy do spójników logicznych, powiedzmy b1∧b2. Ponieważ opisujemy teraz pojedyncze (małe) kroki składające się na wykonanie programu, musimy podać w jakiej kolejności będą się obliczać b1 i b2. Zacznijmy od strategii lewostronnej:

b1,s⟹b'1,sb1∧b2,s⟹b'1∧b2,sb2,s⟹b'2,sl1∧b2,s⟹l1∧b2,sl1∧l2⟹l, o ile l=l1∧l2

Podobnie jak poprzednio, możemy zaniechać obliczania b2 jeśli b1 oblicza się do false. Oto odpowiednio zmodyfikowane reguły:

b1,s⟹b'1,sb1∧b2,s⟹b'1∧b2,sfalse∧b2,s⟹falsetrue∧b2,s⟹b2,s

Analogicznie reguły prawostronne to:

b2,s⟹b'2,sb1∧b2,s⟹b1∧b'2,sb1∧false,s⟹falseb1∧true,s⟹b1,s

Reguły równoległe otrzymujemy jako sumę reguł lewo- i prawostronnych (w sumie 6 reguł). Zauważmy, że obliczanie wyrażeń b1 i b2 odbywa się teraz w twz. przeplocie: Pojedynczy krok polega na wykonaniu jednego kroku obliczenia b1 albo jednego kroku obliczenia b2. Zwróćmy też uwagę, że po raz pierwszy nasze tranzycje nie posiadają własności determinizmu: wyrażenie b1∧b2 może wyewoluować w pojedyńczym kroku albo do b'1∧b2 albo do b1∧b'2. Na szczęście, końcowy wynik, do jakiego oblicza się wyrażenie jest zawsze taki sam, niezależnie od przeplotu.

Oto reguła dla negacji:

¬true,s⟹false,s¬false,s⟹true,sb,s⟹b′,s¬b,s⟹¬b′,s

Reguły dla e1≤e2 są następujące:

e1,s⟹e'1,se1≤e2,s⟹e'1≤e2,se2,s⟹e'2,se1≤e2,s⟹e1≤e'2,sn1≤n2,s⟹true,s o ile n1≤n2n1≤n2,s⟹false,s o ile n1>n2

Reguły powyższe zależą od semantyki wyrażen arytmetycznych. Zauważmy, że ponownie pozostawiliśmy dowolność jeśli chodzi o kolejność obliczania wyrażeń arytmetycznych e_1 i e_2.

Rozważmy teraz instrukcję warunkową i instrukcję pętli. Najpierw obliczamy wartość dozoru:

b,s⟹b′,s𝐢𝐟b𝐭𝐡𝐞𝐧I1𝐞𝐥𝐬𝐞I2,s⟹𝐢𝐟b′𝐭𝐡𝐞𝐧I1𝐞𝐥𝐬𝐞I2,sb,s⟹b′,s𝐰𝐡𝐢𝐥𝐞b𝐝𝐨I,s⟹𝐰𝐡𝐢𝐥𝐞b′𝐝𝐨I,s

a gdy dozór jest już obliczony, podejmujemy decyzję. W przypadku instrukcji warunkowej reguły są oczywiste:

𝐢𝐟true𝐭𝐡𝐞𝐧I1𝐞𝐥𝐬𝐞I2,s⟹I1,s𝐢𝐟false𝐭𝐡𝐞𝐧I1𝐞𝐥𝐬𝐞I2,s⟹I2,s

Gorzej jest w przypadku instukcji pętli. Reguła mogłaby wyglądać tak:

𝐰𝐡𝐢𝐥𝐞true𝐝𝐨I,s⟹I;𝐰𝐡𝐢𝐥𝐞?𝐝𝐨I,s

ale nie wiemy już, jaki był dozór pętli (widzimy tylko wynik obliczenia tego dozoru w stanie s, true). Możemy odwołać się do tranzycji dużych kroków:

Parser nie mógł rozpoznać (błąd składni): {\displaystyle \frac{b, s \longrightarrow true} {\mathbf{while}\, b\, \mathbf{do}\' I, s \Longrightarrow I;\, \mathbf{while}\, b\, \mathbf{do}\, I, s} \quad \quad \quad \frac{b, s \longrightarrow false} {\mathbf{while}\, b\, \mathbf{do}\, I, s \Longrightarrow s} }

Takie rozwiązanie nie jest zatem czystą semantyką małych kroków. Istnieją inne możliwe rozwiązania, w stylu małych kroków, których znalezienie pozostawiamy dociekliwemu czytelnikowi.

Na koniec podajemy reguły dla operacji arytmetycznych, na przykładzie dodawania. Przyjmijmy, dla przykładu, strategię lewostronną:

e1,s⟹e'1,se1+e2,s⟹e'1+e2,se2,s⟹e'2,sn+e2,s⟹n+e'2,sn1+n2,s⟹n,s o ile n=n1+n2

Niektóre konfiguracje nie były wogóle przez nas używane. Które?

Zadanie:

Rozważ dodatkowo operację dzielenia: e::=…|e1/e2 i rozszerz semantyki 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, tak w semantyce naturalnej jak i w semantyce małych kroków. 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 w semantyce naturalnej:

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

a tak w semantyce małych kroków:

e1/0,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}×State.

Przejdźmy teraz do drugiego punktu. Potrzebujemy dodatkowych reguł, które zagwarantują, że błąd, raz pojawiwszy się, propaguje się przez wszystkie konstrukcje składniowe, a normalne obliczenie wyrażenia jest wstrzymame. Zacznijmy od sementyki naturalnej:

Parser nie mógł rozpoznać (nieznana funkcja „\dkrok”): {\displaystyle \frac{e_1, s \dkrok Blad} {e_1 \leq e_2, s \dkrok Blad} \quad \quad \quad \frac{e_2, s \dkrok Blad} {e_1 \leq e_2, s \dkrok Blad} }

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

Parser nie mógł rozpoznać (nieznana funkcja „\dkrok”): {\displaystyle \frac{b \dkrok Blad} {\mathbf{if}\, b\, \mathbf{then}\, I_1\, \mathbf{else}\, I_2, s \dkrok Blad} \quad \quad \quad \frac{b \dkrok Blad} {\mathbf{while}\, b\, \mathbf{do}\, I, s \dkrok Blad} }

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

Parser nie mógł rozpoznać (nieznana funkcja „\dkrok”): {\displaystyle \frac{I_1, s \dkrok Blad} {I_1;\, I_2, s \dkrok Blad} \quad \quad \quad \frac{I_1, s \dkrok Blad} {\mathbf{if}\, b\, \mathbf{then}\, I_1\, \mathbf{else}\, I_2, s \dkrok Blad} \quad \quad \quad \frac{I_2, s \dkrok Blad} {\mathbf{if}\, b\, \mathbf{then}\, I_1\, \mathbf{else}\, I_2, s \dkrok Blad} \quad \quad \quad \frac{I, s \dkrok Blad} {\mathbf{while}\, b\, \mathbf{do}\, I, s \dkrok Blad} }

I tak dalej.

Pytanie dla Czytelnika: jak napisać tę semantykę w podejściu mało-krokowym?

(Powyżej traktowaliśmy tranzycję Parser nie mógł rozpoznać (nieznana funkcja „\dkrok”): {\displaystyle I, s \dkrok Blad } jak duży krok. Ale tak naprawdę pojawienie się błędu powinno spowodować natychmiastowe zatrzymanie programu, więc może tranzycję taką można również traktować jak mały krok, Parser nie mógł rozpoznać (nieznana funkcja „\mkrok”): {\displaystyle I, s \mkrok Blad } ?)

Źródło: „https://wazniak.mimuw.edu.pl/index.php?title=Semantyka_i_weryfikacja_programów/Ćwiczenia_1&oldid=5733”