Semantyka i weryfikacja programów/Ćwiczenia 12

From Studia Informatyczne

Semantyka kontynuacyjna

Zadanie 1

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

n \, ::= \,\, 0 \,\,|\,\, 1 \,\,|\,\, \ldots

x \, ::= \,\, \ldots \, (identyfikatory) \, \ldots

e \,  ::=  \,\,           n   \,\,|\,\,         x   \,\,|\,\,         e_1 + e_2

b \,  ::=  \,\,           e_1 <= e_2   \,\,|\,\,         \mathbf{not}\, b    \,\,|\,\,         b_1\, \mathbf{or}\, b_2 \,\,|\,\,         \mathbf{true}

i \, ::= \,\,          x := e     \,\,|\,\,          i_1; i_2   \,\,|\,\,          \mathbf{if}\, b \,\mathbf{then}\, i_1 \,\mathbf{else}\, i_2 \,\,|\,\,          \mathbf{skip} \,\,|\,\,          \mathbf{for}\, x = e_1\, \mathbf{to} e_2 \,\mathbf{try}\, i_1          \mathbf{else}\, i_2 \,\,|\,\,          \mathbf{fail} \,\,|\,\,          \mathbf{begin}\, d; i\, \mathbf{end}

Znaczenie wszystkich konstrukcji z wyjątkiem \mathbf{for}\, x = e_1\, \mathbf{to}\, e_2 \, \mathb{try}\, i_1\, \mathbf{else}\, i_2 oraz \mathbf{fail} jest standardowe.

Znaczenie instrukcji \mathbf{for}\, x = e_1\, \mathbf{to}\, e_2\, \mathbf{try}\, i_1\, \mathbf{else}\, 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 \leq 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{if}\, e \,\mathbf{then}\, i_1 \,\mathbf{else}\, i_2 \,\,|\,\,          \mathbf{skip} \,\,|\,\,          \mathbf{back} \,\,|\,\,          \mathbf{left}\, i \,\,|\,\,          \mathbf{right}\, 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.