Semantyka i weryfikacja programów/Ćwiczenia 12

Semantyka kontynuacyjna

Zadanie 1

Zdefiniuj kontynuacyjną semantykę następującego języka:

$n::=0|1|\dots$

$x::=\dots (identyfikatory)\dots$

$e::=n|x|e_1+e_2$

$b::=e_1<=e_2|\mathbf{𝐧}\mathbf{𝐨}\mathbf{𝐭}b|b_1\mathbf{𝐨}\mathbf{𝐫}{b}_2|\mathbf{𝐭}\mathbf{𝐫}\mathbf{𝐮}\mathbf{𝐞}$

$i::=x:=e|i_1;i_2|\mathbf{𝐢}\mathbf{𝐟}b\mathbf{𝐭}\mathbf{𝐡}\mathbf{𝐞}\mathbf{𝐧}{i}_1\mathbf{𝐞}\mathbf{𝐥}\mathbf{𝐬}\mathbf{𝐞}{i}_2|\mathbf{𝐬}\mathbf{𝐤}\mathbf{𝐢}\mathbf{𝐩}|\mathbf{𝐟}\mathbf{𝐨}\mathbf{𝐫}x=e_1\mathbf{𝐭}\mathbf{𝐨}{e}_2\mathbf{𝐭}\mathbf{𝐫}\mathbf{𝐲}{i}_1\mathbf{𝐞}\mathbf{𝐥}\mathbf{𝐬}\mathbf{𝐞}{i}_2|\mathbf{𝐟}\mathbf{𝐚}\mathbf{𝐢}\mathbf{𝐥}|\mathbf{𝐛}\mathbf{𝐞}\mathbf{𝐠}\mathbf{𝐢}\mathbf{𝐧}d;i\mathbf{𝐞}\mathbf{𝐧}\mathbf{𝐝}$

Znaczenie wszystkich konstrukcji z wyjątkiem Parser nie mógł rozpoznać (nieznana funkcja „\mathb”): {\displaystyle \mathbf{for}\, x = e_1\, \mathbf{to}\, e_2 \, \mathb{try}\, i_1\, \mathbf{else}\, i_2} oraz $\mathbf{𝐟}\mathbf{𝐚}\mathbf{𝐢}\mathbf{𝐥}$ jest standardowe.

Znaczenie instrukcji $\mathbf{𝐟}\mathbf{𝐨}\mathbf{𝐫}x=e_1\mathbf{𝐭}\mathbf{𝐨}{e}_2\mathbf{𝐭}\mathbf{𝐫}\mathbf{𝐲}{i}_1\mathbf{𝐞}\mathbf{𝐥}\mathbf{𝐬}\mathbf{𝐞}{i}_2$ jest następujące. Najpierw jeden raz jest obliczana wartość wyrażenia $e_1$ i podstawiana na zmienną $x$. Potem w pętli robimy co następuje: jeśli $x>e_2$ to wykonujemy $i_2$ w stanie sprzed instrukcji for (w szczególności wartość zmiennej $x$ na początku wykonywania $i_2$ powinna być przywrócona do tej sprzed wykonania instrukcji for) i przechodzimy do dalszej części programu. Natomiast jeśli $x\le e_2$, to jest wykonywana instrukcja $i_1$. Jeśli w $i_1$ nie zostanie napotkana instrukcja fail, to przywracamy starą wartość zmiennej $x$ (tę sprzed wykonania instrukcji for) i przechodzimy do dalszej części programu. Jeśli jednak napotkamy fail, to przywracamy stan sprzed wykonania instrukcji for (zachowując oczywiście wartość zmiennej $x$), zwiększamy wartość zmiennej $x$ o 1 i powtarzamy procedurę opisaną powyżej.

Instrukcja fail poza instrukcją for powinna powodować natychmiastowe zakończenie wykonywania programu. Jeśli fail występuję po else, czyli w $i_2$, to odnosi się ono do (być może nieistniejącej) zewnętrznej pętli for.

Zadanie 2

Oto pewien śmieszny język programowania:

$i::=x:=e|i_1;i_2|\mathbf{𝐢}\mathbf{𝐟}e\mathbf{𝐭}\mathbf{𝐡}\mathbf{𝐞}\mathbf{𝐧}{i}_1\mathbf{𝐞}\mathbf{𝐥}\mathbf{𝐬}\mathbf{𝐞}{i}_2|\mathbf{𝐬}\mathbf{𝐤}\mathbf{𝐢}\mathbf{𝐩}|\mathbf{𝐛}\mathbf{𝐚}\mathbf{𝐜}\mathbf{𝐤}|\mathbf{𝐥}\mathbf{𝐞}\mathbf{𝐟}\mathbf{𝐭}i|\mathbf{𝐫}\mathbf{𝐢}\mathbf{𝐠}\mathbf{𝐡}\mathbf{𝐭}i$

Programy w tym języku mogą wykonywać się w dwie strony: od lewej do prawej oraz od prawej do lewej. Wykonanie rozpoczyna się od pierwszej instrukcji i przebiega od lewej do prawej. Instrukcja back powoduje zmianę kierunku wykonania. Instrukcja left i powoduje wykonanie i jeśli wykonanie przebiega od prawej do lewej, w przeciwnym razie jest to instrukcja pusta. Symetrycznie działa right. Napisz semantykę tego języka.