Semantyka i weryfikacja programów/Ćwiczenia 2

Zadania z rozwiązaniami

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

$e::=0|1|\dots |x|e_1+e_2|\dots$

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$.

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$

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 nasze tranzycje nie posiadają teraz 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, czyli $\mathbf{𝐭}\mathbf{𝐫}\mathbf{𝐮}\mathbf{𝐞}$). Możemy odwołać się do tranzytywnego domknięcia relacji $⟹$ (czyli w zadadzie do semantyki 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, np. przy użyciu rozszerzonej składni. Znalezienie takiego rozwiązania pozostawiamy dociekliwemu czytelnikowi.

Reguły dla operacji arytmetycznych pozostawiamy do napisania Czytelnikowi.

Zadanie 2

Rozszerzmy język Tiny o następujące dobrze znane konstrukcje iteracji:

$I::=\mathbf{𝐫}\mathbf{𝐞}\mathbf{𝐩}\mathbf{𝐞}\mathbf{𝐚}\mathbf{𝐭}I\mathbf{𝐮}\mathbf{𝐧}\mathbf{𝐭}\mathbf{𝐢}\mathbf{𝐥}b|FORx:=e_1\mathbf{𝐭}\mathbf{𝐨}{e}_2\mathbf{𝐝}\mathbf{𝐨}I|\mathbf{𝐝}\mathbf{𝐨}Ie\mathbf{𝐭}\mathbf{𝐢}\mathbf{𝐦}\mathbf{𝐞}\mathbf{𝐬}|\mathbf{𝐝}\mathbf{𝐨}I\mathbf{𝐰}\mathbf{𝐡}\mathbf{𝐢}\mathbf{𝐥}\mathbf{𝐞}b$

Napisz semantykę małych kroków dla powyższych konstrukcji. Niedozwolone jest korzystanie z jakiejś konstrukcji w semantyce innej, np.

$\mathbf{𝐝}\mathbf{𝐨}I\mathbf{𝐰}\mathbf{𝐡}\mathbf{𝐢}\mathbf{𝐥}\mathbf{𝐞}b⟹\mathbf{𝐫}\mathbf{𝐞}\mathbf{𝐩}\mathbf{𝐞}\mathbf{𝐚}\mathbf{𝐭}I\mathbf{𝐮}\mathbf{𝐧}\mathbf{𝐭}\mathbf{𝐢}\mathbf{𝐥}\mathrm{\neg }b$

Zadanie 3

Rozszerz język Tiny o następującą instrukcję pętli:

$I::=LOOPI|EXIT|CONT\mathbf{𝐢}\mathbf{𝐧}UE$

$LOOPI$ to instrukcja pętli, $I$ stanowi instrukcję wewnętrzną. Instrukcja $EXIT$ wychodzi z nabliższej pętli $LOOP$ i kontynuuje wykonanie programu od pierwszej instrukcji za tą pętlą. Instrukcje $CONT\mathbf{𝐢}\mathbf{𝐧}UE$ powraca na początek instrukcji wewnętrznej.