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 (i d e n t y f i k a t o r y) \dots$

$e : : = n | x | e_{1} + e_{2} | 𝐢 𝐟 e_{1} 𝐭 𝐡 𝐞 𝐧 e_{2} 𝐞 𝐥 𝐬 𝐞 e_{3}$

Wynikiem wyra¿enienia warunkowego $𝐢 𝐟 e_{1} 𝐭 𝐡 𝐞 𝐧 e_{2} 𝐞 𝐥 𝐬 𝐞 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

Rozszerzmy jêzyk wyra¿eñ z poprzedniego zadania o jedn± konstrukcjê

$e : : = \dots | 𝐥 𝐞 𝐭 x = e_{1} 𝐢 𝐧 e_{2}$

Wyra¿enie $𝐥 𝐞 𝐭 x = e_{1} 𝐢 𝐧 e_{2}$ zawiera w sobie deklaracjê $x = e_{1}$ , która stanowi mechanizm wi±zania identyfikatorów w naszym jêzyku. Deklaracja $x = e_{1}$ wprowadza now± zmienn± $x$ oraz przypisuje jej warto¶æ. Warto¶æ wyra¿enia $𝐥 𝐞 𝐭 x = e_{1} 𝐢 𝐧 e_{2}$ obliczamy nastêpuj±co: najpierw oblicza siê warto¶æ $e_{1}$ , podstawia j± na zmienna $x$ , a nastêpnie oblicza wyra¿enie $e_{2}$ . Zakresem zmiennej $x$ jest wyra¿enie $e_{2}$ , czyli wewn±trz $e_{2}$ mo¿na odwo³ywaæ siê (wielokrotnie) do zmiennej $x$ ; Ogólniej, odwo³ania do zmiennej w wyra¿eniu odnosz± siê do najbli¿szej (najbardziej zagnie¿dzonej) deklaracji tej zmiennej. Taki mechanizm wi±zania identyfikatorów nazywamy wi±zaniem statycznym. Przyjmujemy zwyk³e (statyczne) regu³y przes³aniania zmiennych, np. je¶li w $e_{2}$ wystêpuje podwyra¿enie $𝐥 𝐞 𝐭 x = e 𝐢 𝐧 e^{'}$ to deklaracja $x = e$ przes³ania deklaracjê $x = e_{1}$ w wyra¿eniu $e^{'}$ .

Zak³adamy, ¿e na pocz±tku warto¶ci wszystkich zmiennych s± nieokre¶lone, czyli zmienne s± niezainicjowane, a odwo³anie do niezainicjowanej zmiennej jest uwa¿ane za niepoprawne.

Przykład

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

$𝐥 𝐞 𝐭 y = 5 𝐢 𝐧 𝐥 𝐞 𝐭 x = (𝐥 𝐞 𝐭 y = 3 𝐢 𝐧 y + y) 𝐢 𝐧 x + y \mapsto 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 }

$𝐥 𝐞 𝐭 x = 1 𝐢 𝐧 𝐥 𝐞 𝐭 x = x + x 𝐢 𝐧 x + x \mapsto 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 ⟹^{*} B l a d .$

Ćwiczenie 3

Rozwa¿ rozszerzenie jêzyka wyra¿eñ o wyra¿enia boolowskie:

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

$x : : = \dots (i d e n t y f i k a t o r y) \dots$

$b : : = 𝐭 𝐫 𝐮 𝐞 | 𝐟 𝐚 𝐥 𝐬 𝐞 | e_{1} \leq e_{2} | \neg b | b_{1} \land b_{2}$

$e : : = n | x | e_{1} + e_{2} | 𝐢 𝐟 b 𝐭 𝐡 𝐞 𝐧 e_{2} 𝐞 𝐥 𝐬 𝐞 e_{3} | 𝐥 𝐞 𝐭 x = e_{1} 𝐢 𝐧 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} \land b_{2}$ , gdy $b_{1}$ zosta³o obliczone do $𝐟 𝐚 𝐥 𝐬 𝐞$ , w podej¶ciu leniwym nie ma wogóle potrzeby obliczania $b_{2}$ .

Semantyka i weryfikacja programów/Ćwiczenia 1

Zawarto¶æ

Semantyka operacyjna wyra¿eñ

Zadania domowe

Menu nawigacyjne

Działania na stronie

Opcje strony

Narzędzia osobiste

Nawigacja

Szukaj

Narzędzia