Semantyka i weryfikacja programów/Ćwiczenia 5: Różnice pomiędzy wersjami
Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
m Zastępowanie tekstu – „.↵</math>” na „</math>” |
|||
| (Nie pokazano 5 pośrednich wersji utworzonych przez tego samego użytkownika) | |||
| Linia 8: | Linia 8: | ||
== Semantyka naturalna pewnej instrukcji <math>\mathbf{for}\ | == Semantyka naturalna pewnej instrukcji <math>\mathbf{for}\ </math>, == | ||
| Linia 25: | Linia 25: | ||
Znaczenie instrukcji <math>\mathbf{for}\, x = e_1 \,\mathbf{to}\, e_2 \,\mathbf{try}\, I_1 \,\mathbf{else}\, I_2</math> jest następujące. | Znaczenie instrukcji <math>\mathbf{for}\, x = e_1 \,\mathbf{to}\, e_2 \,\mathbf{try}\, I_1 \,\mathbf{else}\, I_2</math> jest następujące. | ||
Obliczamy wartości wyrażeń <math>e_1</math> i <math>e_2</math>. Jeśli pierwsza z nich jest mniejsza od lub równa drugiej, podstawiamy pierwszą wartość (wartość wyrażenia <math>e_1</math>) na zmienną <math>x</math> i uruchamiamy <math>I_1</math>. | Obliczamy wartości wyrażeń <math>e_1</math> i <math>e_2</math>. Jeśli pierwsza z nich jest mniejsza od lub równa drugiej, podstawiamy pierwszą wartość (wartość wyrażenia <math>e_1</math>) na zmienną <math>x</math> i uruchamiamy <math>I_1</math>. | ||
Jeśli w <math>I_1</math> nie zostanie napotkana instrukcja <math>\mathbf{fail}</math>, kończymy instrukcję <math>\mathbf{for}\ | Jeśli w <math>I_1</math> nie zostanie napotkana instrukcja <math>\mathbf{fail}</math>, kończymy instrukcję <math>\mathbf{for}\ </math>, i przyracamy wartość zmiennej <math>x</math> | ||
sprzed tej instrukcji. | sprzed tej instrukcji. | ||
Natomiast jeśli w <math>I_1</math> zostanie napotkana instrukcja <math>\mathbf{fail}</math>, podstawiamy na <math>x</math> kolejną, o jeden większą wartość, przywracamy wartości wszystkich | Natomiast jeśli w <math>I_1</math> zostanie napotkana instrukcja <math>\mathbf{fail}</math>, podstawiamy na <math>x</math> kolejną, o jeden większą wartość, przywracamy wartości wszystkich | ||
pozostałych zmiennych sprzed instrukcji <math>\mathbf{for}\ | pozostałych zmiennych sprzed instrukcji <math>\mathbf{for}\ </math>, i ponownie wykonujemy <math>I_1</math>. | ||
Powtarzamy w ten sposób, aż <math>I_1</math> zakończy się nie napotkawszy <math>\mathbf{fail}</math>, albo wartość zmiennej <math>x</math> przekroczy wartość wyrażenia <math>e_2</math> obliczoną na początku. | Powtarzamy w ten sposób, aż <math>I_1</math> zakończy się nie napotkawszy <math>\mathbf{fail}</math>, albo wartość zmiennej <math>x</math> przekroczy wartość wyrażenia <math>e_2</math> obliczoną na początku. | ||
W pierwszym przypadku kończymy instrukcję <math>\mathbf{for}\ | W pierwszym przypadku kończymy instrukcję <math>\mathbf{for}\ </math>, i przyracamy wartość zmiennej <math>x</math> sprzed tej instrukcji. | ||
W drugim przywracamy wartości wszystkich zmiennych sprzed instrukcji <math>\mathbf{for}\ | W drugim przywracamy wartości wszystkich zmiennych sprzed instrukcji <math>\mathbf{for}\ </math>, i uruchamiamy <math>I_2</math>. | ||
}} | }} | ||
| Linia 40: | Linia 40: | ||
x := 0; y := 1; | x := 0; y := 1; | ||
<math>\mathbf{for}\ | <math>\mathbf{for}\ </math>, x := 1 <math>\,\mathbf{to}\ </math>, 5 <math>\,\mathbf{try}\ </math>, | ||
y := y+1; | y := y+1; | ||
<math>\mathbf{if}\ | <math>\mathbf{if}\ </math>, x <= 4 <math>\,\mathbf{then}\, \mathbf{fail} \,\mathbf{else}\ </math>, z:= x | ||
<math>\,\mathbf{else}\, \mathbf{skip}</math> | <math>\,\mathbf{else}\, \mathbf{skip}</math> | ||
| Linia 57: | Linia 57: | ||
<math> | <math> | ||
I, s \,\longrightarrow\, s' \quad \quad \quad e, s \,\longrightarrow\, n | I, s \,\longrightarrow\, s' \quad \quad \quad e, s \,\longrightarrow\, n</math> | ||
</math> | |||
Zacznijmy od najprostszego przypadku, gdy nie ma wogóle potrzeby uruchamiania instrukcji wewnętrznej <math>I_1</math>, ponieważ wartość wyrażenia <math>e_1</math> jest większa od <math>e_2</math>: | Zacznijmy od najprostszego przypadku, gdy nie ma wogóle potrzeby uruchamiania instrukcji wewnętrznej <math>I_1</math>, ponieważ wartość wyrażenia <math>e_1</math> jest większa od <math>e_2</math>: | ||
| Linia 69: | Linia 68: | ||
I_2, s \,\longrightarrow\, s'} | I_2, s \,\longrightarrow\, s'} | ||
{\mathbf{for}\, x = e_1 \,\mathbf{to}\, e_2 \,\mathbf{try}\, I_1 \,\mathbf{else}\, I_2, s \,\longrightarrow\, s'} | {\mathbf{for}\, x = e_1 \,\mathbf{to}\, e_2 \,\mathbf{try}\, I_1 \,\mathbf{else}\, I_2, s \,\longrightarrow\, s'} | ||
\quad \mbox{ o ile } n_1 > n_2 | \quad \mbox{ o ile } n_1 > n_2</math> | ||
</math> | |||
Po prostu uruchamiamy instrukcję <math>I_2</math> w stanie <math>s</math>, ignorując <math>I_1</math>. | Po prostu uruchamiamy instrukcję <math>I_2</math> w stanie <math>s</math>, ignorując <math>I_1</math>. | ||
| Linia 84: | Linia 82: | ||
I_1, s[x \mapsto n_1] \,\longrightarrow\, s'} | I_1, s[x \mapsto n_1] \,\longrightarrow\, s'} | ||
{\mathbf{for}\, x = e_1 \,\mathbf{to}\, e_2 \,\mathbf{try}\, I_1 \,\mathbf{else}\, I_2, s \,\longrightarrow\, s'[x \mapsto s(x)]} | {\mathbf{for}\, x = e_1 \,\mathbf{to}\, e_2 \,\mathbf{try}\, I_1 \,\mathbf{else}\, I_2, s \,\longrightarrow\, s'[x \mapsto s(x)]} | ||
\quad \mbox{ o ile } n_1 \leq n_2 | \quad \mbox{ o ile } n_1 \leq n_2</math> | ||
</math> | |||
Tym razem uruchamiamy instrukcję <math>I_1</math>, podstawiając na zmienną <math>x</math> wartość <math>n_1</math>. | Tym razem uruchamiamy instrukcję <math>I_1</math>, podstawiając na zmienną <math>x</math> wartość <math>n_1</math>. | ||
| Linia 94: | Linia 91: | ||
<math> | <math> | ||
I, s \,\longrightarrow\, \mbox{było-}\mathbf{fail} | I, s \,\longrightarrow\, \mbox{było-}\mathbf{fail}</math> | ||
</math> | |||
Mówiąc formalnie, poszerzamy zbiór konfiguracji o jeden element <math>\mbox{było-}\mathbf{fail}</math>. | Mówiąc formalnie, poszerzamy zbiór konfiguracji o jeden element <math>\mbox{było-}\mathbf{fail}</math>. | ||
Zauważmy, że po prawej stronie tranzycji nie ma wogóle stanu. | Zauważmy, że po prawej stronie tranzycji nie ma wogóle stanu. | ||
Nie potrzebujemy go dla opisania semantyki instrukcji <math>\mathbf{for}\ | Nie potrzebujemy go dla opisania semantyki instrukcji <math>\mathbf{for}\ </math>,: jeśli wystąpi <math>\mathbf{fail}</math>, powtarzamy <math>I_1</math> dla większej o <math>1</math> wartości zmiennej <math>x</math>, ale pozostałym zmiennym przywracamy wartość ''sprzed'' <math>I_1</math>. | ||
A więc załóżmy, że | A więc załóżmy, że | ||
<math>I_1, s[x \mapsto n_1] \,\longrightarrow\, \mbox{było-}\mathbf{fail} | <math>I_1, s[x \mapsto n_1] \,\longrightarrow\, \mbox{było-}\mathbf{fail}</math>. | ||
W takiej sytuacji powinniśmy przypisać <math>n_1 + 1</math> na zmienną <math>x</math> i spróbować ponownie wykonać <math>I_1</math> przy wartościach wszystkich pozostałych zmiennych, takich jak na początku instrukcji <math>\mathbf{for}\ | W takiej sytuacji powinniśmy przypisać <math>n_1 + 1</math> na zmienną <math>x</math> i spróbować ponownie wykonać <math>I_1</math> przy wartościach wszystkich pozostałych zmiennych, takich jak na początku instrukcji <math>\mathbf{for}\ </math>,. | ||
Powtarzamy ten schemat aż do skutku, tzn. aż do mementu, gdy zaistnieje któraś z poprzednich dwóch (prostych) sytuacji. | Powtarzamy ten schemat aż do skutku, tzn. aż do mementu, gdy zaistnieje któraś z poprzednich dwóch (prostych) sytuacji. | ||
Oto odpowiednia reguła: | Oto odpowiednia reguła: | ||
| Linia 117: | Linia 113: | ||
\mathbf{for}\, x = e_1 + 1 \,\mathbf{to}\, e_2 \,\mathbf{try}\, I_1 \,\mathbf{else}\, I_2, s \,\longrightarrow\, s'} | \mathbf{for}\, x = e_1 + 1 \,\mathbf{to}\, e_2 \,\mathbf{try}\, I_1 \,\mathbf{else}\, I_2, s \,\longrightarrow\, s'} | ||
{\mathbf{for}\, x = e_1 \,\mathbf{to}\, e_2 \,\mathbf{try}\, I_1 \,\mathbf{else}\, I_2, s \,\longrightarrow\, s'} | {\mathbf{for}\, x = e_1 \,\mathbf{to}\, e_2 \,\mathbf{try}\, I_1 \,\mathbf{else}\, I_2, s \,\longrightarrow\, s'} | ||
\quad \mbox{ o ile } n_1 \leq n_2 | \quad \mbox{ o ile } n_1 \leq n_2</math> | ||
</math> | |||
Zwróćmy uwagę na pewnien niezwykle istotny szczegół: po zakończeniu wykonania instrukcji <math>\mathbf{for}\, x = e_1 + 1 \,\mathbf{to}\, e_2 \,\mathbf{try}\, I_1 \,\mathbf{else}\, I_2</math> otrzymujemy stan <math>s'</math>, w którym '''nie przywracamy''' wartości zmiennej <math>x</math>. | Zwróćmy uwagę na pewnien niezwykle istotny szczegół: po zakończeniu wykonania instrukcji <math>\mathbf{for}\, x = e_1 + 1 \,\mathbf{to}\, e_2 \,\mathbf{try}\, I_1 \,\mathbf{else}\, I_2</math> otrzymujemy stan <math>s'</math>, w którym '''nie przywracamy''' wartości zmiennej <math>x</math>. | ||
Gdybyśmy tak zrobili, tzn. gdybyśmy zastąpili <math>s'</math> przez <math>s'[x \mapsto s(x)]</math>, nasze semantyka byłaby niepoprawna. | Gdybyśmy tak zrobili, tzn. gdybyśmy zastąpili <math>s'</math> przez <math>s'[x \mapsto s(x)]</math>, nasze semantyka byłaby niepoprawna. | ||
Dlaczego? Dlatego, że nie wiemy tak naprawdę, czy powinniśmy przywracać wartość zmiennej <math>x</math>, czy nie. | Dlaczego? Dlatego, że nie wiemy tak naprawdę, czy powinniśmy przywracać wartość zmiennej <math>x</math>, czy nie. | ||
Jeśli ostatecznie nasza instrukcja <math>\mathbf{for}\ | Jeśli ostatecznie nasza instrukcja <math>\mathbf{for}\ </math>, zakończyła się przez bezbłędne zakończenie instrukcji <math>I_1</math> (przypadek drugi), to powinniśmy to zrobić; ale jeśli zakończyła się wykonaniem instrukcji <math>I_2</math> (przypadek pierwszy), powinniśmy pozostawić wartość zmiennej <math>x</math> taką, jaka jest ona po zakończeniu <math>I_2</math>. | ||
A zatem w powyższej regule dla przypadku trzeciego nie przywracamy wartości zmiennej <math>x</math>; jeśli było to konieczne, to zostało już wykonane "głębiej", dzięki regule dla przypadku drugiego oraz dzięki temu, że instrukcja <math>\mathbf{for}\, x = e_1 + 1 \,\mathbf{to}\, e_2 \,\mathbf{try}\, I_1 \,\mathbf{else}\, I_2</math> wykonywana jest w orginalnym stanie <math>s</math>, a nie w stanie, w którym kończy się <math>I_1</math> (tego ostatniego stanu nawet nie znamy). | A zatem w powyższej regule dla przypadku trzeciego nie przywracamy wartości zmiennej <math>x</math>; jeśli było to konieczne, to zostało już wykonane "głębiej", dzięki regule dla przypadku drugiego oraz dzięki temu, że instrukcja <math>\mathbf{for}\, x = e_1 + 1 \,\mathbf{to}\, e_2 \,\mathbf{try}\, I_1 \,\mathbf{else}\, I_2</math> wykonywana jest w orginalnym stanie <math>s</math>, a nie w stanie, w którym kończy się <math>I_1</math> (tego ostatniego stanu nawet nie znamy). | ||
| Linia 134: | Linia 129: | ||
</math> | </math> | ||
oraz aby wystąpienie <math>\mathbf{fail}</math> umiejscowione gdzieś "głęboko" zostało rozpropagowane do najbliższej otaczającej instrukcji <math>\mathbf{for}\ | oraz aby wystąpienie <math>\mathbf{fail}</math> umiejscowione gdzieś "głęboko" zostało rozpropagowane do najbliższej otaczającej instrukcji <math>\mathbf{for}\ </math>,. | ||
Jeśli pojawił się <math>\mathbf{fail}</math>, powinniśmy zaniechać dalszego wykonania instrukcji, a w przypadku pętli, powinniśmy zaniechać dalszego iterowania tej pętli. | Jeśli pojawił się <math>\mathbf{fail}</math>, powinniśmy zaniechać dalszego wykonania instrukcji, a w przypadku pętli, powinniśmy zaniechać dalszego iterowania tej pętli. | ||
Oto odpowiednie reguły: | Oto odpowiednie reguły: | ||
| Linia 164: | Linia 159: | ||
Widać podobieństwo do analogicznych reguł dla pętli <math>\mathbf{loop}\, I</math>, którą zajmowaliśmy się na wcześniejszych zajęciach. | Widać podobieństwo do analogicznych reguł dla pętli <math>\mathbf{loop}\, I</math>, którą zajmowaliśmy się na wcześniejszych zajęciach. | ||
Zauważmy, że jeśli <math>\mathbf{fail}</math> zostało wykonane poza jakąkolwiek pętlą <math>\mathbf{for}\ | Zauważmy, że jeśli <math>\mathbf{fail}</math> zostało wykonane poza jakąkolwiek pętlą <math>\mathbf{for}\ </math>,, to program "zakończy się" w konfiguracji <math>\mbox{było-}\mathbf{fail}</math>. | ||
Możemy zatem tę właśnie konfigurację uznać za konfigurację końcową, informującą o porażce wykonania programu. | Możemy zatem tę właśnie konfigurację uznać za konfigurację końcową, informującą o porażce wykonania programu. | ||
| Linia 185: | Linia 180: | ||
Zakładamy zwykłe (statyczne) reguły widoczności, przesłaniania, itp. | Zakładamy zwykłe (statyczne) reguły widoczności, przesłaniania, itp. | ||
}} | }} | ||
| Linia 236: | Linia 229: | ||
<math> | <math> | ||
\mathbf{Store} = \mathbf{Loc} \to_{\mathrm{fin}} \mathbf{Num} | \mathbf{Store} = \mathbf{Loc} \to_{\mathrm{fin}} \mathbf{Num}</math> | ||
</math> | |||
Dla ścisłości używamy innej nazwy (<math>\mathbf{Store}</math>), ale będziemy zwykle używać podobnych symboli jak dotychczas <math>s, s', s_1, \ldots \in \mathbf{Store}</math> itp. do nazywania stanów. | Dla ścisłości używamy innej nazwy (<math>\mathbf{Store}</math>), ale będziemy zwykle używać podobnych symboli jak dotychczas <math>s, s', s_1, \ldots \in \mathbf{Store}</math> itp. do nazywania stanów. | ||
| Linia 276: | Linia 268: | ||
<math> | <math> | ||
\mathtt{newloc}(s) \notin \mathrm{dom}(s) | \mathtt{newloc}(s) \notin \mathrm{dom}(s)</math> | ||
</math> | |||
Dla ilustracji popatrzmy na przykładową regułę dla deklaracji. | Dla ilustracji popatrzmy na przykładową regułę dla deklaracji. | ||
| Linia 285: | Linia 276: | ||
E[x \mapsto l] \,\vdash\, I, s[l \mapsto n] \,\longrightarrow\, s'} | E[x \mapsto l] \,\vdash\, I, s[l \mapsto n] \,\longrightarrow\, s'} | ||
{E \,\vdash\, \mathbf{begin}\, \mathbf{var}\, x=e;\, I \,\mathbf{end}, s \,\longrightarrow\, s'} | {E \,\vdash\, \mathbf{begin}\, \mathbf{var}\, x=e;\, I \,\mathbf{end}, s \,\longrightarrow\, s'} | ||
\quad \mbox{ gdzie } l = \mathtt{newloc}(s) | \quad \mbox{ gdzie } l = \mathtt{newloc}(s)</math> | ||
</math> | |||
Zauważmy, że stan <math>s'</math> po zakończeniu instrukcji <math>\mathbf{begin}\, \mathbf{var}\, x=e;\, I \,\mathbf{end}</math> zawiera informację o zmiennej lokalnej <math>x</math>, tzn. <math>s(l)</math> jest określone. | Zauważmy, że stan <math>s'</math> po zakończeniu instrukcji <math>\mathbf{begin}\, \mathbf{var}\, x=e;\, I \,\mathbf{end}</math> zawiera informację o zmiennej lokalnej <math>x</math>, tzn. <math>s(l)</math> jest określone. | ||
| Linia 382: | Linia 372: | ||
E[x \mapsto l] \,\vdash\, I, s[l \mapsto n] \,\longrightarrow\, s'} | E[x \mapsto l] \,\vdash\, I, s[l \mapsto n] \,\longrightarrow\, s'} | ||
{E \,\vdash\, \mathbf{begin}\, \mathbf{var}\, x=e;\, I \,\mathbf{end}, s \,\longrightarrow\, s' \setminus \{ (l, s'(l)) \}} | {E \,\vdash\, \mathbf{begin}\, \mathbf{var}\, x=e;\, I \,\mathbf{end}, s \,\longrightarrow\, s' \setminus \{ (l, s'(l)) \}} | ||
\quad \mbox{ gdzie } l = \mathtt{newloc}(s) | \quad \mbox{ gdzie } l = \mathtt{newloc}(s)</math> | ||
</math> | |||
</div></div> | </div></div> | ||
| Linia 396: | Linia 385: | ||
<math> | <math> | ||
I \, ::= \,\, | I \, ::= \,\, | ||
\ | \ldots \,\,|\,\, | ||
\mathbf{throw}\, x \,\,|\,\, | \mathbf{throw}\, x \,\,|\,\, | ||
\,\mathbf{try}\, I_1 \,\mathbf{catch}\, exc\, I_2 | \,\mathbf{try}\, I_1 \,\mathbf{catch}\, exc\, I_2 | ||
| Linia 410: | Linia 399: | ||
Instrukcja <math>I = \,\mathbf{try}\, I_1 \,\mathbf{catch}\, exc\, I_2</math> wykonuje <math>I_1</math>. | Instrukcja <math>I = \,\mathbf{try}\, I_1 \,\mathbf{catch}\, exc\, I_2</math> wykonuje <math>I_1</math>. | ||
Jeśli podczas wykonania <math>I_1</math> zostanie podniesiony wyjątek <math>x</math>, i <math>exc = x</math> albo <math>exc = \mathbf{any}</math>, to następuje przerwanie <math>I_1</math> i sterowanie zostaje przeniesione do <math>I_2</math> (następuje ''obsługa wyjątku''). | Jeśli podczas wykonania <math>I_1</math> zostanie podniesiony wyjątek <math>x</math>, i <math>exc = x</math> albo <math>exc = \mathbf{any}</math>, to następuje przerwanie <math>I_1</math> i sterowanie zostaje przeniesione do <math>I_2</math> (następuje ''obsługa wyjątku''). | ||
Jeśli zaś podczas wykonania <math>I_1</math> zostanie podniesiony wyjątek <math>x</math> oraz <math>exc \neq x</math> i <math>exc \neq \mathbf{any}</math>, to obsługa wyjątku przekazana jest do najbliższej instrukcji <math>\,\mathbf{try}\ | Jeśli zaś podczas wykonania <math>I_1</math> zostanie podniesiony wyjątek <math>x</math> oraz <math>exc \neq x</math> i <math>exc \neq \mathbf{any}</math>, to obsługa wyjątku przekazana jest do najbliższej instrukcji <math>\,\mathbf{try}\ </math>, otaczającej <math>I</math>. | ||
Umawiamy się, że <math>\,\mathbf{try}\, I_1 \,\mathbf{catch}\, exc\, I_2</math> ''otacza'' <math>I_1</math> i wszystkie instrukcje wewnątrz <math>I_1</math>, ale ''nie'' otacza <math>I_2</math>. | Umawiamy się, że <math>\,\mathbf{try}\, I_1 \,\mathbf{catch}\, exc\, I_2</math> ''otacza'' <math>I_1</math> i wszystkie instrukcje wewnątrz <math>I_1</math>, ale ''nie'' otacza <math>I_2</math>. | ||
}} | }} | ||
Aktualna wersja na dzień 21:30, 11 wrz 2023
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 ,
Ćwiczenie 1
Rozszerzamy język TINY następująco:
Znaczenie instrukcji jest następujące. Obliczamy wartości wyrażeń i . Jeśli pierwsza z nich jest mniejsza od lub równa drugiej, podstawiamy pierwszą wartość (wartość wyrażenia ) na zmienną i uruchamiamy . Jeśli w nie zostanie napotkana instrukcja , kończymy instrukcję , i przyracamy wartość zmiennej sprzed tej instrukcji. Natomiast jeśli w zostanie napotkana instrukcja , podstawiamy na kolejną, o jeden większą wartość, przywracamy wartości wszystkich pozostałych zmiennych sprzed instrukcji , i ponownie wykonujemy . Powtarzamy w ten sposób, aż zakończy się nie napotkawszy , albo wartość zmiennej przekroczy wartość wyrażenia obliczoną na początku. W pierwszym przypadku kończymy instrukcję , i przyracamy wartość zmiennej sprzed tej instrukcji. W drugim przywracamy wartości wszystkich zmiennych sprzed instrukcji , i uruchamiamy .
Przykład
Oto przykładowy program:
x := 0; y := 1; , x := 1 , 5 , y := y+1; , x <= 4 , z:= x
Wartości zmiennych po zakończeniu programu to: .
Rozwiązanie
Semantyka naturalna bloków
Ćwiczenie 2 (bloki i deklaracje zmiennych)
Rozszerz semantykę języka TINY o deklarację zmiennej:
Zasięgiem zmiennej jest instrukcja , czyli wnętrze bloku, w którym jest zadeklarowana. Zakładamy zwykłe (statyczne) reguły widoczności, przesłaniania, itp.
Rozwiązanie
Zadania domowe
Ćwiczenie 1
Napisz semantykę naturalną dla następującego rozszerzenia języka TINY:
Instrukcja oznacza podniesienie wyjątku o nazwie . Instrukcja wykonuje . Jeśli podczas wykonania zostanie podniesiony wyjątek , i albo , to następuje przerwanie i sterowanie zostaje przeniesione do (następuje obsługa wyjątku). Jeśli zaś podczas wykonania zostanie podniesiony wyjątek oraz i , to obsługa wyjątku przekazana jest do najbliższej instrukcji , otaczającej . Umawiamy się, że otacza i wszystkie instrukcje wewnątrz , ale nie otacza .
Ć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.
