Semantyka i weryfikacja programów/Ćwiczenia 5: Różnice pomiędzy wersjami
Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
Nie podano opisu zmian |
Nie podano opisu zmian |
||
| Linia 1: | Linia 1: | ||
== Zawartość == | == Zawartość == | ||
Kontynuujemy ćwiczenie semantyki naturalnej, dodając pewne konstrukcje do języka | Kontynuujemy ćwiczenie semantyki naturalnej, dodając pewne konstrukcje do języka TINY. | ||
W szczególności rozszerzymy go o deklaracje zmiennych (bloki). | 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. | Po raz pierwszy roszdzielimy informację przechowywaną w konfiguracji na ''środowisko'' określające wiązanie identyfikatorów i ''stan'' przechowujący wartości zmiennych. | ||
| Linia 15: | Linia 14: | ||
Rozszerzamy język | Rozszerzamy język TINY następująco: | ||
<math> | <math> | ||
| Linia 25: | Linia 24: | ||
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 lub równa | 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}\,</math> i przyracamy wartość zmiennej <math>x</math> | 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}\,</math> | 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}\,</math> i przyracamy wartość zmiennej <math>x</math> sprzed tej instrukcji. | 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}\,</math> i uruchamiamy <math>I_2</math>. | W drugim przywracamy wartości wszystkich zmiennych sprzed instrukcji <math>\mathbf{for}\,</math> i uruchamiamy <math>I_2</math>. | ||
| Linia 74: | Linia 73: | ||
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>. | ||
Kolejny nietrudny przypadek to sytuacja, w której <math>n_1 \leq n_2</math> a wykonanie instrukcji wewnętrznej <math>I_1</math> kończy się sukcesem, tzn. nie następuje wywołanie instrukcji <math>\mathbf{fail}</math>. | Kolejny nietrudny przypadek to sytuacja, w której <math>n_1 \leq n_2</math>, a wykonanie instrukcji wewnętrznej <math>I_1</math> kończy się sukcesem, tzn. nie następuje wywołanie instrukcji <math>\mathbf{fail}</math>. | ||
Oto reguła dla tego przypadku: | Oto reguła dla tego przypadku: | ||
| Linia 90: | Linia 89: | ||
Zwróćmy uwagę, że po zakończeniu <math>I_1</math> przywracamy wartość zmiennej <math>x</math> sprzed jej wykonania. | Zwróćmy uwagę, że po zakończeniu <math>I_1</math> przywracamy wartość zmiennej <math>x</math> sprzed jej wykonania. | ||
Pozostał nam trzeci przypadek, gdy <math>n_1 \leq n_2</math> a wykonanie instrukcji <math>I_1</math> zakończyło się wykonaniem instrukcji <math>\mathbf{fail}</math> gdzieś wewnątrz <math>I_1</math>. | Pozostał nam trzeci przypadek, gdy <math>n_1 \leq n_2</math>, a wykonanie instrukcji <math>I_1</math> zakończyło się wykonaniem instrukcji <math>\mathbf{fail}</math> gdzieś wewnątrz <math>I_1</math>. | ||
Aby poprawnie opisać takie zdarzenie, potrzebujemy dodatkowych tranzycji postaci: | Aby poprawnie opisać takie zdarzenie, potrzebujemy dodatkowych tranzycji postaci: | ||
| Linia 104: | Linia 103: | ||
<math>I_1, s[x \mapsto n_1] \,\longrightarrow\, \mbox{było-}\mathbf{fail}.</math> | <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 | 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. | |||
Oto odpowiednia reguła: | Oto odpowiednia reguła: | ||
| Linia 122: | Linia 121: | ||
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}\,</math> | 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 | 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). | ||
Jeszcze jeden drobiazg: zamiast <math>e_1 {+} 1</math> w <math>\mathbf{for}\, x = e_1 + 1 \,\mathbf{to}\, e_2 \,\mathbf{try}\, I_1 \,\mathbf{else}\, I_2, s \,\longrightarrow\, s'</math> w regule powyżej, moglibyśmy podstawić policzoną już wartość, czyli <math>n_1 {+} 1</math>. | Jeszcze jeden drobiazg: zamiast <math>e_1 {+} 1</math> w <math>\mathbf{for}\, x = e_1 + 1 \,\mathbf{to}\, e_2 \,\mathbf{try}\, I_1 \,\mathbf{else}\, I_2, s \,\longrightarrow\, s'</math> w regule powyżej, moglibyśmy podstawić policzoną już wartość, czyli <math>n_1 {+} 1</math>. | ||
| Linia 134: | Linia 133: | ||
</math> | </math> | ||
oraz aby wystąpienie <math>\mathbf{fail}</math> umiejscowione gdzieś | 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 163: | ||
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 | 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 176: | Linia 175: | ||
{{cwiczenie|2 (bloki i deklaracje zmiennych)|cw2| | {{cwiczenie|2 (bloki i deklaracje zmiennych)|cw2| | ||
Rozszerz semantykę języka | Rozszerz semantykę języka TINY o deklarację zmiennej: | ||
<math> | <math> | ||
| Linia 184: | Linia 183: | ||
</math> | </math> | ||
Zasięgiem zmiennej <math>x</math> | Zasięgiem zmiennej <math>x</math> jest instrukcja <math>I</math>, czyli wnętrze bloku, w którym jest zadeklarowana. | ||
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 209: | Linia 208: | ||
mówiącą, że instrukcja wewnętrzna <math>I</math> ewaluowana jest w stanie, w którym dodatkowo zaznaczono wartość zmiennej <math>x</math> równą wartości, do której oblicza się <math>e</math>. | mówiącą, że instrukcja wewnętrzna <math>I</math> ewaluowana jest w stanie, w którym dodatkowo zaznaczono wartość zmiennej <math>x</math> równą wartości, do której oblicza się <math>e</math>. | ||
Oczywiście takie rozwiązanie jest niepoprawne, gdyż wartość zmiennej <math>x</math> | Oczywiście takie rozwiązanie jest niepoprawne, gdyż wartość zmiennej <math>x</math> pozostaje w stanie nawet po wyjściu z bloku ("wycieka" z bloku). | ||
Musimy dodać | Musimy dodać "dealokację" zmiennej <math>x</math>: | ||
<math> | <math> | ||
| Linia 218: | Linia 217: | ||
</math> | </math> | ||
I znów napotykamy | I znów napotykamy podobne trudności jak na wcześniejszych zajęciach: powyższa reguła nie obejmuje przypadku, gdy <math>s(x)</math> jest nieokreślone. | ||
I choć moglibyśmy naprawić ten mankament podobnie jak kiedyś(co pozostawiamy Czytelnikowi), istnieje inne, bardzo eleganckie i elastyczne rozwiązanie tego problemu, które teraz omówimy. | I choć moglibyśmy naprawić ten mankament podobnie jak kiedyś (co pozostawiamy Czytelnikowi), istnieje inne, bardzo eleganckie i elastyczne rozwiązanie tego problemu, które teraz omówimy. | ||
<br> | <br> | ||
| Linia 225: | Linia 224: | ||
<br> | <br> | ||
Podstawowy pomysł polega na rozdzieleniu informacji przechowywanej dotychczas w stanie, czyli odwzorowania nazw zmiennych w wartości, na dwa | Podstawowy pomysł polega na rozdzieleniu informacji przechowywanej dotychczas w stanie, czyli odwzorowania nazw zmiennych w wartości, na dwa "etapy". | ||
Pierwszy z nich odwzorowuje identyfikatory zmiennych w ''lokacje'', a drugi lokacje w wartości. | Pierwszy z nich odwzorowuje identyfikatory zmiennych w ''lokacje'', a drugi lokacje w wartości. | ||
Mamy więc ''środowiska'' <math>E \in \mathbf{Env}</math>, będące funkcjami częściowymi z <math>\mathbf{Var}</math> do <math>\mathbf{Loc}</math>, zbioru lokacji: | Mamy więc ''środowiska'' <math>E \in \mathbf{Env}</math>, będące funkcjami częściowymi z <math>\mathbf{Var}</math> do <math>\mathbf{Loc}</math>, zbioru lokacji: | ||
| Linia 239: | Linia 238: | ||
</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. | ||
Intuicyjnie można myśleć o lokacjach w pamięci operacyjnej maszyny. Środowisko zawiera informację o lokacji, w której | Intuicyjnie można myśleć o lokacjach w pamięci operacyjnej maszyny. Środowisko zawiera informację o lokacji, w której | ||
przechowywana jest wartość danej zmiennej a stan opisuje właśnie zawartość używanych lokacji. | przechowywana jest wartość danej zmiennej a stan opisuje właśnie zawartość używanych lokacji. | ||
| Linia 257: | Linia 256: | ||
</math> | </math> | ||
czyli instrukcja <math>I</math> będzie modyfikować stan ale nie będzie zmieniać środowiska <math>E</math>. Dla czytelności będziemy zapisywać nasze reguły w następujący sposób: | czyli instrukcja <math>I</math> będzie modyfikować stan, ale nie będzie zmieniać środowiska <math>E</math>. Dla czytelności będziemy zapisywać nasze reguły w następujący sposób: | ||
<math> | <math> | ||
| Linia 264: | Linia 263: | ||
podkreślając w ten sposób, że środowisko nie ulega zmianie. | podkreślając w ten sposób, że środowisko nie ulega zmianie. | ||
Ale należy pamiętać, że konfiguracja, w której | Ale należy pamiętać, że konfiguracja, w której "uruchamiamy" instrukcję <math>I</math> składa się naprawdę z trójki <math>(I, s, E)</math>. | ||
Deklarując nową zmienną <math>x</math> dodamy po prostu do <math>E</math> parę <math>(x, l)</math>, gdzie <math>l</math> jest nową, nieużywaną dotychczas lokacją. | Deklarując nową zmienną <math>x</math> dodamy po prostu do <math>E</math> parę <math>(x, l)</math>, gdzie <math>l</math> jest nową, nieużywaną dotychczas lokacją. | ||
| Linia 289: | Linia 288: | ||
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. | ||
Ale lokacja <math>l</math> jest | Ale lokacja <math>l</math> jest "nieosiągalna" w środowisku <math>E</math>, gdyż para <math>x \mapsto l</math> została dodana tylko do środowiska, w którym ewaluuje się wnętrze bloku, a środowisko <math>E</math> całego bloku nie jest modyfikowane. | ||
Poniżej przedstawiamy reguły dla pozostałych instrukcji. | Poniżej przedstawiamy reguły dla pozostałych instrukcji. | ||
| Linia 361: | Linia 360: | ||
</math> | </math> | ||
i zastanówmy się, jak | i zastanówmy się, jak "posprzątać" po zakończeniu wykonania bloku, tzn. zwolnić lokację <math>l</math>, która była używana tylko w tym bloku i w związku z tym nie będzie już potrzebna. | ||
Oznaczałoby to przywrócenie lokacji <math>l</math> do puli wolnych (nieużywanych) lokacji. | Oznaczałoby to przywrócenie lokacji <math>l</math> do puli wolnych (nieużywanych) lokacji. | ||
| Linia 373: | Linia 372: | ||
</math> | </math> | ||
gdzie <math>\bar{s}</math> to stan <math>s''</math> | gdzie <math>\bar{s}</math> to stan <math>s''</math> "okrojony" do dziedziny stanu <math>s</math>. | ||
Powinniśmy po prostu przywrócić nieokreśloność stanu dla lokacji <math>l</math>. | Powinniśmy po prostu przywrócić nieokreśloność stanu dla lokacji <math>l</math>. | ||
Natomiast oczywiście nie ma potrzeby dealokownia środowiska! | Natomiast oczywiście nie ma potrzeby dealokownia środowiska! | ||
| Linia 393: | Linia 392: | ||
{{cwiczenie|1|cw1.dom| | {{cwiczenie|1|cw1.dom| | ||
Napisz semantykę naturalną dla następującego rozszerzenia języka | Napisz semantykę naturalną dla następującego rozszerzenia języka TINY: | ||
<math> | <math> | ||
| Linia 410: | Linia 409: | ||
Instrukcja <math>\mathbf{throw}\, x</math> oznacza podniesienie wyjątku o nazwie <math>x</math>. | Instrukcja <math>\mathbf{throw}\, x</math> oznacza podniesienie wyjątku o nazwie <math>x</math>. | ||
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 | 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 | 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>. | ||
}} | }} | ||
| Linia 418: | Linia 417: | ||
{{cwiczenie|2|cw2.dom| | {{cwiczenie|2|cw2.dom| | ||
Zaproponuj modyfikację semantyki, w której deklaracja jest wykonywana | 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. | Przy takiej semantyce kolejność poszczególnych deklaracji powinna być nieistotna. | ||
}} | }} | ||
Wersja z 14:41, 29 wrz 2006
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
{{{3}}}
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
{{{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 }
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.
