Semantyka i weryfikacja programów/Ćwiczenia 5

Zawarto¶æ

Kontynuujemy æwiczenie semantyki naturalnej, dodaj±c pewne konstrukcje do jêzyka Tiny. W szczególno¶ci rozszerzymy go o deklaracje zmiennych (bloki). Po raz pierwszy roszdzielimy informacjê przechowywan± w konfiguracji na ¶rodowisko okre¶laj±ce wi±zanie identyfikatorów i stan przechowuj±cy warto¶ci zmiennych. Bêdzie to przygotowanie do kolejnych zajêæ.

Semantyka naturalna pewnej instrukcji $\mathbf{𝐟}\mathbf{𝐨}\mathbf{𝐫}$

Ćwiczenie 1

Rozszerzamy jêzyk Tiny nastêpuj±co:

$I::=\dots |\mathbf{𝐟}\mathbf{𝐨}\mathbf{𝐫}x=e_1\mathbf{𝐭}\mathbf{𝐨}{e}_2\mathbf{𝐭}\mathbf{𝐫}\mathbf{𝐲}{I}_1\mathbf{𝐞}\mathbf{𝐥}\mathbf{𝐬}\mathbf{𝐞}{I}_2|\mathbf{𝐟}\mathbf{𝐚}\mathbf{𝐢}\mathbf{𝐥}$

Znaczenie instrukcji $\mathbf{𝐟}\mathbf{𝐨}\mathbf{𝐫}x=e_1\mathbf{𝐭}\mathbf{𝐨}{e}_2\mathbf{𝐭}\mathbf{𝐫}\mathbf{𝐲}{I}_1\mathbf{𝐞}\mathbf{𝐥}\mathbf{𝐬}\mathbf{𝐞}{I}_2$ jest nastêpuj±ce. Obliczamy warto¶ci wyra¿eñ $e_1$ i $e_2$. Je¶li pierwsza z nich jest mniejsza lub równa od drugiej, to podstawiamy pierwsz± warto¶æ (warto¶æ wyra¿enia $e_1$) na zmienn± $x$ i uruchamiamy $I_1$. Je¶li w $I_1$ nie zostanie napotkana instrukcja $\mathbf{𝐟}\mathbf{𝐚}\mathbf{𝐢}\mathbf{𝐥}$, koñczymy instrukcjê $\mathbf{𝐟}\mathbf{𝐨}\mathbf{𝐫}$ i przyracamy warto¶æ zmiennej $x$ sprzed tej instrukcji. Natomiast je¶li w $I_1$ zostanie napotkana instrukcja $\mathbf{𝐟}\mathbf{𝐚}\mathbf{𝐢}\mathbf{𝐥}$, podstawiamy na $x$ kolejn±, o jeden wiêksz± warto¶æ, przywracamy warto¶ci wszystkich pozosta³ych zmiennych sprzed instrukcji $\mathbf{𝐟}\mathbf{𝐨}\mathbf{𝐫}$, i ponownie wykonujemy $I_1$. Powtarzamy w ten sposób a¿ $I_1$ zakoñczy siê nie napotkawszy $\mathbf{𝐟}\mathbf{𝐚}\mathbf{𝐢}\mathbf{𝐥}$, albo warto¶æ zmiennej $x$ przekroczy warto¶æ wyra¿enia $e_2$ obliczon± na pocz±tku. W pierwszym przypadku koñczymy instrukcjê $\mathbf{𝐟}\mathbf{𝐨}\mathbf{𝐫}$ i przyracamy warto¶æ zmiennej $x$ sprzed tej instrukcji. W drugim przywracamy warto¶ci wszystkich zmiennych sprzed instrukcji $\mathbf{𝐟}\mathbf{𝐨}\mathbf{𝐫}$ i uruchamiamy $I_2$.

Przykład

Oto przyk³adowy program:

x := 0; y := 1;
$\mathbf{𝐟}\mathbf{𝐨}\mathbf{𝐫}$ x := 1 \,\mathbf{to}\, 5 $\mathbf{𝐭}\mathbf{𝐫}\mathbf{𝐲}$
  y := y+1;
  $\mathbf{𝐢}\mathbf{𝐟}$ x <= 4 $\mathbf{𝐭}\mathbf{𝐡}\mathbf{𝐞}\mathbf{𝐧}\mathbf{𝐟}\mathbf{𝐚}\mathbf{𝐢}\mathbf{𝐥}\mathbf{𝐞}\mathbf{𝐥}\mathbf{𝐬}\mathbf{𝐞}$ z:= x
$\mathbf{𝐞}\mathbf{𝐥}\mathbf{𝐬}\mathbf{𝐞}\mathbf{𝐬}\mathbf{𝐤}\mathbf{𝐢}\mathbf{𝐩}$

Warto¶ci zmiennych po zakoñczeniu programu to: $x=0,y=2,z=5$.

Rozwiązanie

{{{3}}}

Semantyka naturalna bloków

Ćwiczenie 2 (bloki i deklaracje zmiennych)

Rozszerz semantykê jêzyka Tiny o deklaracjê zmiennej:

$I::=\dots |\mathbf{𝐛}\mathbf{𝐞}\mathbf{𝐠}\mathbf{𝐢}\mathbf{𝐧}\mathbf{𝐯}\mathbf{𝐚}\mathbf{𝐫}x=e;I\mathbf{𝐞}\mathbf{𝐧}\mathbf{𝐝}$

Zasiêgiem zmiennej $x$ jest instrukcja $I$ czyli wnêtrze bloku, w którym jest zadeklarowana. Zak³adamy zwyk³e (statyczne) regu³y widoczno¶ci, przes³aniania, itp.

Rozwiązanie

{{{3}}}

Zadania domowe

Ćwiczenie 1

Napisz semantykê naturaln± dla nastêpuj±cego rozszerzenia jêzyka Tiny:

Parser nie mógł rozpoznać (nieznana funkcja „\ldotes”): {\displaystyle I \, ::= \,\, \ldotes \,\,|\,\, \mathbf{throw}\, x \,\,|\,\, \,\mathbf{try}\, I_1 \,\mathbf{catch}\, exc\, I_2 }

$exc::=x|\mathbf{𝐚}\mathbf{𝐧}\mathbf{𝐲}$

Instrukcja $\mathbf{𝐭}\mathbf{𝐡}\mathbf{𝐫}\mathbf{𝐨}\mathbf{𝐰}x$ oznacza podniesienie wyj±tku o nazwie $x$. Instrukcja $I=\mathbf{𝐭}\mathbf{𝐫}\mathbf{𝐲}{I}_1\mathbf{𝐜}\mathbf{𝐚}\mathbf{𝐭}\mathbf{𝐜}\mathbf{𝐡}exc{I}_2$ wykonuje $I_1$. Je¶li podczas wykonania $I_1$ zostanie podniesiony wyj±tej $x$, i $exc=x$ albo $exc=\mathbf{𝐚}\mathbf{𝐧}\mathbf{𝐲}$, to nastêpuje przerwanie $I_1$ i sterowanie zostaje przeniesione do $I_2$ (nastêpuje obs³uga wyj±tku). Je¶li za¶ podczas wykonania $I_1$ zostanie podniesiony wyj±tej $x$ oraz $exc\ne x$ i $exc\ne \mathbf{𝐚}\mathbf{𝐧}\mathbf{𝐲}$, to obs³uga wyj±tku przekazana jest do najbli¿szej instrukcji $\mathbf{𝐭}\mathbf{𝐫}\mathbf{𝐲}$ otaczaj±cej $I$. Umawiamy siê, ¿e $\mathbf{𝐭}\mathbf{𝐫}\mathbf{𝐲}{I}_1\mathbf{𝐜}\mathbf{𝐚}\mathbf{𝐭}\mathbf{𝐜}\mathbf{𝐡}exc{I}_2$ otacza $I_1$ i wszystkie instrukcje wewn±trz $I_1$, ale nie otacza $I_2$.

Ćwiczenie 2

Zaproponuj modyfikacjê semantyki, w której deklaracja jest wykonywana ,,równolegle", analogicznie do przypisania równoleg³ego. Przy takiej semantyce kolejno¶æ poszczególnych deklaracji powinna byæ nieistotna.