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: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|false|e_1\le e_2|\mathrm{\neg }b|b_1\wedge b_2|b_1\vee 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⟶nb,s⟶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$, 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 $\mathrm{\Gamma }$ następująco:

$\mathrm{\Gamma }=(Instr\times State)\cup (Expr\times State)\cup (BExpr\times State)\cup State\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. $State=Var\to 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:

$\frac{b,s⟶trueI;\mathbf{𝐰}\mathbf{𝐡}\mathbf{𝐢}\mathbf{𝐥}\mathbf{𝐞}b\mathbf{𝐝}\mathbf{𝐨}I,s⟶s^{\prime }}{\mathbf{𝐰}\mathbf{𝐡}\mathbf{𝐢}\mathbf{𝐥}\mathbf{𝐞}b\mathbf{𝐝}\mathbf{𝐨}I,s⟶s^{\prime }}$

$\frac{b,s⟶false}{\mathbf{𝐰}\mathbf{𝐡}\mathbf{𝐢}\mathbf{𝐥}\mathbf{𝐞}b\mathbf{𝐝}\mathbf{𝐨}I,s⟶s}$

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

$n,s⟶n,\text{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:

$true,s⟶truefalse,s⟶false$

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\wedge l_2}{b_1\wedge 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⟶false}{b_1\wedge b_2,s⟶false}\frac{b_1,s⟶true{b}_2,s⟶l}{b_1\wedge 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⟶false}{b_1\wedge b_2,s⟶false}\frac{b_2,s⟶false}{b_1\wedge b_2,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:

$\frac{b_1,s⟶true{b}_2,s⟶true}{b_1\wedge b_2,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 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^{\prime },s$ i podobnie dla wyrażeń boolowskich: $b,s⟶b^{\prime },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\wedge 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{\text{'}}_1,s}{b_1\wedge b_2,s⟹b{\text{'}}_1\wedge b_2,s}\frac{b_2,s⟹b{\text{'}}_2,s}{l_1\wedge b_2,s⟹l_1\wedge b_2,s}{l}_1\wedge l_2⟹l,\text{ o ile }l=l_1\wedge 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{\text{'}}_1,s}{b_1\wedge b_2,s⟹b{\text{'}}_1\wedge b_2,s}false\wedge b_2,s⟹falsetrue\wedge b_2,s⟹b_2,s$

Analogicznie reguły prawostronne to:

$\frac{b_2,s⟹b{\text{'}}_2,s}{b_1\wedge b_2,s⟹b_1\wedge b{\text{'}}_2,s}{b}_1\wedge false,s⟹false{b}_1\wedge true,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\wedge b_2$ może wyewoluować w pojedyńczym kroku albo do $b{\text{'}}_1\wedge b_2$ albo do $b_1\wedge b{\text{'}}_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:

$\mathrm{\neg }true,s⟹false,s\mathrm{\neg }false,s⟹true,s\frac{b,s⟹b^{\prime },s}{\mathrm{\neg }b,s⟹\mathrm{\neg }{b}^{\prime },s}$

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

$\frac{e_1,s⟹e{\text{'}}_1,s}{e_1\le e_2,s⟹e{\text{'}}_1\le e_2,s}\frac{e_2,s⟹e{\text{'}}_2,s}{e_1\le e_2,s⟹e_1\le e{\text{'}}_2,s}{n}_1\le n_2,s⟹true,s\text{ o ile }{n}_1\le n_2{n}_1\le n_2,s⟹false,s\text{ 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^{\prime },s}{\mathbf{𝐢}\mathbf{𝐟}b\mathbf{𝐭}\mathbf{𝐡}\mathbf{𝐞}\mathbf{𝐧}{I}_1\mathbf{𝐞}\mathbf{𝐥}\mathbf{𝐬}\mathbf{𝐞}{I}_2,s⟹\mathbf{𝐢}\mathbf{𝐟}{b}^{\prime }\mathbf{𝐭}\mathbf{𝐡}\mathbf{𝐞}\mathbf{𝐧}{I}_1\mathbf{𝐞}\mathbf{𝐥}\mathbf{𝐬}\mathbf{𝐞}{I}_2,s}\frac{b,s⟹b^{\prime },s}{\mathbf{𝐰}\mathbf{𝐡}\mathbf{𝐢}\mathbf{𝐥}\mathbf{𝐞}b\mathbf{𝐝}\mathbf{𝐨}I,s⟹\mathbf{𝐰}\mathbf{𝐡}\mathbf{𝐢}\mathbf{𝐥}\mathbf{𝐞}{b}^{\prime }\mathbf{𝐝}\mathbf{𝐨}I,s}$

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

$\mathbf{𝐢}\mathbf{𝐟}true\mathbf{𝐭}\mathbf{𝐡}\mathbf{𝐞}\mathbf{𝐧}{I}_1\mathbf{𝐞}\mathbf{𝐥}\mathbf{𝐬}\mathbf{𝐞}{I}_2,s⟹I_1,s\mathbf{𝐢}\mathbf{𝐟}false\mathbf{𝐭}\mathbf{𝐡}\mathbf{𝐞}\mathbf{𝐧}{I}_1\mathbf{𝐞}\mathbf{𝐥}\mathbf{𝐬}\mathbf{𝐞}{I}_2,s⟹I_2,s$

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

$\mathbf{𝐰}\mathbf{𝐡}\mathbf{𝐢}\mathbf{𝐥}\mathbf{𝐞}true\mathbf{𝐝}\mathbf{𝐨}I,s⟹I;\mathbf{𝐰}\mathbf{𝐡}\mathbf{𝐢}\mathbf{𝐥}\mathbf{𝐞}?\mathbf{𝐝}\mathbf{𝐨}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⟶true}{\mathbf{𝐰}\mathbf{𝐡}\mathbf{𝐢}\mathbf{𝐥}\mathbf{𝐞}b\mathbf{𝐝}\mathbf{𝐨}I,s⟹I;\mathbf{𝐰}\mathbf{𝐡}\mathbf{𝐢}\mathbf{𝐥}\mathbf{𝐞}b\mathbf{𝐝}\mathbf{𝐨}I,s}\frac{b,s⟶false}{\mathbf{𝐰}\mathbf{𝐡}\mathbf{𝐢}\mathbf{𝐥}\mathbf{𝐞}b\mathbf{𝐝}\mathbf{𝐨}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{\text{'}}_1,s}{e_1+e_2,s⟹e{\text{'}}_1+e_2,s}\frac{e_2,s⟹e{\text{'}}_2,s}{n+e_2,s⟹n+e{\text{'}}_2,s}{n}_1+n_2,s⟹n,s\text{ 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ą $Blad$. 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⟶Blad}$

a tak w semantyce małych kroków:

$e_1/0,s⟹Blad$

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⟹Blad,s$

I zamiast pojedyńczej konfiguracji końcowej $Blad$, potrzebowalibyśmy oczywiście całego zbioru $\{Blad\}\times 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:

$\frac{e_1,s⟶Blad}{e_1\le e_2,s⟶Blad}\frac{e_2,s⟶Blad}{e_1\le e_2,s⟶Blad}$

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

$\frac{b⟶Blad}{\mathbf{𝐢}\mathbf{𝐟}b\mathbf{𝐭}\mathbf{𝐡}\mathbf{𝐞}\mathbf{𝐧}{I}_1\mathbf{𝐞}\mathbf{𝐥}\mathbf{𝐬}\mathbf{𝐞}{I}_2,s⟶Blad}\frac{b⟶Blad}{\mathbf{𝐰}\mathbf{𝐡}\mathbf{𝐢}\mathbf{𝐥}\mathbf{𝐞}b\mathbf{𝐝}\mathbf{𝐨}I,s⟶Blad}$

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

$\frac{I_1,s⟶Blad}{I_1;I_2,s⟶Blad}\frac{I_1,s⟶Blad}{\mathbf{𝐢}\mathbf{𝐟}b\mathbf{𝐭}\mathbf{𝐡}\mathbf{𝐞}\mathbf{𝐧}{I}_1\mathbf{𝐞}\mathbf{𝐥}\mathbf{𝐬}\mathbf{𝐞}{I}_2,s⟶Blad}\frac{I_2,s⟶Blad}{\mathbf{𝐢}\mathbf{𝐟}b\mathbf{𝐭}\mathbf{𝐡}\mathbf{𝐞}\mathbf{𝐧}{I}_1\mathbf{𝐞}\mathbf{𝐥}\mathbf{𝐬}\mathbf{𝐞}{I}_2,s⟶Blad}\frac{I,s⟶Blad}{\mathbf{𝐰}\mathbf{𝐡}\mathbf{𝐢}\mathbf{𝐥}\mathbf{𝐞}b\mathbf{𝐝}\mathbf{𝐨}I,s⟶Blad}$

I tak dalej.

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

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