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 : S t a t e \to S t a t e$ 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 : : = t r u e | f a l s e | e_{1} \leq e_{2} | \neg b | b_{1} \land b_{2} | b_{1} \lor b_{2}$

$e : : = 0 | 1 | \dots | x | e_{1} + e_{2} | e_{1} * e_{2} | e_{1} - e_{2}$

Zacznijmy od dużych kroków.

Semantyka naturalna

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

$e, s ⟶ n b, s ⟶ l,$ gdzie $s \in S t a t e$ , $n$ jest liczbą całkowitą, $n \in I n t$ , a $l \in B o o l = {t r u e, f a l s e}$ . 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:

$Γ = (I n s t r \times S t a t e) \cup (E x p r \times S t a t e) \cup (B E x p r \times S t a t e) \cup S t a t e \cup I n t \cup B o o l$

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. $S t a t e = V a r \to I n t$ . 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:

$\frac{b, s ⟶ t r u e I; while b do I, s ⟶ s^{'}}{𝐰 𝐡 𝐢 𝐥 𝐞 b 𝐝 𝐨 I, s ⟶ s^{'}}$

$\frac{b, s ⟶ f a l s e}{w h i l e b d o I, s ⟶ s}$

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

$n, s ⟶ n, dla n \in I n t$

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: $t r u e, s ⟶ t r u e f a l s e, s ⟶ f a l s e$ Czynimy tu analogiczne założenie, że Bool jest podbiorem wyrażen boolowskich.

Operatory arytmetyczne definiujemy następująco: $\frac{e_{1}, s ⟶ n_{1} e_{2}, s ⟶ n_{2} n = n_{1} + n_{2}}{e_{1} + e_{2}, 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:

$\frac{b_{1}, s ⟶ l_{1} b_{2}, s ⟶ l_{2} l = l_{1} \land l_{2}}{b_{1} \land b_{2}, 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):

$\frac{b_{1}, s ⟶ f a l s e}{b_{1} \land b_{2}, s ⟶ f a l s e} \frac{b_{1}, s ⟶ t r u e b_{2}, s ⟶ l}{b_{1} + b_{2}, 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): $\frac{b_{1}, s ⟶ f a l s e}{b_{1} \land b_{2}, s ⟶ f a l s e} \frac{b_{2}, s ⟶ f a l s e}{b_{1} \land b_{2}, s ⟶ f a l s e}$ Czyli jeśli którekolwiek z podwyrażeń daje wynik false, to taki wynik zyskuje całe wyrażenie. Dodatkowo potrzebujemy jeszcze reguły: $\frac{b_{1}, s ⟶ t r u e b_{2}, s ⟶ t r u e}{b_{1} \land b_{2}, s ⟶ t r u e}$ 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.

$t r u e, s ⟹ t r u e f a l s e, s ⟹ f a l s e$

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:

$\frac{b_{1}, s ⟹ b'_{1}, s}{b_{1} \land b_{2}, s ⟹ b'_{1} \land b_{2}, s} \frac{b_{2}, s ⟹ b'_{2}, s}{l_{1} \land b_{2}, s ⟹ l_{1} \land b_{2}, s} l_{1} \land l_{2} ⟹ l, o ile l = l_{1} \land l_{2}$

Podobnie jak poprzednio, możemy zaniechać obliczania b_2 jeśli b_1 oblicza się do false.

$\frac{b_{1}, s ⟹ b'_{1}, s}{b_{1} \land b_{2}, s ⟹ b'_{1} \land b_{2}, s} f a l s e \land b_{2}, s ⟹ f a l s e t r u e \land b_{2}, s ⟹ b_{2}, s$

Analogicznie reguły prawostronne to:

$\frac{b_{2}, s ⟹ b'_{2}, s}{b_{1} \land b_{2}, s ⟹ b_{1} \land b'_{2}, s} b_{1} \land f a l s e, s ⟹ f a l s e b_{1} \land t r u e, s ⟹ b_{1}, s$

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

Oto reguła dla negacji: $\neg t r u e, s ⟹ f a l s e, s \neg f a l s e, s ⟹ t r u e, s$

Reguły dla e_1 \leq e_2 są następujące:

$\frac{e_{1}, s ⟹ e'_{1}, s}{e_{1} \leq e_{2}, s ⟹ e'_{1} \leq e_{2}, s} \frac{e_{2}, s ⟹ e'_{2}, s}{e_{1} \leq e_{2}, s ⟹ e_{1} \leq e'_{2}, s} n_{1} \leq n_{2}, s ⟹ t r u e, s o i l e n_{1} \leq n_{2} n_{1} \leq n_{2}, s ⟹ f a l s e, s o i l e n_{1} > n_{2}$

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:

$\frac{b, s ⟹ b^{'}, s}{i f b t h e n I_{1} e l s e I_{2}, s ⟹ i f b^{'} t h e n I_{1} e l s e I_{2}, s} \frac{b, s ⟹ b^{'}, s}{w h i l e b d o I, s ⟹ w h i l e b^{'} d o I, s}$

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

$i f t r u e t h e n I_{1} e l s e I_{2}, s ⟹ I_{1}, s i f f a l s e t h e n I_{1} e l s e I_{2}, s ⟹ I_{2}, s$

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

$w h i l e t r u e d o I, s ⟹ I; w h i l e ? d o 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:

$\frac{b, s ⟶ t r u e}{w h i l e b d o I, s ⟹ I; w h i l e b d o I, s} \frac{b, s ⟶ f a l s e}{w h i l e b d o I, 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ą:

$\frac{e_{1}, s ⟹ e'_{1}, s}{e_{1} + e_{2}, s ⟹ e'_{1} + e_{2}, s} \frac{e_{2}, s ⟹ e'_{2}, s}{n + e_{2}, s ⟹ n + e'_{2}, s} n_{1} + n_{2}, s ⟹ n, s o i l e n = n_{1} + n_{2}$

Zadanie:

Rozważ dodatkowo operację dzielenia: $e : : = \dots | e_{1} / e_{2}$ 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:

....

Semantyka i weryfikacja programów/Ćwiczenia 1

Spis treści

Ćwiczenia 1: Semantyka operacyjna wyrażeń

Zadanie:

Rozwiązanie:

Semantyka naturalna

Strukturalna semantyka operacyjna (małe kroki)

Zadanie:

Rozwiązanie:

Menu nawigacyjne

Działania na stronie

Opcje strony

Narzędzia osobiste

Nawigacja

Szukaj

Narzędzia