Semantyka i weryfikacja programów/Ćwiczenia 11

From Studia Informatyczne

Spis treści

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

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

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 \, ::= \ldots \,\, -1, \,\, 0 \,\,|\,\, 1 \,\,|\,\, \ldots

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

l \, ::= \,\,          x     \,\,|\,\,         x [e]  \,\,|\,\,

e \,  ::=  \,\,           n   \,\,|\,\,         l   \,\,|\,\,         e_1 + e_2 \,\,|\,\,         b\, ?\, e_2\, :\, e_3  \,\,|\,\,         l++ \,\,|\,\,         ++l \,\,|\,\,         l = e \,\,|\,\,         l += e \,\,|\,\,         \mathbf{call}\, F (e)

i \, ::= \,\,          e     \,\,|\,\,          i_1; i_2   \,\,|\,\,          \mathbf{if}\, (e)\,  i \,\,|\,\,          \mathbf{skip} \,\,|\,\,          \mathbf{while}\, (e) \,i \,\,|\,\,          \mathbf{for}\, (i_1; e; i_2) \,i_3 \,\,|\,\,          \mathbf{break} \,\,|\,\,          \mathbf{continue} \,\,|\,\,          \mathbf{return}\, e \,\,|\,\,          \{ d; i \}

d \, ::= \,\,          \mathbf{var}\, x        \,\,|\,\,         \mathbf{array}\, 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.