Semantyka i weryfikacja programów/Ćwiczenia 11

Semantyka w pełni 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_2:e_3$

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

Parser nie mógł rozpoznać (błąd składni): {\displaystyle i \, ::= \,\, x := e \,\,|\,\, i_1; i_2 \,\,|\,\, \mathbf{if}\, b \,\mathbf{then}\, i_1 \,\mathbf{else}\, i_2 \,\,|\,\, \mathbf{skip} \,\,|\,\, \mathbf{while}\, b \,\mathbf{do}\, i \,\,|\,\} ,

Wyrażenie $b?e_1:e_2$ to wyrażenie warunkowe. Wylicza się go wyliczając najpierw $b$. Jeśli wyliczy się ono do prawdy, to wartością całego wyrażenia jest wartość wyrażenia $e_1$, a w przeciwnym razie wartość wyrażenia $e_2$.

Zadanie 2

Tym razem większy przykład. Spróbujemy zdefiniować semantykę języka wzorowanego "nieco" na języku programowania C. Oto składnia:

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

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

Parser nie mógł rozpoznać (błąd składni): {\displaystyle l \, ::= \,\, x \,\,|\,\, x [e] \,\,|\,\} ,

$e::=n|l|e_1+e_2|b?e_2:e_3|l++|++l|l=e|l+=e|\mathbf{𝐜}\mathbf{𝐚}\mathbf{𝐥}\mathbf{𝐥}F(e)$

$i::=e|i_1;i_2|\mathbf{𝐢}\mathbf{𝐟}(e)i|\mathbf{𝐬}\mathbf{𝐤}\mathbf{𝐢}\mathbf{𝐩}|\mathbf{𝐰}\mathbf{𝐡}\mathbf{𝐢}\mathbf{𝐥}\mathbf{𝐞}(e)i|\mathbf{𝐟}\mathbf{𝐨}\mathbf{𝐫}(i_1;e;i_2)i_3|\mathbf{𝐛}\mathbf{𝐫}\mathbf{𝐞}\mathbf{𝐚}\mathbf{𝐤}|\mathbf{𝐜}\mathbf{𝐨}\mathbf{𝐧}\mathbf{𝐭}\mathbf{𝐢}\mathbf{𝐧}\mathbf{𝐮}\mathbf{𝐞}|\mathbf{𝐫}\mathbf{𝐞}\mathbf{𝐭}\mathbf{𝐮}\mathbf{𝐫}\mathbf{𝐧}e|\{d;i\}$

$d::=\mathbf{𝐯}\mathbf{𝐚}\mathbf{𝐫}x|\mathbf{𝐚}\mathbf{𝐫}\mathbf{𝐫}\mathbf{𝐚}\mathbf{𝐲}x[e]|d_1;d_2$

Zadanie 3

Zmień semantykę powyższego języka tak, aby przekazywanie parametrów odbywało się przez nazwę.

Zadanie 4

Zmień semantykę powyższego języka tak, aby przekazywanie parametrów odbywało się metodą copy-in copy-out.