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

Wersja z 08:02, 9 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 \,\mathbf{to}\, 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:02, 9 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 1: / Linia 1: @@
-== Zawartość ==
+== 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).
+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''
+na ''¶rodowisko'' okre¶laj±ce wi±zanie identyfikatorów i ''stan''
-przechowujący wartości zmiennych.
+przechowuj±cy warto¶ci zmiennych.
-Będzie to przygotowanie do kolejnych zajęć.
+Bêdzie to przygotowanie do kolejnych zajêæ.
-== Zadania z rozwiązaniami ==
+== Semantyka naturalna pewnej instrukcji <math>\mathbf{for}\,</math> ==
@@ Linia 18: / Linia 18: @@
-Rozszerzamy język Tiny następująco:
+Rozszerzamy jêzyk Tiny nastêpuj±co:
 <math>
@@ Linia 28: / Linia 28: @@
 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
+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ą
+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>.
+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>,
+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>
+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ść,
+podstawiamy na <math>x</math> kolejn±, o jeden wiêksz± warto¶æ,
-przywracamy wartości wszystkich
+przywracamy warto¶ci wszystkich
-pozostałych zmiennych sprzed instrukcji <math>\mathbf{for}\,</math>, i ponownie
+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>,
+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>
+albo warto¶æ zmiennej <math>x</math> przekroczy warto¶æ wyra¿enia <math>e_2</math>
-obliczoną na początku.
+obliczon± na pocz±tku.
 W pierwszym przypadku
-kończymy instrukcję <math>\mathbf{for}\,</math> i przyracamy wartość zmiennej <math>x</math>
+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
+W drugim przywracamy warto¶ci wszystkich zmiennych sprzed instrukcji
 <math>\mathbf{for}\,</math> i uruchamiamy <math>I_2</math>.
 }}
@@ Linia 52: / Linia 52: @@
 {{przyklad|||
-Oto przykładowy program:
+Oto przyk³adowy program:
 }}
   x := 0; y := 1;
   <math>\mathbf{for}\,</math> x := 1 \,\mathbf{to}\, 5 <math>\,\mathbf{try}\,</math>
     y := y+1;
-    <math>\mathbf{if}\,</math> x \leq 4 <math>\,\mathbf{then}\, \mathbf{fail} \,\mathbf{else}\,</math> z:= x
+    <math>\mathbf{if}\,</math> x <= 4 <math>\,\mathbf{then}\, \mathbf{fail} \,\mathbf{else}\,</math> z:= x
   <math>\,\mathbf{else}\, \mathbf{skip}</math>
-Wartości zmiennych po zakończeniu programu to: <math>x = 0, y = 2, z = 5</math>.
+Warto¶ci zmiennych po zakoñczeniu programu to: <math>x = 0, y = 2, z = 5</math>.
@@ Linia 71: / Linia 70: @@
 <div class="mw-collapsible mw-made=collapsible mw-collapsed"><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>
@@ Linia 78: / Linia 77: @@
 Zacznijmy od najprostszego przypadku, gdy nie ma wogóle potrzeby
-uruchamiania instrukcji wewnętrznej <math>I_1</math>, ponieważ
+uruchamiania instrukcji wewnêtrznej <math>I_1</math>, poniewa¿
-wartość wyrażenia <math>e_1</math> jest większa od <math>e_2</math>:
+warto¶æ wyra¿enia <math>e_1</math> jest wiêksza od <math>e_2</math>:
 <math>
@@ Linia 91: / Linia 90: @@
 </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>.
 Kolejny nietrudny przypadek to sytuacja, w której
-<math>n_1 \leq n_2</math> a wykonanie instrukcji wewnętrznej <math>I_1</math>
+<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
+koñczy siê sukcesem, tzn. nie nastêpuje wywo³anie instrukcji
-<math>\mathbf{fail}</math>. Oto reguła dla tego przypadku:
+<math>\mathbf{fail}</math>. Oto regu³a dla tego przypadku:
 <math>
@@ Linia 109: / Linia 108: @@
 </math>
-Tym razem uruchamiamy instrukcję <math>I_1</math>, podstawiając
+Tym razem uruchamiamy instrukcjê <math>I_1</math>, podstawiaj±c
-pod 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
+Zwróæmy uwagê, ¿e po zakoñczeniu <math>I_1</math> przywracamy
-wartość zmiennej <math>x</math> sprzed jej wykonania.
+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ę
+a wykonanie instrukcji <math>I_1</math> zakoñczy³o siê
-wykonaniem instrukcji <math>\mathbf{fail}</math> gdzieś wewnątrz <math>I_1</math>.
+wykonaniem instrukcji <math>\mathbf{fail}</math> gdzie¶ wewn±trz <math>I_1</math>.
-Aby poprawnie opisać takie zdarzenie, potrzebujemy dodatkowych
+Aby poprawnie opisaæ takie zdarzenie, potrzebujemy dodatkowych
 tranzycji postaci:
 <math>
-I, s \,\longrightarrow\, \mbox{było-}\mathbf{fail}.
+I, s \,\longrightarrow\, \mbox{by³o-}\mathbf{fail}.
 </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.
+Zauwa¿my, ¿e po prawej stronie tranzycji nie ma wogóle stanu.
 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
+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''
+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>
+<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ć
+na zmienn± <math>x</math> i spróbowaæ ponownie wykonaæ
-<math>I_1</math> przy wartościach wszystkich pozostałych
+<math>I_1</math> przy warto¶ciach wszystkich pozosta³ych
-zmiennych takich, jak na początku instrukcji <math>\mathbf{for}\,</math>.
+zmiennych takich, jak na pocz±tku instrukcji <math>\mathbf{for}\,</math>.
-I powtarzać ten schemat aż do skutku, tzn. aż do mementu,
+I powtarzaæ ten schemat a¿ do skutku, tzn. a¿ do mementu,
-gdy zaistnieje któraś z poprzednich dwóch (prostych) sytuacji.
+gdy zaistnieje która¶ z poprzednich dwóch (prostych) sytuacji.
-Oto odpowiednia reguła:
+Oto odpowiednia regu³a:
 <math>
@@ Linia 148: / Linia 147: @@
        e_2, s \,\longrightarrow\, n_2
        \quad
-       I_1, s[x \mapsto n_1]  \,\longrightarrow\, \mbox{było-}\mathbf{fail}
+       I_1, s[x \mapsto n_1]  \,\longrightarrow\, \mbox{by³o-}\mathbf{fail}
        \quad
        \mathbf{for}\, x = e_1 + 1 \,\mathbf{to}\, e_2 \,\mathbf{try}\, I_1 \,\mathbf{else}\, I_2, s \,\longrightarrow\, s'}
@@ Linia 155: / Linia 154: @@
 </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
+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'
+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
+</math> przez <math>s'[x \mapsto s(x)]</math>, nasze semantyka by³aby
-niepoprawna. Dlaczego? Dlatego, że nie wiemy tak naprawdę,
+niepoprawna. Dlaczego? Dlatego, ¿e nie wiemy tak naprawdê,
-czy powinniśmy przywracać wartość zmiennej <math>x</math> czy nie.
+czy powinni¶my przywracaæ warto¶æ zmiennej <math>x</math> czy nie.
-Jeśli ostatecznie nasza instrukcja <math>\mathbf{for}\,</math> zakończyla
+Je¶li ostatecznie nasza instrukcja <math>\mathbf{for}\,</math> zakoñczyla
-się przez bezbłędne zakończenie instrukcji <math>I_1</math>
+siê przez bezb³êdne zakoñczenie instrukcji <math>I_1</math>
-(przypadek drugi), to powinniśmy to zrobić;
+(przypadek drugi), to powinni¶my to zrobiæ;
-ale jeśli zakończyła się wykonaniem instrukcji <math>I_2</math>
+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ą,
+to powinni¶my pozostawiæ warto¶æ zmiennej <math>x</math> tak±,
-jaka jest ona po zakończeniu <math>I_2</math>.
+jaka jest ona po zakoñczeniu <math>I_2</math>.
-A zatem w powyższej regule dla przypadku trzeciego
+A zatem w powy¿szej regule dla przypadku trzeciego
-nie przywracamy wartości zmiennej <math>x</math>; jeśli było
+nie przywracamy warto¶ci zmiennej <math>x</math>; je¶li by³o
-to konieczne, to zostało już wykonane ,,głębiej",
+to konieczne, to zosta³o ju¿ wykonane ,,g³êbiej",
-dzięki regule dla przypadku drugiego oraz dzięki temu,
+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>
+¿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>
+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ż
+w regule powy¿ej, mogliby¶my podstawiæ policzon± ju¿
-wartość, czyli <math>n_1 {+} 1</math>.
+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>
-\mathbf{fail}, s \,\longrightarrow\, \mbox{było-}\mathbf{fail}
+\mathbf{fail}, s \,\longrightarrow\, \mbox{by³o-}\mathbf{fail}
 </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
+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
+Je¶li pojawi³ siê <math>\mathbf{fail}</math>, powinni¶my zaniechaæ dalszego
-wykonania instrukcji a w przypadku pętli, powinniśmy
+wykonania instrukcji a w przypadku pêtli, powinni¶my
-zaniechać dalszego iterowania tej pętli.
+zaniechaæ dalszego iterowania tej pêtli.
-Oto odpowiednie reguły:
+Oto odpowiednie regu³y:
 <math>
-\frac{I_1, s \,\longrightarrow\, \mbox{było-}\mathbf{fail}}
+\frac{I_1, s \,\longrightarrow\, \mbox{by³o-}\mathbf{fail}}
-      {I_1;\, I_2, s \,\longrightarrow\, \mbox{było-}\mathbf{fail}}
+      {I_1;\, I_2, s \,\longrightarrow\, \mbox{by³o-}\mathbf{fail}}
 \quad \quad
-\frac{I_1, s \,\longrightarrow\, s' \quad \quad I_2, s' \,\longrightarrow\, \mbox{było-}\mathbf{fail}}
+\frac{I_1, s \,\longrightarrow\, s' \quad \quad I_2, s' \,\longrightarrow\, \mbox{by³o-}\mathbf{fail}}
-      {I_1;\, I_2, s \,\longrightarrow\, \mbox{było-}\mathbf{fail}}
+      {I_1;\, I_2, s \,\longrightarrow\, \mbox{by³o-}\mathbf{fail}}
 </math>
 <math>
-\frac{b, s \,\longrightarrow\, \mathbf{true} \quad \quad I_1, s \,\longrightarrow\, \mbox{było-}\mathbf{fail}}
+\frac{b, s \,\longrightarrow\, \mathbf{true} \quad \quad I_1, s \,\longrightarrow\, \mbox{by³o-}\mathbf{fail}}
-      {\mathbf{if}\, b \,\mathbf{then}\, I_1 \,\mathbf{else}\, I_2, s \,\longrightarrow\, \mbox{było-}\mathbf{fail}}
+      {\mathbf{if}\, b \,\mathbf{then}\, I_1 \,\mathbf{else}\, I_2, s \,\longrightarrow\, \mbox{by³o-}\mathbf{fail}}
 \quad \quad
 \mbox{ i analogicznie gdy } b, s \,\longrightarrow\, \mathbf{false}
@@ Linia 214: / Linia 213: @@
 <math>
-\frac{b, s \,\longrightarrow\, \mathbf{true} \quad \quad I, s \,\longrightarrow\, \mbox{było-}\mathbf{fail}}
+\frac{b, s \,\longrightarrow\, \mathbf{true} \quad \quad I, s \,\longrightarrow\, \mbox{by³o-}\mathbf{fail}}
-      {\mathbf{while}\, b \,\mathbf{do}\, I, s \,\longrightarrow\, \mbox{było-}\mathbf{fail}}
+      {\mathbf{while}\, b \,\mathbf{do}\, I, s \,\longrightarrow\, \mbox{by³o-}\mathbf{fail}}
 \quad \quad
 \frac{b, s \,\longrightarrow\, \mathbf{true} \quad \quad I, s \,\longrightarrow\, s' \quad \quad
-       \mathbf{while}\, b \,\mathbf{do}\, I, s' \,\longrightarrow\, \mbox{było-}\mathbf{fail}}
+       \mathbf{while}\, b \,\mathbf{do}\, I, s' \,\longrightarrow\, \mbox{by³o-}\mathbf{fail}}
-      {\mathbf{while}\, b \,\mathbf{do}\, I, s \,\longrightarrow\, \mbox{było-}\mathbf{fail}}
+      {\mathbf{while}\, b \,\mathbf{do}\, I, s \,\longrightarrow\, \mbox{by³o-}\mathbf{fail}}
 </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
+pêtli <math>\mathbf{loop}\, I</math>, któr± zajmowali¶my siê na wcze¶niejszych
-zajęciach.
+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
+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ę
+<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
+uznaæ za konfiguracjê koñcow±, informuj±c± o pora¿ce
 wykonania programu.
 </div></div>
 }}
+== Semantyka naturalna bloków ==
 {{cwiczenie|2 (bloki i deklaracje zmiennych)|cw2|
-Rozszerz semantykę języka Tiny o deklarację zmiennej:
+Rozszerz semantykê jêzyka Tiny o deklaracjê zmiennej:
 <math>
@@ Linia 246: / Linia 248: @@
 </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.
+Zak³adamy zwyk³e (statyczne) regu³y widoczno¶ci, przes³aniania, itp.
 }}
@@ Linia 256: / Linia 258: @@
 <div class="mw-collapsible mw-made=collapsible mw-collapsed"><div class="mw-collapsible-content" style="display:none">
-'''Rozwiązanie 1 (tylko stan)'''
+'''Rozwi±zanie 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.
-Zatem przyjmijmy, że
+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 273: / Linia 275: @@
 </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>
+w stanie, w którym dodatkowo zaznaczono warto¶æ zmiennej <math>x</math>
-równą wartości, do której oblicza się <math>e</math>.
+równ± warto¶ci, do której oblicza siê <math>e</math>.
-Oczywiście takie rozwiązanie jest niepoprawne, gdyż wartość
+Oczywi¶cie takie rozwi±zanie jest niepoprawne, gdy¿ warto¶æ
-zmiennej <math>x</math>  pozostaje w stanie nawet po wyjściu z bloku
+zmiennej <math>x</math>  pozostaje w stanie nawet po wyj¶ciu z bloku
 (,,wycieka" z bloku).
-Musimy dodać ,,dealokację" zmiennej <math>x</math>:
+Musimy dodaæ ,,dealokacjê" zmiennej <math>x</math>:
 <math>
@@ Linia 287: / Linia 289: @@
 </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
+powy¿sza regu³a nie obejmuje przypadku, gdy <math>s(x)</math> jest
-nieokreślone.
+nieokre¶lone.
-I choć moglibyśmy naprawić ten mankament podobnie jak kiedyś
+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 elastyczne rozwi±zanie tego problemu, które teraz omówimy.
 <br>
-'''Rozwiązanie 2 (stan i środowisko)'''
+'''Rozwi±zanie 2 (stan i ¶rodowisko)'''
 <br>
-Podstawowy pomysł polega na rozdzielenie informacji przechowywanej
+Podstawowy pomys³ polega na rozdzielenie informacji przechowywanej
 dotychczas w stanie na dwa ,,etapy".
 Pierwszy z nich, odwzorowuje identyfikatory zmiennych na ''lokacje'', a drugi
-lokacje na wartości.
+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>
+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 310: / Linia 312: @@
 </math>
-oraz stany, będące teraz funkcjami częściowymi z <math>\mathbf{Loc}</math> do <math>\mathbf{Num}</math>:
+oraz stany, bêd±ce teraz funkcjami czê¶ciowymi z <math>\mathbf{Loc}</math> do <math>\mathbf{Num}</math>:
 <math>
@@ Linia 316: / Linia 318: @@
 </math>
-Dla jednoznaczności używamy innej nazwy (<math>\mathbf{Store}</math>) ale będziemy
+Dla jednoznaczno¶ci u¿ywamy innej nazwy (<math>\mathbf{Store}</math>) ale bêdziemy
-zwykle używać symbolu <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
+Intuicyjnie mo¿na my¶leæ o lokacjach w pamiêci
-operacyjnej maszyny. Środowisko zawiera informację o lokacji, w której
+operacyjnej maszyny. ¦rodowisko zawiera informacjê o lokacji, w której
-przechowywana jest wartość danej zmiennej
+przechowywana jest warto¶æ danej zmiennej
-a stan opisuje właśnie zawartość używanych lokacji.
+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
+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
+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.
+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.
+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>
+Ponadto obraz funkcji czê¶ciowej <math>E</math>
-będzie zawsze zawarty w zbiorze aktualnie używanych lokacji,
+bêdzie zawsze zawarty w zbiorze aktualnie u¿ywanych lokacji,
-czyli zawarty w dziedzinie funkcji częściowej <math>s</math>, oznaczanej
+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,
+bêdziemy umieli ³atwo i elastycznie opisywaæ deklaracje zmiennych,
-przesłanianie identyfikatorów, itp.
+przes³anianie identyfikatorów, itp.
-Tranzycje będą teraz postaci:
+Tranzycje bêd± teraz postaci:
 <math>
@@ Linia 346: / Linia 348: @@
 </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ć
+zmieniaæ ¶rodowiska <math>E</math>. Dla czytelno¶ci bêdziemy zapisywaæ
-nasze reguły w następujący sposób:
+nasze regu³y w nastêpuj±cy sposób:
 <math>
@@ Linia 354: / Linia 356: @@
 </math>
-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 ,,uruchamiamy"
+Ale nale¿y pamiêtaæ, ¿e konfiguracja, w której ,,uruchamiamy"
-instrukcję <math>I</math> składa się naprawdę z pary <math>(E, s)</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ę
+Dla wygody zapisu za³ó¿my, ¿e mamy do dyspozycji funkcjê
-funkcję
+funkcjê
 <math>
@@ Linia 367: / Linia 369: @@
 </math>
-która zwraca jakąś nową, nieużywaną lokację. Formalnie wymagamy, by
+która zwraca jak±¶ now±, nieu¿ywan± lokacjê. Formalnie wymagamy, by
 <math>
@@ Linia 373: / Linia 375: @@
 </math>
-Dla ilustracji popatrzmy na przykładową regułę dla deklaracji.
+Dla ilustracji popatrzmy na przyk³adow± regu³ê dla deklaracji.
 <math>
@@ Linia 382: / Linia 384: @@
 </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
+<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.
+lokalnej <math>x</math>, tzn. <math>s(l)</math> jest okre¶lone.
-Ale lokacja <math>l</math> jest ,,nieosiągalna" w środowisku
+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
+<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
+¶rodowiska, w którym ewaluuje siê wnêtrze bloku, a ¶rodowisko
-<math>E</math> całego bloku nie jest modyfikowane.
+<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.
-Przede wszystkim złożenie sekwencyjne:
+Przede wszystkim z³o¿enie sekwencyjne:
 <math>
@@ Linia 400: / Linia 402: @@
 </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
+¶rodowisko pozostaje to samo, gdy przechodzimy od jednej instrukcji do
-następnej, a stan oczywiście ewoluuje wraz ze zmieniającymi się
+nastêpnej, a stan oczywi¶cie ewoluuje wraz ze zmieniaj±cymi siê
-wartościami zmiennych.
+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ń:
+Musimy tylko najpierw ustaliæ postaæ regu³ dla wyra¿eñ:
 <math>
@@ Linia 413: / Linia 415: @@
 </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.
-Reguły mogą wyglądać np. tak:
+Regu³y mog± wygl±daæ np. tak:
 <math>
@@ Linia 441: / Linia 443: @@
 </math>
-Reguły dla wyrażeń są oczywiste:
+Regu³y dla wyra¿eñ s± oczywiste:
 <math>
@@ Linia 450: / Linia 452: @@
 </math>
-i tak dalej -- pomijamy pozostałe reguły.
+i tak dalej -- pomijamy pozosta³e regu³y.
@@ Linia 457: / Linia 459: @@
 <br>
-Przypomnijmy sobie semantykę bloku
+Przypomnijmy sobie semantykê bloku
 <math>
@@ Linia 466: / Linia 468: @@
 </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
+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.
+i w zwi±zku z tym nie bêdzie ju¿ potrzebne.
-Oznaczałoby to przywrócenie lokacji <math>l</math> do puli wolnych
+Oznacza³oby to przywrócenie lokacji <math>l</math> do puli wolnych
-(nieużywanych) lokacji.
+(nieu¿ywanych) lokacji.
-Zmodyfikowana reguła dla instrukcji bloku powinna wyglądać mniej więcej tak:
+Zmodyfikowana regu³a dla instrukcji bloku powinna wygl±daæ mniej wiêcej tak:
 <math>
@@ Linia 482: / Linia 484: @@
 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>.
-Natomiast oczywiście nie ma potrzeby dealokownia środowiska!
+Natomiast oczywi¶cie nie ma potrzeby dealokownia ¶rodowiska!
-Oto rozwiązanie:
+Oto rozwi±zanie:
 <math>
@@ Linia 500: / Linia 502: @@
-==== Zadanie 1 ====
+{{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 518: / Linia 520: @@
 </math>
-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>.
-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>
+</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'').
+(nastêpuje ''obs³uga wyj±tku'').
-Jeśli zaś podczas wykonania <math>I_1</math> zostanie podniesiony wyjątej <math>x
+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
+</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
+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>
+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>,
+i wszystkie instrukcje wewn±trz <math>I_1</math>,
 ale ''nie'' otacza <math>I_2</math>.
+}}
-==== Zadanie 2 ====
+{{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. Przy takiej semantyce kolejność poszczególnych
+równoleg³ego. Przy takiej semantyce kolejno¶æ poszczególnych
-deklaracji powinna być nieistotna.
+deklaracji powinna byæ nieistotna.
+}}

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

Wersja z 08:02, 9 sie 2006

Zawarto¶æ

Semantyka naturalna pewnej instrukcji 𝐟𝐨𝐫

Semantyka naturalna bloków

Zadania domowe

Menu nawigacyjne

Szukaj

Semantyka naturalna pewnej instrukcji $𝐟 𝐨 𝐫$