Semantyka i weryfikacja programów/Ćwiczenia 5: Różnice pomiędzy wersjami
Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
Nie podano opisu zmian |
m Zastępowanie tekstu – „.↵</math>” na „</math>” |
||
| (Nie pokazano 8 wersji utworzonych przez 2 użytkowników) | |||
| 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 9: | Linia 8: | ||
== Semantyka naturalna pewnej instrukcji <math>\mathbf{for}\ | == Semantyka naturalna pewnej instrukcji <math>\mathbf{for}\ </math>, == | ||
| 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}\ | 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 41: | 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 50: | Linia 49: | ||
<div class="mw-collapsible mw-made=collapsible mw-collapsed"><div class="mw-collapsible-content" style="display:none"> | <div class="mw-collapsible mw-made=collapsible mw-collapsed"> | ||
<span class="mw-collapsible-toogle mw-collapsible-toogle-default style="font-variant:small-caps">Rozwiązanie</span> | |||
<div class="mw-collapsible-content" style="display:none"> | |||
Będziemy posługiwać się jak zwykle tranzycjami postaci: | Będziemy posługiwać się jak zwykle tranzycjami postaci: | ||
<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>. | ||
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 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>. | ||
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: | ||
<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 | 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 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 | 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 129: | ||
</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 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 | 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. | ||
</div></div> | </div></div> | ||
== Semantyka naturalna bloków == | == Semantyka naturalna bloków == | ||
| Linia 176: | Linia 169: | ||
{{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 177: | ||
</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. | ||
}} | }} | ||
<div class="mw-collapsible mw-made=collapsible mw-collapsed"> | |||
<span class="mw-collapsible-toogle mw-collapsible-toogle-default style="font-variant:small-caps">Rozwiązanie</span> | |||
<div class="mw-collapsible mw-made=collapsible mw-collapsed"><div class="mw-collapsible-content" style="display:none"> | <div class="mw-collapsible-content" style="display:none"> | ||
'''Wariant 1 (tylko stan)''' | '''Wariant 1 (tylko stan)''' | ||
| Linia 209: | Linia 202: | ||
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 211: | ||
</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 218: | ||
<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 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. | ||
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 249: | ||
</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 256: | ||
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 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. | ||
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 351: | ||
</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 363: | ||
</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 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> | ||
== Zadania domowe == | == Zadania domowe == | ||
| Linia 393: | Linia 381: | ||
{{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> | ||
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 398: | ||
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 406: | ||
{{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. | ||
}} | }} | ||
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.
