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ęć.

Zadania z rozwiązaniami

Ć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 \leq 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}}}

Ć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

Zadanie 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$.

Zadanie 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.