Semantyka i weryfikacja programów/Ćwiczenia 1

Ćwiczenia 1: Semantyka operacyjna wyrażeń

Zadanie 1

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} | \dots$

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; 𝐰 𝐡 𝐢 𝐥 𝐞 b 𝐝 𝐨 I, s ⟶ s^{'}}{𝐰 𝐡 𝐢 𝐥 𝐞 b 𝐝 𝐨 I, s ⟶ s^{'}}$

$\frac{b, s ⟶ f a l s e}{𝐰 𝐡 𝐢 𝐥 𝐞 b 𝐝 𝐨 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 I n t$ 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$

Analogicznie, czynimy tu 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 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:

$\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 (nazwijmy je regułami lewo-stronnymi, ponieważ rozpoczynamy od lewego koniunktu):

$\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} \land 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 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 \in S t a t e$ . 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ę obliczać $b_{1}$ i $b_{2}$ . 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. Oto odpowiednio zmodyfikowane reguły:

$\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ł). Zauważmy, że obliczanie wyrażeń $b_{1}$ i $b_{2}$ odbywa się teraz w twz. przeplocie: Pojedynczy krok polega na wykonaniu jednego kroku obliczenia $b_{1}$ albo jednego kroku obliczenia $b_{2}$ . Zwróćmy też uwagę, że po raz pierwszy nasze tranzycje nie posiadają własności determinizmu: wyrażenie $b_{1} \land b_{2}$ może wyewoluować w pojedyńczym kroku albo do $b'_{1} \land b_{2}$ albo do $b_{1} \land 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:

$\neg t r u e, s ⟹ f a l s e, s \neg f a l s e, s ⟹ t r u e, s \frac{b, s ⟹ b^{'}, s}{\neg b, s ⟹ \neg b^{'}, 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 ile n_{1} \leq n_{2} n_{1} \leq n_{2}, s ⟹ f a l s e, s o ile 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}{𝐢 𝐟 b 𝐭 𝐡 𝐞 𝐧 I_{1} 𝐞 𝐥 𝐬 𝐞 I_{2}, s ⟹ 𝐢 𝐟 b^{'} 𝐭 𝐡 𝐞 𝐧 I_{1} 𝐞 𝐥 𝐬 𝐞 I_{2}, s} \frac{b, 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:

$𝐢 𝐟 t r u e 𝐭 𝐡 𝐞 𝐧 I_{1} 𝐞 𝐥 𝐬 𝐞 I_{2}, s ⟹ I_{1}, s 𝐢 𝐟 f a l s e 𝐭 𝐡 𝐞 𝐧 I_{1} 𝐞 𝐥 𝐬 𝐞 I_{2}, s ⟹ I_{2}, s$

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

$𝐰 𝐡 𝐢 𝐥 𝐞 t r u e 𝐝 𝐨 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:

$\frac{b, s ⟶ t r u e}{𝐰 𝐡 𝐢 𝐥 𝐞 b 𝐝 𝐨 I, s ⟹ I; 𝐰 𝐡 𝐢 𝐥 𝐞 b 𝐝 𝐨 I, s} \frac{b, s ⟶ f a l s e}{𝐰 𝐡 𝐢 𝐥 𝐞 b 𝐝 𝐨 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 ile n = n_{1} + n_{2}$

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

Zadanie 2

Rozważ dodatkowo operację dzielenia: $e : : = \dots | e_{1} / e_{2}$ 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ą $B l a d$ . Reguła opisująca powstanie błędu może wyglądać np. tak w semantyce naturalnej:

$\frac{e_{2}, s ⟶ 0}{e_{1} / e_{2}, s ⟶ B l a d}$

a tak w semantyce małych kroków:

$e_{1} / 0, s ⟹ B l a d$

Pomijamy tutaj reguły dla przypadku, gdy $e_{2}$ 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:

$e_{1} / 0, s ⟹ B l a d, s$

I zamiast pojedyńczej konfiguracji końcowej $B l a d$ , potrzebowalibyśmy oczywiście całego zbioru ${B l a d} \times S t a t e$ .

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:

$\frac{e_{1}, s ⟶ B l a d}{e_{1} \leq e_{2}, s ⟶ B l a d} \frac{e_{2}, s ⟶ B l a d}{e_{1} \leq e_{2}, s ⟶ B l a d}$

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

$\frac{b ⟶ B l a d}{𝐢 𝐟 b 𝐭 𝐡 𝐞 𝐧 I_{1} 𝐞 𝐥 𝐬 𝐞 I_{2}, s ⟶ B l a d} \frac{b ⟶ B l a d}{𝐰 𝐡 𝐢 𝐥 𝐞 b 𝐝 𝐨 I, s ⟶ B l a d}$

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

$\frac{I_{1}, s ⟶ B l a d}{I_{1}; I_{2}, s ⟶ B l a d} \frac{I_{1}, s ⟶ B l a d}{𝐢 𝐟 b 𝐭 𝐡 𝐞 𝐧 I_{1} 𝐞 𝐥 𝐬 𝐞 I_{2}, s ⟶ B l a d} \frac{I_{2}, s ⟶ B l a d}{𝐢 𝐟 b 𝐭 𝐡 𝐞 𝐧 I_{1} 𝐞 𝐥 𝐬 𝐞 I_{2}, s ⟶ B l a d} \frac{I, s ⟶ B l a d}{𝐰 𝐡 𝐢 𝐥 𝐞 b 𝐝 𝐨 I, s ⟶ B l a d}$

I tak dalej.

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

(Powyżej traktowaliśmy tranzycję $I, s ⟶ B l a d$ 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, $I, s ⟹ B l a d$ ?)

Semantyka i weryfikacja programów/Ćwiczenia 1

Spis treści

Ćwiczenia 1: Semantyka operacyjna wyrażeń

Zadanie 1

Rozwiązanie

Semantyka naturalna

Strukturalna semantyka operacyjna (małe kroki)

Zadanie 2

Rozwiązanie (szkic)

Menu nawigacyjne

Działania na stronie

Opcje strony

Narzędzia osobiste

Nawigacja

Szukaj

Narzędzia