Semantyka i weryfikacja programów/Ćwiczenia 1

Zawartość

Tematem tych zajęć jest semantyka operacyjna wyrażeń (małe kroki).

Semantyka operacyjna wyrażeń

Ćwiczenie 1

Rozważmy bardzo prosty język wyrażeń, którego składnia opisana jest następującą gramatyką:

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

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

$e::=n|x|e_1+e_2|\mathbf{𝐢}\mathbf{𝐟}{e}_1\mathbf{𝐭}\mathbf{𝐡}\mathbf{𝐞}\mathbf{𝐧}{e}_2\mathbf{𝐞}\mathbf{𝐥}\mathbf{𝐬}\mathbf{𝐞}{e}_3$

Wynikiem wyrażenienia warunkowego $\mathbf{𝐢}\mathbf{𝐟}{e}_1\mathbf{𝐭}\mathbf{𝐡}\mathbf{𝐞}\mathbf{𝐧}{e}_2\mathbf{𝐞}\mathbf{𝐥}\mathbf{𝐬}\mathbf{𝐞}{e}_3$ jest wartość wyrażenia $e_2$, o ile wyrażenie $e_1$ oblicza się do wartości różnej od zera; w przeciwnym przypadku wynikiem jest wartość wyrażenia $e_3$.

Zaproponuj semantykę operacyjną (małe kroki) dla tego języka.

Rozwiązanie

{{{3}}}

Ćwiczenie 2

{{{3}}}

Przykład

$\mathbf{𝐥}\mathbf{𝐞}\mathbf{𝐭}x=0\mathbf{𝐢}\mathbf{𝐧}\mathbf{𝐥}\mathbf{𝐞}\mathbf{𝐭}y=7\mathbf{𝐢}\mathbf{𝐧}\mathbf{𝐥}\mathbf{𝐞}\mathbf{𝐭}x=y+3\mathbf{𝐢}\mathbf{𝐧}x+x+y\mapsto \text{wynik}=24$

$\mathbf{𝐥}\mathbf{𝐞}\mathbf{𝐭}y=5\mathbf{𝐢}\mathbf{𝐧}\mathbf{𝐥}\mathbf{𝐞}\mathbf{𝐭}x=(\mathbf{𝐥}\mathbf{𝐞}\mathbf{𝐭}y=3\mathbf{𝐢}\mathbf{𝐧}y+y)\mathbf{𝐢}\mathbf{𝐧}x+y\mapsto \text{wynik}=11$

Parser nie mógł rozpoznać (błąd składni): {\displaystyle \mathbf{let}\, z = 5 \,\mathbf{in}\, x+z \quad \quad \mapsto \quad \quad \mbox{brak wyniku; odwołanie do niezainicjowanej zmiennej}\, x }

$\mathbf{𝐥}\mathbf{𝐞}\mathbf{𝐭}x=1\mathbf{𝐢}\mathbf{𝐧}\mathbf{𝐥}\mathbf{𝐞}\mathbf{𝐭}x=x+x\mathbf{𝐢}\mathbf{𝐧}x+x\mapsto \text{wynik}=4$

Rozwiązanie

{{{3}}}

Zadania domowe

Ćwiczenie 1

Zapisz wariant 2 semantyki z poprzedniego zadania.

Ćwiczenie 2

Dotychczas wystąpienie błędu podczas obliczania wyrażenia, np. odwołanie do niezainicjowanej zmiennej, powodowało, że wyrażenie nie posiadało wartości (nie było ciągu tranzycji prowadzących do konfiguracji końcowej). Zmodyfikuj którąś z semantyk z poprzednich zadań tak, aby błąd był komunikowany jako jedna z konfiguracji końcowych. To znaczy: jeśli obliczenie wyrażenia $e$ w stanie $s$ jest niemożliwe bo wystąpił błąd, to

$e,s{⟹}^{*}\mathtt{B}\mathtt{l}\mathtt{a}\mathtt{d}.$

Ćwiczenie 3

Rozważ rozszerzenie języka wyrażeń o wyrażenia boolowskie:

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

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

$b::=\mathbf{𝐭}\mathbf{𝐫}\mathbf{𝐮}\mathbf{𝐞}|\mathbf{𝐟}\mathbf{𝐚}\mathbf{𝐥}\mathbf{𝐬}\mathbf{𝐞}|e_1\le e_2|\mathrm{\neg }b|b_1\wedge b_2$

$e::=n|x|e_1+e_2|\mathbf{𝐢}\mathbf{𝐟}b\mathbf{𝐭}\mathbf{𝐡}\mathbf{𝐞}\mathbf{𝐧}{e}_2\mathbf{𝐞}\mathbf{𝐥}\mathbf{𝐬}\mathbf{𝐞}{e}_3|\mathbf{𝐥}\mathbf{𝐞}\mathbf{𝐭}x=e_1\mathbf{𝐢}\mathbf{𝐧}{e}_2$

Zaproponuj semantykę małych kroków dla tego języka. Rozważ różne strategie obliczania wyrażeń boolowskich, oraz podejście leniwe. Na przykład w strategii lewostronnej dla $b_1\wedge b_2$, gdy $b_1$ zostało obliczone do $\mathbf{𝐟}\mathbf{𝐚}\mathbf{𝐥}\mathbf{𝐬}\mathbf{𝐞}$, w podejściu leniwym nie ma wogóle potrzeby obliczania $b_2$.