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

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
następna edycja →
WizualnieWikikod
Sl (dyskusja | edycje)
101 edycji
Nie podano opisu zmian
 
Sl (dyskusja | edycje)
101 edycji
cw 1 pierwsza przymiarka
Linia 1: Linia 1:
== Ćwiczenia 1: Semantyka operacyjna wyrażeń ==
== Ćwiczenia 1: Semantyka operacyjna wyrażeń ==


Linia 16: Linia 17:


<math>
<math>
b ::=  true  \|
b \, ::= \,\,  
         false  \|
        true  \,\,|\,\,
         e_1 e<sub>1</sub> \leq e<sub>2</sub> \|
         false  \,\,|\,\,
         \neg b  \|
         e_1 \leq e_2 \,\,|\,\,
         b<sub>1</sub> \land  b<sub>2</sub>   \|
         \neg b  \,\,|\,\,
         b<sub>1</sub> \lor  b<sub>2</sub>
         b_1 \land  b_2   \,\,|\,\,
         b_1 \lor  b_2
</math>
</math>


<math>
<math>
e  ::=  0  \|  1    \|  \ldots  \|
e \, ::= \,\,  
         x  \|
        0  \,\,|\,\,   1    \,\,|\,\,   \ldots  \,\,|\,\,
         e<sub>1</sub> + e<sub>2</sub> \|
         x  \,\,|\,\,
         e<sub>1</sub> * e<sub>2</sub> \|
         e_1 + e_2 \,\,|\,\,
         e<sub>1</sub> - e<sub>2</sub>
         e_1 * e_2 \,\,|\,\,
         e_1 - e_2
</math>
</math>


Linia 38: Linia 41:


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 \dkrok n   
e, s \longrightarrow n   
 
\quad \quad \quad
b, s \dkrok l
b, s \longrightarrow l,
</math>
</math>
gdzie s \in State,
gdzie  
n jest liczbą całkowitą, n \in Int, a l \in Bool = \{ true, false \}.
<math>s \in State</math>,
<math>n</math> jest liczbą całkowitą,  
<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 e w stanie s wylicza się do
wartości n (wyrażenie logiczne b w stanie s wylicza się do l).
wartości 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
Zauważmy, że zakładamy tu, iż obliczenie wyrażenia nie zmienia
stanu (nie ma efektów ubocznych).
stanu (nie ma efektów ubocznych).


W tym celu rozszerzamy zbiór konfiguracji <math>\Gamma</math> następująco:
W tym celu rozszerzamy zbiór konfiguracji <math>\Gamma</math> następująco:
<math>
<math>
\Gamma = (Instr \times Stan) \cup (Expr \times Stan) \cup (BExpr \times Stan) \cup Stan \cup Int \cup Bool
\Gamma = (Instr \times State) \cup (Expr \times State) \cup (BExpr \times State) \cup State \cup Int \cup Bool
</math>
</math>
gdzie Instr oznacza zbiór instrukcji (jedna z kategorii syntaktycznych
gdzie Instr oznacza zbiór instrukcji (jedna z kategorii syntaktycznych
języka Tiny), Expr zbiór wyrażeń arytmetycznych a BExpr
języka Tiny), Expr zbiór wyrażeń arytmetycznych a BExpr
zbiór wyrażeń boolowskich. Stan = Var \to Int.
zbiór wyrażeń boolowskich.  
Konfiguracje końcowe pozostają bez zmian (Stan).
<math>State = Var \to Int</math>.
Konfiguracje końcowe pozostają bez zmian (State).
Tranzycje dla instrukcji pozostają zasadniczo bez zmian, z tym,
Tranzycje dla instrukcji pozostają zasadniczo bez zmian, z tym,
że odwołania do funkcji semantycznych dla wyrazżen zastępujemy
że odwołania do funkcji semantycznych dla wyrazżen zastępujemy
Linia 64: Linia 73:


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


<math>
<math>
\regula{b, s \dkrok false}{while b do I, s \dkrok s}
\frac{b, s \longrightarrow false}{while b do I, s \longrightarrow s}
</math>
</math>


Linia 75: Linia 85:
Teraz zajmiemy się tranzycjami dla wyrażeń.
Teraz zajmiemy się tranzycjami dla wyrażeń.
Zacznijmy od stalych arytmetycznych:
Zacznijmy od stalych arytmetycznych:
<math>
<math>
n, s \dkrok n,  dla n \in Int
n, s \longrightarrow n, \quad \quad   \mbox{dla } n \in Int
</math>
</math>
Zauważmy, iż celowo nie odróżniamy liczby n \in Int od  
Zauważmy, iż celowo nie odróżniamy liczby n \in Int 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ę
Linia 87: Linia 99:
Analogiczne tranzycje dla stałych boolowskich to:
Analogiczne tranzycje dla stałych boolowskich to:
<math>
<math>
true, s \dkrok true
true, s \longrightarrow true


false, s \dkrok false
false, s \longrightarrow false
</math>
</math>
Czynimy tu analogiczne założenie, że Bool jest podbiorem
Czynimy tu analogiczne założenie, że Bool jest podbiorem
Linia 96: Linia 108:
Operatory arytmetyczne definiujemy następująco:
Operatory arytmetyczne definiujemy następująco:
<math>
<math>
\regula{e<sub>1</sub>, s \dkrok n<sub>1</sub>      
\frac{e_1, s \longrightarrow n_1      
         e<sub>2</sub>, s \dkrok n<sub>2</sub>
         e_2, s \longrightarrow n_2
         n = n<sub>1</sub> + n<sub>2</sub>   }
         n = n_1 + n_2   }
{e<sub>1</sub> + e<sub>2</sub>,s \dkrok n}
{e_1 + e_2,s \longrightarrow n}
</math>
</math>
Czyli aby obliczyć sumę e<sub>1</sub> + e<sub>2</sub> w stanie s, trzeba
Czyli aby obliczyć sumę e_1 + e_2 w stanie s, trzeba
najpierw obliczyć e<sub>1</sub> i e<sub>2</sub> w stanie s,
najpierw obliczyć e_1 i e_2 w stanie s,
a następnie dodać obliczone wartości.
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<sub>1</sub> i e<sub>2</sub>.
obliczać e_1 i e_2.
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 dopuszczał efekty uboczne wyrażeń.
Linia 113: Linia 125:


<math>
<math>
\regula{b<sub>1</sub>, s \dkrok l<sub>1</sub>   b<sub>2</sub>, s
\frac{b_1, s \longrightarrow l_1   b_2, s
\dkrok l<sub>2</sub>   l = l<sub>1</sub> \land l<sub>2</sub>}
\longrightarrow l_2   l = l_1 \land l_2}
{b<sub>1</sub> \land  b<sub>2</sub>, s \dkrok l}
{b_1 \land  b_2, s \longrightarrow l}
</math>
</math>
Oczywiście jeśli b<sub>1</sub> oblicza się do false, wartość
Oczywiście jeśli b_1 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<sub>2</sub>.
b_2.


Czyli jeśli zaczniemy od obliczenia b<sub>1</sub> i wynikiem będzie
Czyli jeśli zaczniemy od obliczenia b_1 i wynikiem będzie
false, to nie ma wogóle potrzeby obliczania b<sub>2</sub>.
false, to nie ma wogóle potrzeby obliczania b_2.
Oto odpowiednie reguły (lewo-stronne):
Oto odpowiednie reguły (lewo-stronne):


<math>
<math>
\regula{b<sub>1</sub>, s \dkrok false}
\frac{b_1, s \longrightarrow false}
{b<sub>1</sub> \land b<sub>2</sub>,s \dkrok false}
{b_1 \land b_2,s \longrightarrow false}


\regula{b<sub>1</sub>, s \dkrok true     
\frac{b_1, s \longrightarrow true     
         b<sub>2</sub>, s \dkrok l}
         b_2, s \longrightarrow l}
{b<sub>1</sub> + b<sub>2</sub>,s \dkrok l}
{b_1 + b_2,s \longrightarrow l}
</math>
</math>


Wybraliśmy następującą kolejność obliczania wyrażeń:
Wybraliśmy następującą kolejność obliczania wyrażeń:
najpierw b<sub>1</sub>, potem b<sub>2</sub>.
najpierw b_1, potem b_2.
Pozostawiamy Czytelnikowi napisanie analogicznych reguł dla
Pozostawiamy Czytelnikowi napisanie analogicznych reguł dla
kolejności odwrotnej (reguły prawo-stronne).
kolejności odwrotnej (reguły prawo-stronne).
Linia 142: Linia 154:
(reguły równoległe):
(reguły równoległe):
<math>
<math>
\regula{b<sub>1</sub>, s \dkrok false}
\frac{b_1, s \longrightarrow false}
{b<sub>1</sub> \land b<sub>2</sub>,s \dkrok false}
{b_1 \land b_2,s \longrightarrow false}


\regula{b<sub>2</sub>, s \dkrok false}
\frac{b_2, s \longrightarrow false}
{b<sub>1</sub> \land b<sub>2</sub>,s \dkrok 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,
Linia 152: Linia 164:
Dodatkowo potrzebujemy jeszcze reguły:
Dodatkowo potrzebujemy jeszcze reguły:
<math>
<math>
\regula{b<sub>1</sub>, s \dkrok true   
\frac{b_1, s \longrightarrow true   
b<sub>2</sub>, s \dkrok true}
b_2, s \longrightarrow true}
{b<sub>1</sub> \land b<sub>2</sub>,s \dkrok 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<sub>1</sub> czy b<sub>2</sub>.
b_1 czy b_2.
Reguły te odpowiadają raczej strategii ,,równoległej'':
Reguły te odpowiadają raczej strategii ,,równoległej'':
obliczaj ,,jednocześnie'' b<sub>1</sub> i b<sub>2</sub>
obliczaj ,,jednocześnie'' b_1 i b_2
albo do pierwszego false, albo aż obydwa się zakończą
albo do pierwszego false, albo aż obydwa się zakończą
z wynikiem true.
z wynikiem true.
Linia 179: Linia 191:
Chcemy, aby tranzycje dla wyrażeń były postaci:
Chcemy, aby tranzycje dla wyrażeń były postaci:
<math>
<math>
e, s \dkro e', s
e, s \longrightarrow e', s
</math>
</math>
i podobnie dla wyrażeń boolowskich:
i podobnie dla wyrażeń boolowskich:
<math>
<math>
b, s \dkrok b', s
b, s \longrightarrow b', s
</math>
</math>
gdzie s \in State.
gdzie s \in State.
Linia 192: Linia 204:


<math>
<math>
true, s \mkrok true
true, s \Longrightarrow true


false, s \mkrok false
false, s \Longrightarrow false
</math>
</math>


Przejdźmy do spójników logicznych, powiedzmy b<sub>1</sub> \land b<sub>2</sub>.
Przejdźmy do spójników logicznych, powiedzmy b_1 \land b_2.
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ę
Linia 203: Linia 215:


<math>
<math>
\reguła{b<sub>1</sub>, s \mkrok b'<sub>1</sub>, s}
\frac{b_1, s \Longrightarrow b'_1, s}
{b<sub>1</sub> \land b<sub>2</sub>, s \mkrok b'<sub>1</sub> \land b<sub>2</sub>, s}
{b_1 \land b_2, s \Longrightarrow b'_1 \land b_2, s}
 
\quad
\reguła{b<sub>2</sub>, s \mkrok b'<sub>2</sub>, s}
\frac{b_2, s \Longrightarrow b'_2, s}
{l<sub>1</sub> \land b<sub>2</sub>, s \mkrok l<sub>1</sub> \land b<sub>2</sub>, s}
{l_1 \land b_2, s \Longrightarrow l_1 \land b_2, s}
 
\quad
l<sub>1</sub> \land l<sub>2</sub> \mkrok l,   
l_1 \land l_2 \Longrightarrow l,   
jeśli l = l<sub>1</sub> \land l<sub>2</sub>
\mbox{ o ile } l = l_1 \land l_2
</math>
</math>


Podobnie jak poprzednio, możemy zaniechać obliczania
Podobnie jak poprzednio, możemy zaniechać obliczania
b<sub>2</sub> jeśli b<sub>1</sub> oblicza się do false.
b_2 jeśli b_1 oblicza się do false.


<math>
<math>
\reguła{b<sub>1</sub>, s \mkrok b'<sub>1</sub>, s}
\frac{b_1, s \Longrightarrow b'_1, s}
{b<sub>1</sub> \land b<sub>2</sub>, s \mkrok b'<sub>1</sub> \land b<sub>2</sub>, s}
{b_1 \land b_2, s \Longrightarrow b'_1 \land b_2, s}


false \land b<sub>2</sub>, s \mkrok false
false \land b_2, s \Longrightarrow false


true  \land b<sub>2</sub>, s \mkrok b<sub>2</sub>,s  
true  \land b_2, s \Longrightarrow b_2,s  
</math>
</math>


Linia 228: Linia 240:


<math>
<math>
\reguła{b<sub>2</sub>, s \mkrok b'<sub>2</sub>, s}
\frac{b_2, s \Longrightarrow b'_2, s}
{b<sub>1</sub> \land b<sub>2</sub>, s \mkrok b<sub>1</sub> \land b'<sub>2</sub>, s}
{b_1 \land b_2, s \Longrightarrow b_1 \land b'_2, s}


b<sub>1</sub> \land false, s \mkrok false
b_1 \land false, s \Longrightarrow false


b<sub>1</sub> \land true, s \mkrok b<sub>1</sub>, s
b_1 \land true, s \Longrightarrow b_1, s
</math>
</math>


Linia 241: Linia 253:
Oto reguła dla negacji:
Oto reguła dla negacji:
<math>
<math>
\neg true, s \mkrok false, s
\neg true, s \Longrightarrow false, s


\neg false, s \mkrok true, s  
\neg false, s \Longrightarrow true, s  
</math>
</math>


Reguły dla e<sub>1</sub> \leq e<sub>2</sub> są następujące:
Reguły dla e_1 \leq e_2 są następujące:


<math>
<math>
\regula{e<sub>1</sub>, s \mkrok e'<sub>1</sub>, s}
\frac{e_1, s \Longrightarrow e'_1, s}
{e<sub>1</sub> \leq e<sub>2</sub>, s \mkrok e'<sub>1</sub> \leq e<sub>2</sub>, s}
{e_1 \leq e_2, s \Longrightarrow e'_1 \leq e_2, s}


\regula{e<sub>2</sub>, s \mkrok e'<sub>2</sub>, s}
\frac{e_2, s \Longrightarrow e'_2, s}
{e<sub>1</sub> \leq e<sub>2</sub>, s \mkrok e<sub>1</sub> \leq e'<sub>2</sub>, s}
{e_1 \leq e_2, s \Longrightarrow e_1 \leq e'_2, s}


n<sub>1</sub> \leq n<sub>2</sub>, s \mkrok true, s    o ile  
n_1 \leq n_2, s \Longrightarrow true, s    o ile  
n<sub>1</sub> \leq n<sub>2</sub>
n_1 \leq n_2


n<sub>1</sub> \leq n<sub>2</sub>, s \mkrok false, s    o ile  
n_1 \leq n_2, s \Longrightarrow false, s    o ile  
n<sub>1</sub> > n<sub>2</sub>
n_1 > n_2
</math>
</math>


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


Rozważmy teraz instrukcję warunkową i instrukcję pętli.
Rozważmy teraz instrukcję warunkową i instrukcję pętli.
Linia 270: Linia 282:


<math>
<math>
\regula{b, s \mkrok b', s}
\frac{b, s \Longrightarrow b', s}
{if b then I<sub>1</sub> else I<sub>2</sub>, s \mkrok
{if b then I_1 else I_2, s \Longrightarrow
if b' then I<sub>1</sub> else I<sub>2</sub>, s}
if b' then I_1 else I_2, s}


\regula{b, s \mkrok b', s}
\frac{b, s \Longrightarrow b', s}
{while b do I, s \mkrok while b' do I, s}
{while b do I, s \Longrightarrow while b' do I, s}
<math>
</math>


a gdy dozór jest już obliczony, podejmujemy decyzję.
a gdy dozór jest już obliczony, podejmujemy decyzję.
Linia 282: Linia 294:


<math>
<math>
if true then I<sub>1</sub> else I<sub>2</sub>, s \mkrok
if true then I_1 else I_2, s \Longrightarrow
I<sub>1</sub>, s
I_1, s


if false then I<sub>1</sub> else I<sub>2</sub>, s \mkrok
if false then I_1 else I_2, s \Longrightarrow
I<sub>2</sub>, s
I_2, s
</math>
</math>


Linia 292: Linia 304:


<math>
<math>
while true do I, s \mkrok I; while ? do I, s
while true do I, s \Longrightarrow I; while ? do I, s
</math>
</math>


Linia 300: Linia 312:


<math>
<math>
\regula{b, s \dkrok true}
\frac{b, s \longrightarrow true}
{while b do I, s \mkrok I; while b do I, s}
{while b do I, s \Longrightarrow I; while b do I, s}


\regula{b, s \dkrok false}
\frac{b, s \longrightarrow false}
{while b do I, s \mkrok s}
{while b do I, s \Longrightarrow s}
</math>
</math>


Linia 317: Linia 329:


<math>
<math>
\regula{e<sub>1</sub>, s \mkrok e'<sub>1</sub>, s}
\frac{e_1, s \Longrightarrow e'_1, s}
{e<sub>1</sub> + e<sub>2</sub>, s \mkrok e'<sub>1</sub> + e<sub>2</sub>, s}  
{e_1 + e_2, s \Longrightarrow e'_1 + e_2, s}  


\regula{e<sub>2</sub>, s \mkrok e'<sub>2</sub>, s}
\frac{e_2, s \Longrightarrow e'_2, s}
{n + e<sub>2</sub>, s \mkrok n + e'<sub>2</sub>, s}  
{n + e_2, s \Longrightarrow n + e'_2, s}  


n<sub>1</sub> + n<sub>2</sub>, s \mkrok n, s  o ile
n_1 + n_2, s \Longrightarrow n, s  o ile
n = n<sub>1</sub> + n<sub>2</sub>
n = n_1 + n_2
</math>
</math>


Linia 331: Linia 343:
Rozważ dodatkowo operację dzielenia:
Rozważ dodatkowo operację dzielenia:
<math>
<math>
e ::=   \ldots  \|
e \, ::= \,\,  \ldots  \,\,|\,\,
         e<sub>1</sub> / e<sub>2</sub>
         e_1 / e_2
</math>
</math>
i rozszerz semantyki z poprzedniego zadania tak, by dzielenie przez
i rozszerz semantyki z poprzedniego zadania tak, by dzielenie przez
zero kończyło program.
zero kończyło program.
Oprócz stanu wynikiem programu powinna byc informacja
Zamiast stanu wynikiem programu powinna byc informacja
o błędzie.
o błędzie.


Wersja z 09:21, 15 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 s wylicza się do wartości 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; while b do I,s⟶s′𝐰𝐡𝐢𝐥𝐞b𝐝𝐨I,s⟶s′

b,s⟶falsewhilebdoI,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 \in 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 Czynimy tu analogiczne 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ę e_1 + e_2 w stanie s, trzeba najpierw obliczyć e_1 i e_2 w stanie s, a następnie dodać obliczone wartości. Zauważmy, że nie specyfikujemy kolejności, w jakiej mają się obliczać e_1 i e_2. I choć tutaj nie ma to żadnego znaczenia, w przyszłości będzie inaczej, gdy jezyk będzie dopuszczał efekty uboczne 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 b_1 oblicza się do false, wartość całego wyrażenia jest false niezależnie od wartości wyrażenia b_2.

Czyli jeśli zaczniemy od obliczenia b_1 i wynikiem będzie false, to nie ma wogóle potrzeby obliczania b_2. Oto odpowiednie reguły (lewo-stronne):

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ć b_1 czy b_2. Reguły te odpowiadają raczej strategii ,,równoległej: obliczaj ,,jednocześnie b_1 i b_2 albo do pierwszego false, albo aż obydwa się zakończą z wynikiem true.

W naszym prostym języku wszystkie czterech 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 \in 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 b_1 \land b_2. Ponieważ opisujemy teraz pojedyncze (małe) kroki składające się na wykonanie programu, musimy podać w jakiej kolejności będą się wykonywać. 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 b_2 jeśli b_1 oblicza się do false.

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

Oto reguła dla negacji: ¬true,s⟹false,s¬false,s⟹true,s

Reguły dla e_1 \leq e_2 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,soilen1≤n2n1≤n2,s⟹false,soilen1>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′,sifbthenI1elseI2,s⟹ifb′thenI1elseI2,sb,s⟹b′,swhilebdoI,s⟹whileb′doI,s

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

iftruethenI1elseI2,s⟹I1,siffalsethenI1elseI2,s⟹I2,s

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

whiletruedoI,s⟹I;while?doI,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ę więc do tranzycji dużych kroków:

b,s⟶truewhilebdoI,s⟹I;whilebdoI,sb,s⟶falsewhilebdoI,s⟹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,soilen=n1+n2


Zadanie:

Rozważ dodatkowo operację dzielenia: e::=…|e1/e2 i rozszerz semantyki z poprzedniego zadania tak, by dzielenie przez zero kończyło program. Zamiast stanu wynikiem programu powinna byc informacja o błędzie.

Rozwiązanie:

....

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