Semantyka i weryfikacja programów/Ćwiczenia 1

Ćwiczenia 1: Semantyka operacyjna wyrażeń

Zadanie:

Semantyka języka Tiny z wykładu używała funkcji semantycznych $B,E:State\to 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\Vert false\Vert e_{1}e₁\le e₂\Vert \mathrm{\neg }b\Vert b₁\wedge b₂\Vert b₁\vee b₂$

$e::=0\Vert 1\Vert \dots \Vert x\Vert e₁+e₂\Vert e₁*e₂\Vert e₁-e₂$

Zacznijmy od dużych kroków.

Semantyka naturalna

Chcemy, aby tranzycje wyrażen wyglądały następująco: Parser nie mógł rozpoznać (nieznana funkcja „\dkrok”): {\displaystyle e, s \dkrok n b, s \dkrok l } gdzie s \in State, n jest liczbą całkowitą, n \in Int, a l \in Bool = \{ true, false \}. 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). 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 $\mathrm{\Gamma }$ następująco: $\mathrm{\Gamma }=(Instr\times Stan)\cup (Expr\times Stan)\cup (BExpr\times Stan)\cup Stan\cup Int\cup 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. Stan = Var \to Int. Konfiguracje końcowe pozostają bez zmian (Stan). 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:

Parser nie mógł rozpoznać (nieznana funkcja „\regula”): {\displaystyle \regula{b, s \dkrok true I; while b do I, s \dkrok s'} {while b do I, s \dkrok s'} }

Parser nie mógł rozpoznać (nieznana funkcja „\regula”): {\displaystyle \regula{b, s \dkrok false}{while b do I, s \dkrok s} }

Podobnie dla instrukcji warunkowej. Teraz zajmiemy się tranzycjami dla wyrażeń. Zacznijmy od stalych arytmetycznych: Parser nie mógł rozpoznać (nieznana funkcja „\dkrok”): {\displaystyle n, s \dkrok n, dla n \in 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: Parser nie mógł rozpoznać (nieznana funkcja „\dkrok”): {\displaystyle true, s \dkrok true false, s \dkrok false } Czynimy tu analogiczne założenie, że Bool jest podbiorem wyrażen boolowskich.

Operatory arytmetyczne definiujemy następująco: Parser nie mógł rozpoznać (nieznana funkcja „\regula”): {\displaystyle \regula{e₁, s \dkrok n₁ e₂, s \dkrok n₂ n = n₁ + n₂ } {e₁ + e₂,s \dkrok n} } Czyli aby obliczyć sumę e₁ + e₂ w stanie s, trzeba najpierw obliczyć e₁ i e₂ w stanie s, a następnie dodać obliczone wartości. Zauważmy, że nie specyfikujemy kolejności, w jakiej mają się obliczać e₁ i e₂. 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:

Parser nie mógł rozpoznać (nieznana funkcja „\regula”): {\displaystyle \regula{b₁, s \dkrok l₁ b₂, s \dkrok l₂ l = l₁ \land l₂} {b₁ \land b₂, s \dkrok l} } Oczywiście jeśli b₁ oblicza się do false, wartość całego wyrażenia jest false niezależnie od wartości wyrażenia b₂.

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

Parser nie mógł rozpoznać (nieznana funkcja „\regula”): {\displaystyle \regula{b₁, s \dkrok false} {b₁ \land b₂,s \dkrok false} \regula{b₁, s \dkrok true b₂, s \dkrok l} {b₁ + b₂,s \dkrok l} }

Wybraliśmy następującą kolejność obliczania wyrażeń: najpierw b₁, potem b₂. 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): Parser nie mógł rozpoznać (nieznana funkcja „\regula”): {\displaystyle \regula{b₁, s \dkrok false} {b₁ \land b₂,s \dkrok false} \regula{b₂, s \dkrok false} {b₁ \land b₂,s \dkrok 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: Parser nie mógł rozpoznać (nieznana funkcja „\regula”): {\displaystyle \regula{b₁, s \dkrok true b₂, s \dkrok true} {b₁ \land b₂,s \dkrok true} } Zauważmy, że powyższych reguł nie da sie zaimplementować sekwencyjnie: nie wiadomo czy najpierw obliczać b₁ czy b₂. Reguły te odpowiadają raczej strategii ,,równoległej: obliczaj ,,jednocześnie b₁ i b₂ 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: Parser nie mógł rozpoznać (nieznana funkcja „\dkro”): {\displaystyle e, s \dkro e', s } i podobnie dla wyrażeń boolowskich: Parser nie mógł rozpoznać (nieznana funkcja „\dkrok”): {\displaystyle b, s \dkrok 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.

Parser nie mógł rozpoznać (nieznana funkcja „\mkrok”): {\displaystyle true, s \mkrok true false, s \mkrok false }

Przejdźmy do spójników logicznych, powiedzmy b₁ \land b₂. 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:

Parser nie mógł rozpoznać (nieznana funkcja „\regu”): {\displaystyle \reguła{b₁, s \mkrok b'₁, s} {b₁ \land b₂, s \mkrok b'₁ \land b₂, s} \reguła{b₂, s \mkrok b'₂, s} {l₁ \land b₂, s \mkrok l₁ \land b₂, s} l₁ \land l₂ \mkrok l, jeśli l = l₁ \land l₂ }

Podobnie jak poprzednio, możemy zaniechać obliczania b₂ jeśli b₁ oblicza się do false.

Parser nie mógł rozpoznać (nieznana funkcja „\regu”): {\displaystyle \reguła{b₁, s \mkrok b'₁, s} {b₁ \land b₂, s \mkrok b'₁ \land b₂, s} false \land b₂, s \mkrok false true \land b₂, s \mkrok b₂,s }

Analogicznie reguły prawostronne to:

Parser nie mógł rozpoznać (nieznana funkcja „\regu”): {\displaystyle \reguła{b₂, s \mkrok b'₂, s} {b₁ \land b₂, s \mkrok b₁ \land b'₂, s} b₁ \land false, s \mkrok false b₁ \land true, s \mkrok b₁, s }

Reguły równoległe otrzymujemy jako sumę reguł lewo- i prawostronnych (w sumie 6 reguł).

Oto reguła dla negacji: Parser nie mógł rozpoznać (nieznana funkcja „\mkrok”): {\displaystyle \neg true, s \mkrok false, s \neg false, s \mkrok true, s }

Reguły dla e₁ \leq e₂ są następujące:

Parser nie mógł rozpoznać (nieznana funkcja „\regula”): {\displaystyle \regula{e₁, s \mkrok e'₁, s} {e₁ \leq e₂, s \mkrok e'₁ \leq e₂, s} \regula{e₂, s \mkrok e'₂, s} {e₁ \leq e₂, s \mkrok e₁ \leq e'₂, s} n₁ \leq n₂, s \mkrok true, s o ile n₁ \leq n₂ n₁ \leq n₂, s \mkrok false, s o ile n₁ > n₂ }

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₁ i e₂.

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

Parser nie mógł rozpoznać (nieznana funkcja „\regula”): {\displaystyle \regula{b, s \mkrok b', s} {if b then I₁ else I₂, s \mkrok if b' then I₁ else I₂, s} \regula{b, s \mkrok b', s} {while b do I, s \mkrok while b' do I, s} <math> a gdy dozór jest już obliczony, podejmujemy decyzję. W przypadku instrukcji warunkowej reguły są oczywiste: <math> if true then I₁ else I₂, s \mkrok I₁, s if false then I₁ else I₂, s \mkrok I₂, s }

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

Parser nie mógł rozpoznać (nieznana funkcja „\mkrok”): {\displaystyle while true do I, s \mkrok I; while ? do 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ę więc do tranzycji dużych kroków:

Parser nie mógł rozpoznać (nieznana funkcja „\regula”): {\displaystyle \regula{b, s \dkrok true} {while b do I, s \mkrok I; while b do I, s} \regula{b, s \dkrok false} {while b do I, s \mkrok 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ą:

Parser nie mógł rozpoznać (nieznana funkcja „\regula”): {\displaystyle \regula{e₁, s \mkrok e'₁, s} {e₁ + e₂, s \mkrok e'₁ + e₂, s} \regula{e₂, s \mkrok e'₂, s} {n + e₂, s \mkrok n + e'₂, s} n₁ + n₂, s \mkrok n, s o ile n = n₁ + n₂ }

Zadanie:

Rozważ dodatkowo operację dzielenia: $e::=\dots \Vert e₁/e₂$ i rozszerz semantyki z poprzedniego zadania tak, by dzielenie przez zero kończyło program. Oprócz stanu wynikiem programu powinna byc informacja o błędzie.

Rozwiązanie:

....