Semantyka i weryfikacja programów/Ćwiczenia 5: Różnice pomiędzy wersjami

Wersja z 08:35, 11 sie 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:

$I : : = \dots | 𝐟 𝐨 𝐫 x = e_{1} 𝐭 𝐨 e_{2} 𝐭 𝐫 𝐲 I_{1} 𝐞 𝐥 𝐬 𝐞 I_{2} | 𝐟 𝐚 𝐢 𝐥$

Znaczenie instrukcji $𝐟 𝐨 𝐫 x = e_{1} 𝐭 𝐨 e_{2} 𝐭 𝐫 𝐲 I_{1} 𝐞 𝐥 𝐬 𝐞 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 $𝐟 𝐚 𝐢 𝐥$ , kończymy instrukcję $𝐟 𝐨 𝐫$ i przyracamy wartość zmiennej $x$ sprzed tej instrukcji. Natomiast jeśli w $I_{1}$ zostanie napotkana instrukcja $𝐟 𝐚 𝐢 𝐥$ , podstawiamy na $x$ kolejną, o jeden większą wartość, przywracamy wartości wszystkich pozostałych zmiennych sprzed instrukcji $𝐟 𝐨 𝐫$ , i ponownie wykonujemy $I_{1}$ . Powtarzamy w ten sposób aż $I_{1}$ zakończy się nie napotkawszy $𝐟 𝐚 𝐢 𝐥$ , albo wartość zmiennej $x$ przekroczy wartość wyrażenia $e_{2}$ obliczoną na początku. W pierwszym przypadku kończymy instrukcję $𝐟 𝐨 𝐫$ i przyracamy wartość zmiennej $x$ sprzed tej instrukcji. W drugim przywracamy wartości wszystkich zmiennych sprzed instrukcji $𝐟 𝐨 𝐫$ i uruchamiamy $I_{2}$ .

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: $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 | 𝐛 𝐞 𝐠 𝐢 𝐧 𝐯 𝐚 𝐫 x = e; I 𝐞 𝐧 𝐝$

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 }

$e x c : : = x | 𝐚 𝐧 𝐲$

Instrukcja $𝐭 𝐡 𝐫 𝐨 𝐰 x$ oznacza podniesienie wyjątku o nazwie $x$ . Instrukcja $I = 𝐭 𝐫 𝐲 I_{1} 𝐜 𝐚 𝐭 𝐜 𝐡 e x c I_{2}$ wykonuje $I_{1}$ . Jeśli podczas wykonania $I_{1}$ zostanie podniesiony wyjątej $x$ , i $e x c = x$ albo $e x c = 𝐚 𝐧 𝐲$ , 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 $e x c \neq x$ i $e x c \neq 𝐚 𝐧 𝐲$ , to obsługa wyjątku przekazana jest do najbliższej instrukcji $𝐭 𝐫 𝐲$ otaczającej $I$ . Umawiamy się, że $𝐭 𝐫 𝐲 I_{1} 𝐜 𝐚 𝐭 𝐜 𝐡 e x c 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.

Semantyka i weryfikacja programów/Ćwiczenia 5: Różnice pomiędzy wersjami

Wersja z 08:35, 11 sie 2006

Spis treści

Zawartość

Semantyka naturalna pewnej instrukcji $𝐟 𝐨 𝐫$

Semantyka naturalna bloków

Zadania domowe

Menu nawigacyjne

Działania na stronie

Opcje strony

Narzędzia osobiste

Nawigacja

Szukaj

Narzędzia

@@ Linia 3: / Linia 3: @@
 == Zawartość ==
-Kontynuujemy ćwiczenie semantyki naturalnej,
+Kontynuujemy ćwiczenie semantyki naturalnej, dodając pewne konstrukcje do języka Tiny.
-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
+Po raz pierwszy roszdzielimy informację przechowywaną w konfiguracji na ''środowisko'' określające wiązanie identyfikatorów i ''stan'' przechowujący wartości zmiennych.
-na ''środowisko'' określające wiązanie identyfikatorów i ''stan''
-przechowujący wartości zmiennych.
 Będzie to przygotowanie do kolejnych zajęć.
@@ Linia 27: / Linia 24: @@
 </math>
-Znaczenie instrukcji <math>\mathbf{for}\, x = e_1 \,\mathbf{to}\, e_2 \,\mathbf{try}\, I_1 \,\mathbf{else}\, I_2</math>
+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.
-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 od drugiej, to 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
+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>
-z nich jest mniejsza lub równa od drugiej, to 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>
 sprzed tej instrukcji.
-Natomiast jeśli w <math>I_1</math> zostanie napotkana instrukcja <math>\mathbf{fail}</math>,
+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
-podstawiamy na <math>x</math> kolejną, o jeden większą wartość,
+pozostałych zmiennych sprzed instrukcji <math>\mathbf{for}\,</math>, i ponownie wykonujemy <math>I_1</math>.
-przywracamy wartości wszystkich
+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.
-pozostałych zmiennych sprzed instrukcji <math>\mathbf{for}\,</math>, i ponownie
+W pierwszym przypadku kończymy instrukcję <math>\mathbf{for}\,</math> i przyracamy wartość zmiennej <math>x</math> sprzed tej instrukcji.
-wykonujemy <math>I_1</math>.
+W drugim przywracamy wartości wszystkich zmiennych sprzed instrukcji <math>\mathbf{for}\,</math> i uruchamiamy <math>I_2</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.
-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>.
 }}
@@ Linia 56: / Linia 41: @@
   x := 0; y := 1;
-  <math>\mathbf{for}\,</math> x := 1 \,\mathbf{to}\, 5 <math>\,\mathbf{try}\,</math>
+  <math>\mathbf{for}\,</math> x := 1 <math>\,\mathbf{to}\,</math> 5 <math>\,\mathbf{try}\,</math>
     y := y+1;
     <math>\mathbf{if}\,</math> x <= 4 <math>\,\mathbf{then}\, \mathbf{fail} \,\mathbf{else}\,</math> z:= x
@@ Linia 63: / Linia 48: @@
 Wartości zmiennych po zakończeniu programu to: <math>x = 0, y = 2, z = 5</math>.
@@ Linia 76: / Linia 60: @@
 </math>
-Zacznijmy od najprostszego przypadku, gdy nie ma wogóle potrzeby
+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>:
-uruchamiania instrukcji wewnętrznej <math>I_1</math>, ponieważ
-wartość wyrażenia <math>e_1</math> jest większa od <math>e_2</math>:
 <math>
@@ Linia 90: / Linia 72: @@
 </math>
-Po prostu uruchamiamy instrukcję <math>I_2</math> w stanie <math>s</math>, ignorując
+Po prostu uruchamiamy instrukcję <math>I_2</math> w stanie <math>s</math>, ignorując <math>I_1</math>.
-<math>I_1</math>.
-Kolejny nietrudny przypadek to sytuacja, w której
+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>.
-<math>n_1 \leq n_2</math> a wykonanie instrukcji wewnętrznej <math>I_1</math>
+Oto reguła dla tego przypadku:
-kończy się sukcesem, tzn. nie następuje wywołanie instrukcji
-<math>\mathbf{fail}</math>. Oto reguła dla tego przypadku:
 <math>
@@ Linia 108: / Linia 87: @@
 </math>
-Tym razem uruchamiamy instrukcję <math>I_1</math>, podstawiając
+Tym razem uruchamiamy instrukcję <math>I_1</math>, podstawiając na zmienną <math>x</math> wartość <math>n_1</math>.
-pod 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>
+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>.
-a wykonanie instrukcji <math>I_1</math> zakończyło się
+Aby poprawnie opisać takie zdarzenie, potrzebujemy dodatkowych tranzycji postaci:
-wykonaniem instrukcji <math>\mathbf{fail}</math> gdzieś wewnątrz <math>I_1</math>.
-Aby poprawnie opisać takie zdarzenie, potrzebujemy dodatkowych
-tranzycji postaci:
 <math>
@@ Linia 123: / Linia 97: @@
 </math>
-Mówiąc formalnie, poszerzamy zbiór konfiguracji o jeden element
+Mówiąc formalnie, poszerzamy zbiór konfiguracji o jeden element <math>\mbox{było-}\mathbf{fail}</math>.
-<math>\mbox{było-}\mathbf{fail}</math>.
 Zauważmy, że po prawej stronie tranzycji nie ma wogóle stanu.
-Nie potrzebujemy go dla opisania semantyki instrukcji <math>\mathbf{for}\,</math>:
+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>.
-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
 <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>
+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 instrukcj <math>\mathbf{for}\,</math>.
-na zmienną <math>x</math> i spróbować ponownie wykonać
+I powtarzać ten schemat aż do skutku, tzn. aż do mementu, gdy zaistnieje któraś z poprzednich dwóch (prostych) sytuacji.
-<math>I_1</math> przy wartościach wszystkich pozostałych
-zmiennych takich, jak na początku instrukcji <math>\mathbf{for}\,</math>.
-I powtarzać ten schemat aż do skutku, tzn. aż do mementu,
-gdy zaistnieje któraś z poprzednich dwóch (prostych) sytuacji.
 Oto odpowiednia reguła:
@@ Linia 154: / Linia 120: @@
 </math>
-Zwróćmy uwagę na pewnien niezwykle istotny szczegół: po zakończeniu
+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>.
-wykonania instrukcji <math>\mathbf{for}\, x = e_1 + 1 \,\mathbf{to}\, e_2 \,\mathbf{try}\, I_1 \,\mathbf{else}\, I_2</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.
-otrzymujemy stan <math>s'</math>, w którym '''nie przywracamy''' wartości
+Dlaczego? Dlatego, że nie wiemy tak naprawdę, czy powinniśmy przywracać wartość zmiennej <math>x</math> czy nie.
-zmiennej <math>x</math>. Gdybyśmy tak zrobili, tzn. gdybyśmy zastąpili <math>s'
+Jeśli ostatecznie nasza instrukcja <math>\mathbf{for}\,</math> zakończyla 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), to powinniśmy pozostawić wartość zmiennej <math>x</math> taką, jaka jest ona po zakończeniu <math>I_2</math>.
-</math> przez <math>s'[x \mapsto s(x)]</math>, nasze semantyka byłaby
+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).
-niepoprawna. 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> zakończyla
-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),
-to 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).
-Jeszcze jeden drobiazg: zamiast <math>e_1 {+} 1</math> w
+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>.
-<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>.
-Na zakończenie prezentujemy reguły niebędne do tego,
+Na zakończenie prezentujemy reguły niebędne do tego, aby wygenerować <math>\mbox{było-}\mathbf{fail}</math>:
-aby wygenerować <math>\mbox{było-}\mathbf{fail}</math>:
 <math>
@@ Linia 189: / Linia 134: @@
 </math>
-oraz aby wystąpienie <math>\mathbf{fail}</math> umiejscowione gdzieś ,,głęboko"
+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>.
-zostało rozpropagowane do najbliższej otaczającej
+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.
-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.
 Oto odpowiednie reguły:
@@ Linia 221: / Linia 162: @@
 </math>
-Widać podobieństwo do analogicznych reguł dla
+Widać podobieństwo do analogicznych reguł dla pętli <math>\mathbf{loop}\, I</math>, którą zajmowaliśmy się na wcześniejszych zajęciach.
-pętli <math>\mathbf{loop}\, I</math>, którą zajmowaliśmy się na wcześniejszych
-zajęciach.
-Zauważmy, że jesli <math>\mathbf{fail}</math> zostało wykonane poza jakąkolwiek
+Zauważmy, że jesli <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>.
-pętlą <math>\mathbf{for}\,</math>, to program ,,zakończy się" w konfiguracji
+Możemy zatem tę właśnie konfigurację uznać za konfigurację końcową, informującą o porażce wykonania programu.
-<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.
 </div></div>
@@ Linia 248: / Linia 184: @@
 </math>
-Zasięgiem zmiennej <math>x</math>  jest instrukcja <math>I</math>
+Zasięgiem zmiennej <math>x</math>  jest instrukcja <math>I</math> czyli wnętrze bloku, w którym jest zadeklarowana.
-czyli wnętrze bloku, w którym jest zadeklarowana.
 Zakładamy zwykłe (statyczne) reguły widoczności, przesłaniania, itp.
 }}
@@ Linia 258: / Linia 193: @@
 <div class="mw-collapsible mw-made=collapsible mw-collapsed"><div class="mw-collapsible-content" style="display:none">
-'''Rozwiązanie 1 (tylko stan)'''
+'''Wariant 1 (tylko stan)'''
 <br>
-Oczywiście powinniśmy odróżniać zmienne zadeklarowane (i zarazem
+Oczywiście powinniśmy odróżniać zmienne zadeklarowane (i zarazem zainicjowane) od tych niezadeklarowanych.
-zainicjowane) od tych niezadeklarowanych.
 Zatem przyjmijmy, że
 <math>\mathbf{State} = \mathbf{Var} \to_{\mathrm{fin}} \mathbf{Num}</math>.
-Zachowujemy wszystkie reguły semantyczne dla języka Tiny
+Zachowujemy wszystkie reguły semantyczne dla języka Tiny i dodajemy jedną nową:
-i dodajemy jedną nową:
 <math>
@@ Linia 275: / Linia 208: @@
 </math>
-mówiącą, że instrukcja wewnętrzna <math>I</math> ewaluowana jest
+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>.
-w stanie, w którym dodatkowo zaznaczono 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).
-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>  pozostaje w stanie nawet po wyjściu z bloku
-(,,wycieka" z bloku).
 Musimy dodać ,,dealokację" zmiennej <math>x</math>:
@@ Linia 289: / Linia 218: @@
 </math>
-I znów napotykamy podobnie trudności jak na wcześniejszych zajęciach:
+I znów napotykamy podobnie trudności jak na wcześniejszych zajęciach: powyższa reguła nie obejmuje przypadku, gdy <math>s(x)</math> jest nieokreślone.
-powyższa reguła nie obejmuje przypadku, gdy <math>s(x)</math> jest
+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.
-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.
 <br>
-'''Rozwiązanie 2 (stan i środowisko)'''
+'''Wariant 2 (stan i środowisko)'''
 <br>
-Podstawowy pomysł polega na rozdzielenie informacji przechowywanej
+Podstawowy pomysł polega na rozdzieleniu informacji przechowywanej dotychczas w stanie, czyli odwzorowania nazw zmiennych w wartości, na dwa ,,etapy".
-dotychczas w stanie na dwa ,,etapy".
+Pierwszy z nich odwzorowuje identyfikatory zmiennych w ''lokacje'', a drugi lokacje w wartości.
-Pierwszy z nich, odwzorowuje identyfikatory zmiennych na ''lokacje'', a drugi
+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:
-lokacje na 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:
 <math>
@@ Linia 318: / Linia 239: @@
 </math>
-Dla jednoznaczności używamy innej nazwy (<math>\mathbf{Store}</math>) ale będziemy
+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.
-zwykle używać symbolu <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
+przechowywana jest wartość danej zmiennej a stan opisuje właśnie zawartość używanych lokacji.
-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.
-Zakładamy przy tym, że mamy do dyspozycji nieskończony zbiór
+Zakładamy przy tym, że mamy do dyspozycji nieskończony zbiór lokacji <math>\mathbf{Loc} = \{ l_0, l_1, \ldots \}</math> i że w każdym momencie tylko skończenie wiele spośród nich jest wykorzystywane.
-lokacji <math>\mathbf{Loc} = \{ l_0, l_1, \ldots \}</math> i że
-w każdym momencie tylko skończenie wiele spośród nich jest
-wykorzystywane.
 Formalnie mowiąc, dziedzina funkcji częściowej <math>s</math> jest zawsze skończona.
 Daje nam to pewność, że zawsze jest jakaś nieużywana lokacja.
-Środowisko początkowe, w którym uruchamiany
+Środowisko początkowe, w którym uruchamiany będzie program, będzie z reguły puste.
-będzie program, będzie z reguły puste.
+Ponadto obraz funkcji częściowej <math>E</math> będzie zawsze zawarty w zbiorze aktualnie używanych lokacji, czyli zawarty w dziedzinie funkcji częściowej <math>s</math>, oznaczanej <math>\mathrm{dom}(s)</math>.
-Ponadto obraz funkcji częściowej <math>E</math>
-będzie zawsze zawarty w zbiorze aktualnie używanych lokacji,
-czyli zawarty w dziedzinie funkcji częściowej <math>s</math>, oznaczanej
-<math>\mathrm{dom}(s)</math>.
-Pożytek z tego podziału na dwa etapy będzie taki, że
+Pożytek z tego podziału na dwa etapy będzie taki, że będziemy umieli łatwo i elastycznie opisywać deklaracje zmiennych, przesłanianie identyfikatorów, itp.
-będziemy umieli łatwo i elastycznie opisywać deklaracje zmiennych,
-przesłanianie identyfikatorów, itp.
 Tranzycje będą teraz postaci:
@@ Linia 348: / Linia 257: @@
 </math>
-czyli instrukcja <math>I</math> będzie modyfikować stan ale nie będzie
+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:
-zmieniać środowiska <math>E</math>. Dla czytelności będziemy zapisywać
-nasze reguły w następujący sposób:
 <math>
@@ Linia 357: / Linia 264: @@
 podkreślając w ten sposób, że środowisko nie ulega zmianie.
-Ale należy pamiętać, że konfiguracja, w której ,,uruchamiamy"
+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>.
-instrukcję <math>I</math> składa się naprawdę z pary <math>(E, s)</math>.
-Deklarując nową zmienną <math>x</math> dodamy po prostu do <math>E</math> parę
+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ą.
-<math>(x, l)</math>, gdzie <math>l</math> jest nową, nieużywaną dotychczas lokacją.
 Dla wygody zapisu załóżmy, że mamy do dyspozycji funkcję
-funkcję
 <math>
@@ Linia 384: / Linia 288: @@
 </math>
-Zauważmy, że stan <math>s'</math> po zakończeniu instrukcji
+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.
-<math>\mathbf{begin}\, \mathbf{var}\, x=e;\, I \,\mathbf{end}</math> zawiera informację o zmiennej
+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.
-lokalnej <math>x</math>, tzn. <math>s(l)</math> jest określone.
-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.
@@ Linia 402: / Linia 301: @@
 </math>
-Reguła ta  uzmysławia nam różnicę pomiędzy środowiskiem a stanem:
+Reguła ta  uzmysławia nam różnicę pomiędzy środowiskiem a stanem: środowisko pozostaje to samo, gdy przechodzimy od jednej instrukcji do następnej, a stan oczywiście ewoluuje wraz ze zmieniającymi się wartościami zmiennych.
-środowisko pozostaje to samo, gdy przechodzimy od jednej instrukcji do
-następnej, a stan oczywiście ewoluuje wraz ze zmieniającymi się
-wartościami zmiennych.
-Reguły dla przypisania, instrukcji warunkowej i pętli
+Reguły dla przypisania, instrukcji warunkowej i pętli nie przedstawiają żadnych nowych trudności.
-nie przedstawiają żadnych nowych trudności.
 Musimy tylko najpierw ustalić postać reguł dla wyrażeń:
@@ Linia 415: / Linia 310: @@
 </math>
-która jest zupełnie naturalna w naszym podejściu opartym o środowiska
+która jest zupełnie naturalna w naszym podejściu opartym o środowiska i stany.
-i stany.
 Reguły mogą wyglądać np. tak:
@@ Linia 453: / Linia 347: @@
 i tak dalej -- pomijamy pozostałe reguły.
 <br>
-'''Wariant (dealokacja)'''
+'''Wariant 3 (dealokacja)'''
 <br>
@@ Linia 468: / Linia 361: @@
 </math>
-i zastanówmy się, jak ,,posprzątać" po zakończeniu wykonania bloku,
+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ż potrzebne.
-tzn. zwolnić lokację <math>l</math>, która była używana tylko w tym bloku
+Oznaczałoby to przywrócenie lokacji <math>l</math> do puli wolnych (nieużywanych) lokacji.
-i w związku z tym nie będzie już potrzebne.
-Oznaczałoby to przywrócenie lokacji <math>l</math> do puli wolnych
-(nieużywanych) lokacji.
 Zmodyfikowana reguła dla instrukcji bloku powinna wyglądać mniej więcej tak:
@@ Linia 484: / Linia 374: @@
 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
+Powinniśmy po prostu przywrócić nieokreśloność stanu dla lokacji <math>l</math>.
-<math>l</math>.
 Natomiast oczywiście nie ma potrzeby dealokownia środowiska!
 Oto rozwiązanie:
@@ Linia 493: / Linia 382: @@
        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)) \}}
-\quad \mbox{ gdzie } l = \mathtt{newloc}(s)
+\quad \mbox{ gdzie } l = \mathtt{newloc}(s).
 </math>
@@ Linia 504: / Linia 393: @@
 {{cwiczenie|1|cw1.dom|
-Napisz semantykę naturalną dla następującego
+Napisz semantykę naturalną dla następującego rozszerzenia języka Tiny:
-rozszerzenia języka Tiny:
 <math>
@@ Linia 522: / Linia 410: @@
 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>.
-Jeśli podczas wykonania <math>I_1</math> zostanie podniesiony wyjątej <math>x
+Jeśli podczas wykonania <math>I_1</math> zostanie podniesiony wyjątej <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'').
-</math>, i <math>exc = x</math> albo <math>exc = \mathbf{any}</math>, to następuje przerwanie <math>
+Jeśli zaś podczas wykonania <math>I_1</math> zostanie podniesiony wyjątej <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>.
-I_1</math> i sterowanie zostaje przeniesione do <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>.
-(następuje ''obsługa wyjątku'').
-Jeśli zaś podczas wykonania <math>I_1</math> zostanie podniesiony wyjątej <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>.
 }}
@@ Linia 538: / Linia 418: @@
 {{cwiczenie|2|cw2.dom|
-Zaproponuj modyfikację semantyki, w której deklaracja
+Zaproponuj modyfikację semantyki, w której deklaracja jest wykonywana ,,równolegle", analogicznie do przypisania równoległego.
-jest wykonywana ,,równolegle", analogicznie do przypisania
+Przy takiej semantyce kolejność poszczególnych deklaracji powinna być nieistotna.
-równoległego. Przy takiej semantyce kolejność poszczególnych
-deklaracji powinna być nieistotna.
 }}

Semantyka i weryfikacja programów/Ćwiczenia 5: Różnice pomiędzy wersjami

Wersja z 08:35, 11 sie 2006

Zawartość

Semantyka naturalna pewnej instrukcji 𝐟𝐨𝐫

Semantyka naturalna bloków

Zadania domowe

Menu nawigacyjne

Szukaj

Semantyka naturalna pewnej instrukcji $𝐟 𝐨 𝐫$