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

Wersja z 08:03, 9 sie 2006

Zawarto¶æ

Ostatnie zajêcia po¶wiêcone semantyce naturalnej. Rozszerzymy jêzyk Tiny o deklaracje zmiennych i procedur z jednym parametrem. Rozwa¿ymy statyczn± i dynamiczn± widoczno¶æ (wi±zanie) identyfikatorów oraz ró¿ne mechanizmy przekazywania parametrów. Pracujemy ze ¶rodowiskami i stanami.

Semantyka naturalna procedur

Ćwiczenie 1 (procedury)

Rozszerzmy jêzyk Tiny o deklaracje i wywo³ania procedur:

$I : : = \dots | 𝐛 𝐞 𝐠 𝐢 𝐧 d; I 𝐞 𝐧 𝐝 | 𝐜 𝐚 𝐥 𝐥 x_{1} (x_{2})$

$d : : = 𝐯 𝐚 𝐫 x = e | 𝐩 𝐫 𝐨 𝐜 x_{1} (x_{2}); I | d_{1}; d_{2}$

Konstrukcja $𝐩 𝐫 𝐨 𝐜 x_{1} (x_{2})$ deklaruje procedurê o nazwie $x_{1}$ , której parametrem formalnym jest $x_{2}$ . Zak³adamy statyczne wi±zanie identyfikatorów i przekazywanie parametrów przez zmienn± (to znaczy, ¿e w momencie wywo³ania procedury, powinna zostaæ przekazana lokacja odpowiadaj±ca parametrowi aktualnemu). Instrukcja $𝐜 𝐚 𝐥 𝐥 x_{1} (x_{2})$ wywo³uje procedurê $x_{1}$ z parametrem aktualnym $x_{2}$ .

Rozwiązanie

{{{3}}}

Ćwiczenie 2 (wi±zanie dynamiczne)

Zastanówmy siê, jakich modyfikacji wymaga nasza semantyka, aby wi±zanie identyfikatorów by³o dynamiczne, zamiast statycznego. Rozumiemy przez to, ¿e w przypadku odwo³ania do zmiennej wewn±trz procedury, odwo³ujemy siê do ¶rodowiska w miejscu wywo³ania tej procedury, zamiast do ¶rodowiska z miejsca deklaracji jak dotychczas. Tak samo powinno byæ w przypadku wywo³ania innej procedury wewn±trz procedury, czyli wi±zanie dynamiczne dotyczy i zmiennych i procedur.

Przykład

Spójrzmy na kilka prostych programów.

 $𝐛 𝐞 𝐠 𝐢 𝐧$ 
   $𝐯 𝐚 𝐫$  x = 1;
   $𝐩 𝐫 𝐨 𝐜$  p(y); y := y+x;

   $𝐛 𝐞 𝐠 𝐢 𝐧$ 
     $𝐯 𝐚 𝐫$  x = 10;  $𝐯 𝐚 𝐫$  z = 0;

     $𝐜 𝐚 𝐥 𝐥$  p(z);
   $𝐞 𝐧 𝐝$ 
 $𝐞 𝐧 𝐝$

Warto¶æ koñcowa zmiennej $z = 10$ . Gdyby wi±zanie zmiennej $x$ by³o statyczne, to warto¶æ ta wynosi³aby $1$ . Podobnie dla procedur:

 $𝐛 𝐞 𝐠 𝐢 𝐧$ 
   $𝐩 𝐫 𝐨 𝐜$  q(x); x := x+1;
   $𝐩 𝐫 𝐨 𝐜$  p(y);  $𝐜 𝐚 𝐥 𝐥$  q(y);  $𝐜 𝐚 𝐥 𝐥$  q(y);

   $𝐛 𝐞 𝐠 𝐢 𝐧$ 
     $𝐩 𝐫 𝐨 𝐜$   $𝐜 𝐚 𝐥 𝐥$ q(x); x := x+x;
     $𝐯 𝐚 𝐫$  z = 2;

     $𝐜 𝐚 𝐥 𝐥$  p(z);
   $𝐞 𝐧 𝐝$ 
 $𝐞 𝐧 𝐝$

Warto¶æ koñcowa zmiennej $z = 8$ . Gdyby widoczno¶æ procedury $q$ by³a statyczna, to warto¶æ ta wynosi³aby $4$ . A oto przyk³ad programu, który nie wykona³by siê poprawnie przy wi±zaniu statycznych, a wykonuje siê poprawnie przy dynamicznym:

 $𝐛 𝐞 𝐠 𝐢 𝐧$ 
   $𝐩 𝐫 𝐨 𝐜$  q(x);  $𝐜 𝐚 𝐥 𝐥$  r(x);
   $𝐩 𝐫 𝐨 𝐜$  p(y);
     $𝐛 𝐞 𝐠 𝐢 𝐧$ 
       $𝐩 𝐫 𝐨 𝐜$  r(x); x := x+x;

       $𝐜 𝐚 𝐥 𝐥$  q(x);
     $𝐞 𝐧 𝐝$ 
   $𝐯 𝐚 𝐫$  z = 7;

   $𝐜 𝐚 𝐥 𝐥$  p(z);
 $𝐞 𝐧 𝐝$

Warto¶æ koñcowa zmiennej $z$ wynosi $14$ . Procedura $p$ wywo³uje procedurê $q$ , ,,przekazuj±c" jej równie¿ ¶rodowisko z miejsca wo³ania, zawieraj±ce informacjê o procedurze $r$ . Ta ostatnia przy widoczno¶ci statycznej by³aby lokalna, a teraz nie jest.

Rozwiązanie

{{{3}}}

Ćwiczenie 3 (ró¿ne mechanizmy przekazywana parametru)

Rozwa¿ inne mechanizmy przekazywania parametru (wi±zanie statyczne):

przez warto¶æ
in-out

Nale¿y wyja¶niæ ostatni mechanizm (in-out). Parametrem aktualnym jest zmienna, której warto¶æ jest przypisywana parametrowi formalnemu (tak jak przy przekazywaniu przez warto¶æ, gdy parametrem aktualnym jest zmienna). Ale po zakoñczeniu procedury, warto¶æ parametru formalnego, która mog³a zmieniæ siê w czasie dzialania procedury, jest spowrotem przypisywana na zmienn± bêd±c± parametrem aktualnym (a wiêc podobnie do przekazywania przez zmienn±). Parametr formalny jest traktowany jak zmienna lokalna procedury.

Rozwiązanie (przekazywanie parametru przez warto¶æ)

{{{3}}}

Rozwiązanie (przekazywanie parametru in-out)

{{{3}}}

Zadania domowe

Ćwiczenie 1

Zaadaptuj semantykê ,,deklaracji równoleg³ych" dla rekurencji wzajemnej wewn±trz jednej deklaracji równoleg³ej. To znaczy, ¿e procedury zadeklarowane w jednej deklaracji równoleg³ej mog± siê wzajemniej wywo³ywaæ bez ¿adnych ograniczeñ.

Ćwiczenie 2

Zamiast procedur, rozwa¿ funkcje z pojedynczym parametrem przekazywanym przez zmienn±. Wywo³anie funkcji mo¿e teraz pojawiæ siê wewn±trz wyra¿enia:

$e : : = \dots | 𝐜 𝐚 𝐥 𝐥 x_{1} (x_{2}) .$

Uwaga na efekty uboczne!

Ćwiczenie 3

Rozwa¿ nastêpuj±ce warianty:

wi±zanie zmiennych jest statyczne a procedur dynamiczne
wi±zanie zmiennych jest dymamiczne a procedur statyczne.

Ćwiczenie 4

Rozszerz semantykê procedur tak, aby parametrem aktualnym procedury mog³a byæ procedura.

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

Wersja z 08:03, 9 sie 2006

Zawarto¶æ

Semantyka naturalna procedur

Zadania domowe

Menu nawigacyjne

Działania na stronie

Opcje strony

Narzędzia osobiste

Nawigacja

Szukaj

Narzędzia

@@ Linia 1: / Linia 1: @@
-== Zawartość ==
+== Zawarto¶æ ==
-Ostatnie zajęcia poświęcone semantyce naturalnej.
+Ostatnie zajêcia po¶wiêcone semantyce naturalnej.
-Rozszerzymy język Tiny o deklaracje zmiennych i procedur z jednym
+Rozszerzymy jêzyk Tiny o deklaracje zmiennych i procedur z jednym
 parametrem.
-Rozważymy statyczną i dynamiczną widoczność (wiązanie)
+Rozwa¿ymy statyczn± i dynamiczn± widoczno¶æ (wi±zanie)
-identyfikatorów oraz różne mechanizmy przekazywania
+identyfikatorów oraz ró¿ne mechanizmy przekazywania
 parametrów.
-Pracujemy ze środowiskami i stanami.
+Pracujemy ze ¶rodowiskami i stanami.
-== Zadania z rozwiązaniami ==
+== Semantyka naturalna procedur ==
 {{cwiczenie|1 (procedury)|cw1|
-Rozszerzmy języka Tiny o deklaracje i wywołania procedur:
+Rozszerzmy jêzyk Tiny o deklaracje i wywo³ania procedur:
 <math>
@@ Linia 33: / Linia 33: @@
 </math>
-Konstrukcja <math>\mathbf{proc}\, x_1(x_2)</math> deklaraje procedurę o nazwie
+Konstrukcja <math>\mathbf{proc}\, x_1(x_2)</math> deklaruje procedurê o nazwie
 <math>x_1</math>, której parametrem formalnym jest <math>x_2</math>.
-Zakładamy statyczne wiązanie identyfikatorów i przekazywanie
+Zak³adamy statyczne wi±zanie identyfikatorów i przekazywanie
-parametrów przez zmienną (to znaczy, że w momencie wywołania
+parametrów przez zmienn± (to znaczy, ¿e w momencie wywo³ania
-procedury, powinna zostać
+procedury, powinna zostaæ
-przekazana lokacja odpowiadająca parametrowi aktualnemu).
+przekazana lokacja odpowiadaj±ca parametrowi aktualnemu).
-Instrukcja <math>\mathbf{call}\, x_1(x_2)</math> wywołuje procedurę <math>x_1</math>
+Instrukcja <math>\mathbf{call}\, x_1(x_2)</math> wywo³uje procedurê <math>x_1</math>
 z parametrem aktualnym <math>x_2</math>.
 }}
@@ Linia 48: / Linia 48: @@
 <div class="mw-collapsible mw-made=collapsible mw-collapsed"><div class="mw-collapsible-content" style="display:none">
-Użyjemu środowisk <math>E \in \mathbf{Env}</math> i stanów <math>s \in \mathbf{Store}</math>:
+U¿yjemu ¶rodowisk <math>E \in \mathbf{Env}</math> i stanów <math>s \in \mathbf{Store}</math>:
 <math>
@@ Linia 58: / Linia 58: @@
 Nowym elementem jest zbiór <math>\mathbf{Proc}</math>, potrzebny nam do
 przechowywania informacji o procedurach.
-Informacja nt procedury, którą musimy przechowywać, to:
+Informacja nt procedury, któr± musimy przechowywaæ, to:
 * nazwa parametru formalnego,
-* ciało procedury (instrukcja <math>I \in \mathbf{Stmt}</math>) oraz
+* cia³o procedury (instrukcja <math>I \in \mathbf{Stmt}</math>) oraz
-* ''środowisko'', w którym procedura została zadeklarowana.
+* ''¶rodowisko'', w którym procedura zosta³a zadeklarowana.
-Zauważmy, że nie musimy (i nie powinniśmy) pamiętać stanu
+Zauwa¿my, ¿e nie musimy (i nie powinni¶my) pamiêtaæ stanu
-z momentu deklaracji, czyli konkretnych wartości zmiennych
+z momentu deklaracji, czyli konkretnych warto¶ci zmiennych
-wówczas zadeklarowanych. Pamiętamy tylko środowisko,
+wówczas zadeklarowanych. Pamiêtamy tylko ¶rodowisko,
-które wyznacza nam ''wiązanie'' identyfikatorów (nazw
+które wyznacza nam ''wi±zanie'' identyfikatorów (nazw
-zmiennych i procedur) występujących w ciele procedury z
+zmiennych i procedur) wystêpuj±cych w ciele procedury z
-lokacjami (lub opisami procedur z <math>\mathbf{Proc}</math>), a więc z konkretnymi
+lokacjami (lub opisami procedur z <math>\mathbf{Proc}</math>), a wiêc z konkretnymi
 zmiennymi (lub procedurami).
-Widać tutaj jasno, jak elegancki i wygodny jest podział na środowisko
+Widaæ tutaj jasno, jak elegancki i wygodny jest podzia³ na ¶rodowisko
 i stan.
@@ Linia 77: / Linia 77: @@
 Czyli znów zbiór <math>\mathbf{Env}</math> zadany jest przez równanie.
-Nasze tranzycje będą następujących postaci:
+Nasze tranzycje bêd± nastêpuj±cych postaci:
 <math>
@@ Linia 91: / Linia 91: @@
 </math>
-Na uwagę zasługuje ostatnia postać tranzycji: deklaracja,
+Na uwagê zas³uguje ostatnia postaæ tranzycji: deklaracja,
-w odróżnieniu od instrukcji, może zmieniać środowisko.
+w odró¿nieniu od instrukcji, mo¿e zmieniaæ ¶rodowisko.
-Umówmy się, że środowisko <math>E'</math> będzie rozszerzało <math>E</math> o informację
+Umówmy siê, ¿e ¶rodowisko <math>E'</math> bêdzie rozszerza³o <math>E</math> o informacjê
 o nowych identyfikatorach, tzn. tych zadeklarowanych w <math>d</math>.
-Zajmijmy się najpierw deklaracjami zmiennych:
+Zajmijmy siê najpierw deklaracjami zmiennych:
 <math>
@@ Linia 114: / Linia 114: @@
 </math>
-Zauważmy, że deklaracja procedury nie zmienia stanu, tylko środowisko,
+Zauwa¿my, ¿e deklaracja procedury nie zmienia stanu, tylko ¶rodowisko,
-w odróżnieniu od deklaracji zmiennej.
+w odró¿nieniu od deklaracji zmiennej.
-W środowisku pamiętamy trójkę <math>\langle x_2, I, E \rangle</math> zawierającą
+W ¶rodowisku pamiêtamy trójkê <math>\langle x_2, I, E \rangle</math> zawieraj±c±
-nazwę parametru formalnego, ciało procedury oraz ''środowisko
+nazwê parametru formalnego, cia³o procedury oraz ''¶rodowisko
 deklaracji procedury''.
-To ostatnie determinuje statyczne wiązanie identyfikatorów:
+To ostatnie determinuje statyczne wi±zanie identyfikatorów:
-wiązanie identyfikatorów występującuch w ciele procedury jest
+wi±zanie identyfikatorów wystêpuj±cuch w ciele procedury jest
-jakby ,,zamrożone'' (ustalone) w momencie deklaracji procedury.
+jakby ,,zamro¿one'' (ustalone) w momencie deklaracji procedury.
-Aby dokończyć semantykę deklaracji potrzebujemy jeszcze jednej reguły:
+Aby dokoñczyæ semantykê deklaracji potrzebujemy jeszcze jednej regu³y:
 <math>
@@ Linia 131: / Linia 131: @@
 </math>
-która opisuje sekwencyjną ,,kumulację" modyfikacji dokonanych w deklaracjach.
+która opisuje sekwencyjn± ,,kumulacjê" modyfikacji dokonanych w deklaracjach.
-'''Pytanie:''' czy kolejność poszczególnych deklaracji ma znaczenie?
+'''Pytanie:''' czy kolejno¶æ poszczególnych deklaracji ma znaczenie?
-Teraz określimy semantykę bloku:
+Teraz okre¶limy semantykê bloku:
 <math>
@@ Linia 144: / Linia 144: @@
 </math>
-Czyli instrukcja wewnętrzna wykonywana jest w środowisku (i stanie)
+Czyli instrukcja wewnêtrzna wykonywana jest w ¶rodowisku (i stanie)
-''wytworzonym'' (rozszerzonym) przez deklarację <math>d</math>.
+''wytworzonym'' (rozszerzonym) przez deklaracjê <math>d</math>.
-Stan końcowy po wykonaniu bloku to po prostu stan końcowy <math>s''</math>
+Stan koñcowy po wykonaniu bloku to po prostu stan koñcowy <math>s''</math>
-po wykonaniu instrukcji wewnętrznej.
+po wykonaniu instrukcji wewnêtrznej.
-Może się to wydawać niepokojące, gdyż oznacza, że nowe lokacje,
+Mo¿e siê to wydawaæ niepokoj±ce, gdy¿ oznacza, ¿e nowe lokacje,
-powołane podczas deklaracji <math>d</math>, zachowują przechowywaną wartość
+powo³ane podczas deklaracji <math>d</math>, zachowuj± przechowywan± warto¶æ
-również po wyjściu z bloku. Na szczęście wykonanie
+równie¿ po wyj¶ciu z bloku. Na szczê¶cie wykonanie
-bloku nie ma wpływu na środowisko, a to ono decyduje, które
+bloku nie ma wp³ywu na ¶rodowisko, a to ono decyduje, które
-identyfikatory są widoczne (zadeklarowane) i ogólniej, które lokacje
+identyfikatory s± widoczne (zadeklarowane) i ogólniej, które lokacje
-są przypisane identyfikatorom. A więc deklaracja <math>d</math>
+s± przypisane identyfikatorom. A wiêc deklaracja <math>d</math>
-nie ma wpływu na środowisko, w którym zostaną wykonane kolejne
+nie ma wp³ywu na ¶rodowisko, w którym zostan± wykonane kolejne
 instrukcje.
-Widać to jasno w regule dla złożenia sekwencyjnego:
+Widaæ to jasno w regule dla z³o¿enia sekwencyjnego:
 <math>
@@ Linia 166: / Linia 166: @@
-Pozostało nam jeszcze określenie semantyki wywołania procedury:
+Pozosta³o nam jeszcze okre¶lenie semantyki wywo³ania procedury:
 <math>
@@ Linia 176: / Linia 176: @@
 </math>
-Czyli uruchamiane jest ciało <math>I</math> procedury,
+Czyli uruchamiane jest cia³o <math>I</math> procedury,
-w środowisku <math>E'</math> z miejsca deklaracji tej procedury
+w ¶rodowisku <math>E'</math> z miejsca deklaracji tej procedury
 zmodyfikowanym o przypisanie <math>x \mapsto l</math>
 lokacji <math>l</math> do parametru formalnego <math>x</math> procedury.
 Stan, w którym uruchomione jest <math>I</math> to po prostu
-stan bieżący z miejsca wołania procedury; o prawidłowe
+stan bie¿±cy z miejsca wo³ania procedury; o prawid³owe
-wiązanie identyfikatorów ,,troszczy" się wyłącznie
+wi±zanie identyfikatorów ,,troszczy" siê wy³±cznie
-środowisko <math>E'</math>.
+¶rodowisko <math>E'</math>.
-'''Pytanie:''' czy powyższa reguła dopuszcza rekurencyjne wywołania procedury?
+'''Pytanie:''' czy powy¿sza regu³a dopuszcza rekurencyjne wywo³ania procedury?
-Okazuje się, że niestety nie, gdyż w środowisku
+Okazuje siê, ¿e niestety nie, gdy¿ w ¶rodowisku
-<math>E'[x \mapsto l]</math> nie ma informacji o procedurze <math>x_1</math>, którą
+<math>E'[x \mapsto l]</math> nie ma informacji o procedurze <math>x_1</math>, któr±
-właśnie wołamy. Może się zdarzyć, że <math>E'[x \mapsto l] \in \mathbf{Proc}</math>, ale
+w³a¶nie wo³amy. Mo¿e siê zdarzyæ, ¿e <math>E'[x \mapsto l] \in \mathbf{Proc}</math>, ale
-oznacza to tylko, że w miejscu deklaracji procedury <math>x_1</math>
+oznacza to tylko, ¿e w miejscu deklaracji procedury <math>x_1</math>
-była już wcześniej (statycznie) zadeklarowana inna procedura
+by³a ju¿ wcze¶niej (statycznie) zadeklarowana inna procedura
 o tej samej nazwie.
-Aby umożliwić rekurencję, powinniśmy zadbać sami o to, aby
+Aby umo¿liwiæ rekurencjê, powinni¶my zadbaæ sami o to, aby
-środowisko, w którym wykonujemy <math>I</math> zawierało informację
+¶rodowisko, w którym wykonujemy <math>I</math> zawiera³o informacjê
 o naszej procedurze:
@@ Linia 205: / Linia 205: @@
 </math>
-Zauważmy, że przypisanie <math>x_1 \mapsto \langle x, I, E' \rangle</math>
+Zauwa¿my, ¿e przypisanie <math>x_1 \mapsto \langle x, I, E' \rangle</math>
-dodane  do <math>E'</math> wystarcza na tylko jedno wywołanie rekurencyjne
+dodane  do <math>E'</math> wystarcza na tylko jedno wywo³anie rekurencyjne
-(licząc w głąb). Ale każde kolejne wywołanie dodaje tę informację,
+(licz±c w g³±b). Ale ka¿de kolejne wywo³anie dodaje tê informacjê,
-czyli każde wywołanie procedury przygotowuje środowisko dla
+czyli ka¿de wywo³anie procedury przygotowuje ¶rodowisko dla
-następnego.
+nastêpnego.
-I to jest wystarczające.
+I to jest wystarczaj±ce.
-'''Pytanie:''' czy możliwa jest rekurencja wzajemna?
+'''Pytanie:''' czy mo¿liwa jest rekurencja wzajemna?
-Pozostaje jeszcze jedna kwestia: dodajemy do środowiska <math>E'</math>
+Pozostaje jeszcze jedna kwestia: dodajemy do ¶rodowiska <math>E'</math>
 dwa przypisania:
 <math>x \mapsto l</math> oraz <math>x_1 \mapsto \langle x, I, E' \rangle</math>,
-ale dlaczego w takiej kolejności.
+ale dlaczego w takiej kolejno¶ci.
-'''Pytanie:''' co się stanie, gdy zamienimy tę kolejność:
+'''Pytanie:''' co siê stanie, gdy zamienimy tê kolejno¶æ:
 <math>
@@ Linia 229: / Linia 229: @@
 </math>
-Czy obydwie semantyki są sobie równoważne?
+Czy obydwie semantyki s± sobie równowa¿ne?
-Okazuje się, że tak nie jest, oto dwa kontrprzykłady:
+Okazuje siê, ¿e tak nie jest, oto dwa kontrprzyk³ady:
@@ Linia 252: / Linia 252: @@
-Każdy z tych programów uruchomi się poprawnie w dokładnie
+Ka¿dy z tych programów uruchomi siê poprawnie w dok³adnie
 jednym z wariantów semantyki.
 '''Pytanie:''' Który w którym?
-Semantyka pozostałych instrukcji i wyrażeń języka Tiny pozostaje bez zmian.
+Semantyka pozosta³ych instrukcji i wyra¿eñ jêzyka Tiny pozostaje bez zmian.
-Rozważmy na koniec problem dealokacji.
+Rozwa¿my na koniec problem dealokacji.
@@ Linia 266: / Linia 266: @@
 <br>
-Chcemy, aby ,,posprzątano" po zakończeniu wykonania bloku,
+Chcemy, aby ,,posprz±tano" po zakoñczeniu wykonania bloku,
-tzn. aby zwolniono te lokacje, które były używane tylko w tym bloku
+tzn. aby zwolniono te lokacje, które by³y u¿ywane tylko w tym bloku
-i w związku z tym nie będą już potrzebne.
+i w zwi±zku z tym nie bêd± ju¿ potrzebne.
-Oznacza to, że powinniśmy przywrócić nieokreśloność stanu dla
+Oznacza to, ¿e powinni¶my przywróciæ nieokre¶lono¶æ stanu dla
-wszystkich tych lokacji, które były użyte podczas deklaracji <math>d</math>.
+wszystkich tych lokacji, które by³y u¿yte podczas deklaracji <math>d</math>.
-Jest wiele możliwości wyrażenia tego dodatkowego warunku,
+Jest wiele mo¿liwo¶ci wyra¿enia tego dodatkowego warunku,
-np. możemy dodać do powyższej reguły
+np. mo¿emy dodaæ do powy¿szej regu³y
 <math>
@@ Linia 283: / Linia 283: @@
 dodatkowy warunek postaci <math>\mbox{ gdzie } \bar{s} = \ldots</math>.
-Proponujemy tu rozwiązanie ciut bardziej eleganckie.
+Proponujemy tu rozwi±zanie ciut bardziej eleganckie.
-Zacznijmy od tranzycji dokonujących dealokacji,
+Zacznijmy od tranzycji dokonuj±cych dealokacji,
-które mogą być np. postaci: <math>s'', L \,\longrightarrow\, \bar{s}</math>.
+które mog± byæ np. postaci: <math>s'', L \,\longrightarrow\, \bar{s}</math>.
-Zakładamy tutaj, że znamy
+Zak³adamy tutaj, ¿e znamy
 zbiór nowo zaalokowanych lokacji <math>L \subseteq \mathbf{Loc}</math>.
@@ Linia 294: / Linia 294: @@
 \frac{s \setminus \{ (l, s(l)) \} , L \setminus \{ l \} \,\longrightarrow\, s'}
 {s, L \,\longrightarrow\, s'}
-\quad \mbox{ o ile } l \in L \mbox{ i } s(l) \mbox{ jest określone}
+\quad \mbox{ o ile } l \in L \mbox{ i } s(l) \mbox{ jest okre¶lone}
 </math>
-Teraz albo napiszemy w dodatkowym warunku, że
+Teraz albo napiszemy w dodatkowym warunku, ¿e
 <math>L = \mathrm{dom}(s'') \setminus \mathrm{dom}(s)</math>:
@@ Linia 309: / Linia 309: @@
 </math>
-albo możemy poprosić o pomoc w posprzątaniu tego, kto ,,nabałaganił", czyli
+albo mo¿emy poprosiæ o pomoc w posprz±taniu tego, kto ,,naba³agani³", czyli
-deklarację <math>d</math>.
+deklaracjê <math>d</math>.
 Niech deklaracja zwraca, oprócz pary <math>(E', s')</math>,
 dodatkowo zbiór <math>L</math>.
-Oto poprawione reguły dla deklaracji:
+Oto poprawione regu³y dla deklaracji:
@@ Linia 337: / Linia 337: @@
 </math>
-Wtedy ostatecznie reguła dla bloku wygląda następująco:
+Wtedy ostatecznie regu³a dla bloku wygl±da nastêpuj±co:
 <math>
@@ Linia 350: / Linia 350: @@
 }}
-{{cwiczenie|2 (wiązanie dynamiczne)|cw2|
+{{cwiczenie|2 (wi±zanie dynamiczne)|cw2|
-Zastanówmy się, jakich modyfikacji wymaga nasza semantyka,
+Zastanówmy siê, jakich modyfikacji wymaga nasza semantyka,
-aby wiązanie identyfikatorów było dynamiczne, zamiast statycznego.
+aby wi±zanie identyfikatorów by³o dynamiczne, zamiast statycznego.
-Rozumiemy przez to, że w przypadku odwołania do zmiennej
+Rozumiemy przez to, ¿e w przypadku odwo³ania do zmiennej
-wewnątrz procedury, odwułujemy się do środowiska w miejscu
+wewn±trz procedury, odwo³ujemy siê do ¶rodowiska w miejscu
-wywołania tej procedury, zamiast do środowiska z miejsca
+wywo³ania tej procedury, zamiast do ¶rodowiska z miejsca
 deklaracji jak dotychczas.
-Tak samo powinno być w przypadku wywołania innej procedury
+Tak samo powinno byæ w przypadku wywo³ania innej procedury
-wewnątrz procedury, czyli wiązanie dynamiczne dotyczy i zmiennych
+wewn±trz procedury, czyli wi±zanie dynamiczne dotyczy i zmiennych
 i procedur.
 }}
@@ Linia 373: / Linia 373: @@
     <math>\mathbf{begin}\,</math>
-      <math>\mathbf{var}\,</math> x = 10;
+      <math>\mathbf{var}\,</math> x = 10; <math>\mathbf{var}\,</math> z = 0;
-     <math>\mathbf{var}\,</math> z = 0;
       <math>\mathbf{call}\,</math> p(z);
@@ Linia 381: / Linia 380: @@
-Wartość końcowa zmiennej <math>z = 10</math>.
+Warto¶æ koñcowa zmiennej <math>z = 10</math>.
-Gdyby wiązanie zmiennej <math>x</math> było statyczne, to wartość ta
+Gdyby wi±zanie zmiennej <math>x</math> by³o statyczne, to warto¶æ ta
-wynosiłaby <math>1</math>. Podobnie dla procedur:
+wynosi³aby <math>1</math>. Podobnie dla procedur:
@@ Linia 399: / Linia 398: @@
-Wartość końcowa zmiennej <math>z = 8</math>.
+Warto¶æ koñcowa zmiennej <math>z = 8</math>.
-Gdyby widoczność procedury <math>q</math> była statyczna, to wartość ta
+Gdyby widoczno¶æ procedury <math>q</math> by³a statyczna, to warto¶æ ta
-wynosiłaby <math>4</math>.
+wynosi³aby <math>4</math>.
-A oto przykład programu, który nie wykonałby się poprawnie
+A oto przyk³ad programu, który nie wykona³by siê poprawnie
-przy wiązaniu statycznych, a wykonuje się poprawnie przy
+przy wi±zaniu statycznych, a wykonuje siê poprawnie przy
 dynamicznym:
   <math>\mathbf{begin}\,</math>
-    <math>\mathbf{proc}\,</math> q(x); \mathbf{call}\, r(x);
+    <math>\mathbf{proc}\,</math> q(x); <math>\mathbf{call}\,</math> r(x);
     <math>\mathbf{proc}\,</math> p(y);
       <math>\mathbf{begin}\,</math>
@@ Linia 418: / Linia 417: @@
     <math>\mathbf{call}\,</math> p(z);
-  \,\mathbf{end}
+  <math>\,\mathbf{end}</math>
-Wartość końcowa zmiennej <math>z</math> wynosi <math>14</math>.
+Warto¶æ koñcowa zmiennej <math>z</math> wynosi <math>14</math>.
-Procedura <math>p</math> wywołuje procedurę <math>r</math>,
+Procedura <math>p</math> wywo³uje procedurê <math>q</math>,
-,,przekazując" jej również środowisko z miejsca wołania,
+,,przekazuj±c" jej równie¿ ¶rodowisko z miejsca wo³ania,
-zawierające informację o procedurze <math>r</math>, która
+zawieraj±ce informacjê o procedurze <math>r</math>. Ta ostatnia
-przy widoczności statycznej byłaby lokalna, a teraz nie jest.
+przy widoczno¶ci statycznej by³aby lokalna, a teraz nie jest.
@@ Linia 432: / Linia 431: @@
 <div class="mw-collapsible mw-made=collapsible mw-collapsed"><div class="mw-collapsible-content" style="display:none">
-Spójrzmy na regułę dla wywołania procedury:
+Spójrzmy na regu³ê dla wywo³ania procedury:
 <math>
@@ Linia 442: / Linia 441: @@
 </math>
-O statyczności decyduje to, że wnętrze procedury <math>I</math>
+O statyczno¶ci decyduje to, ¿e wnêtrze procedury <math>I</math>
-wykonywane jest w środowisku zmiejsca deklaracji <math>E'</math>.
+wykonywane jest w ¶rodowisku zmiejsca deklaracji <math>E'</math>.
-Wystarczy więc, jeśli zignorujemy to środowisko, a zamiast
+Wystarczy wiêc, je¶li zignorujemy to ¶rodowisko, a zamiast
-niego użyjemy bieżącego środowiska <math>E</math> (czyli środowiska
+niego u¿yjemy bie¿±cego ¶rodowiska <math>E</math> (czyli ¶rodowiska
-z miejsca wywołania):
+z miejsca wywo³ania):
 <math>
@@ Linia 456: / Linia 455: @@
 </math>
-Oczywiście w takim przypadku w środowiskach
+Oczywi¶cie w takim przypadku w ¶rodowiskach
-wystarczy przechowywać dla procedur pary <math>\langle x, I \rangle</math>.
+wystarczy przechowywaæ dla procedur pary <math>\langle x, I \rangle</math>.
-Zastanówmy się teraz, jak uwzględnić rekurencję? Oczywiście
+Zastanówmy siê teraz, jak uwzglêdniæ rekurencjê? Oczywi¶cie
-moglibyśmy postąpić tak jak poprzednio, np.
+mogliby¶my post±piæ tak jak poprzednio, np.
 <math>
@@ Linia 470: / Linia 469: @@
 </math>
-ale jeśli uważnie przyjrzymy się tej regule, to okazuje się,
+ale je¶li uwa¿nie przyjrzymy siê tej regule, to okazuje siê,
-że ,,przelewamy z pustego w próżne". Sciślej,
+¿e ,,przelewamy z pustego w pró¿ne". Sci¶lej,
-dodajemy do <math>E</math> parę <math>x_1 \mapsto \langle x, I \rangle</math>,
+dodajemy do <math>E</math> parê <math>x_1 \mapsto \langle x, I \rangle</math>,
-która już tam tak naprawdę jest!
+która ju¿ tam tak naprawdê jest!
-Okazuje się, że dzięki dynamicznemu wiązaniu identyfikatorów ,,za
+Okazuje siê, ¿e dziêki dynamicznemu wi±zaniu identyfikatorów ,,za
-darmo" otrzymujemy rekurencje! Tak jest na przykład w programie:
+darmo" otrzymujemy rekurencje! Tak jest na przyk³ad w programie:
@@ Linia 486: / Linia 485: @@
-ponieważ w momencie wywołania rekurencyjnego <math>\mathbf{call}\, p(x)</math>,
+poniewa¿ w momencie wywo³ania rekurencyjnego <math>\mathbf{call}\, p(x)</math>,
-w środowisku jest już informacja nt. procedury <math>p</math>!
+w ¶rodowisku jest ju¿ informacja nt. procedury <math>p</math>!
 </div></div>
@@ Linia 493: / Linia 492: @@
-{{cwiczenie|3 (różne mechanizmy przekazywana parametru)|cw3|
+{{cwiczenie|3 (ró¿ne mechanizmy przekazywana parametru)|cw3|
-Rozważ inne mechanizmy przekazywania parametru (wiązanie statyczne):
+Rozwa¿ inne mechanizmy przekazywania parametru (wi±zanie statyczne):
-* przez wartość
+* przez warto¶æ
 <!--
-* przez nazwę leniwie (jak przez wartość, ale leniwa strategia ewaluacji parametru aktualnego)
+* przez nazwê leniwie (jak przez warto¶æ, ale leniwa strategia ewaluacji parametru aktualnego)
-* przez nazwę dynamicznie (dynamiczne wiązanie identyfikatorów podczas obliczania wartości parametru aktualnego)
+* przez nazwê dynamicznie (dynamiczne wi±zanie identyfikatorów podczas obliczania warto¶ci parametru aktualnego)
 -->
 * in-out
-Należy wyjaśnić ostatni mechanizm (in-out).
+Nale¿y wyja¶niæ ostatni mechanizm (in-out).
-Parametrem aktualnym jest zmienna, której wartość jest
+Parametrem aktualnym jest zmienna, której warto¶æ jest
 przypisywana parametrowi formalnemu (tak jak przy przekazywaniu
-przez wartość, gdy parametrem aktualnym jest zmienna).
+przez warto¶æ, gdy parametrem aktualnym jest zmienna).
-Ale po zakończeniu procedury, wartość parametru formalnego,
+Ale po zakoñczeniu procedury, warto¶æ parametru formalnego,
-która mogła zmienić się w czasie dzialania procedury, jest
+która mog³a zmieniæ siê w czasie dzialania procedury, jest
-spowrotem przypisywana na zmienną będącą parametrem aktualnym
+spowrotem przypisywana na zmienn± bêd±c± parametrem aktualnym
-(a więc podobnie do przekazywania przez zmienną).
+(a wiêc podobnie do przekazywania przez zmienn±).
 Parametr formalny jest traktowany jak zmienna lokalna procedury.
 }}
-{{rozwiazanie||roz3|
+{{rozwiazanie|(przekazywanie parametru przez warto¶æ)|roz1|
-'''Przekazywanie przez wartość'''
 <div class="mw-collapsible mw-made=collapsible mw-collapsed"><div class="mw-collapsible-content" style="display:none">
-Omówimy tylko instrukcję wywołania procedury, której składnia jest
+Omówimy tylko instrukcjê wywo³ania procedury, której sk³adnia jest
-teraz szersza niż poprzednio:
+teraz szersza ni¿ poprzednio:
 <math>
@@ Linia 532: / Linia 528: @@
 </math>
-Przed wywołaniem procedury należy zaalokować nową lokację,
+Przed wywo³aniem procedury nale¿y zaalokowaæ now± lokacjê,
-którą przypiszemy parametrowi formalnemu; następnie obliczamy
+któr± przypiszemy parametrowi formalnemu; nastêpnie obliczamy
-wartość parametru aktualnego i umieszczamy ją w tej lokacji:
+warto¶æ parametru aktualnego i umieszczamy j± w tej lokacji:
 <math>
@@ Linia 547: / Linia 543: @@
 </div></div>
+}}
+{{rozwiazanie|(przekazywanie parametru in-out)|roz3.2|
-'''Przekazywanie in-out'''
 <div class="mw-collapsible mw-made=collapsible mw-collapsed"><div class="mw-collapsible-content" style="display:none">
-Początkowo postępujemy tak jak w przypadku przekazywania przez
+Pocz±tkowo postêpujemy tak jak w przypadku przekazywania przez
-wartość: alokujemy nową lokację <math>l</math>, którą przypiszemy
+warto¶æ: alokujemy now± lokacjê <math>l</math>, któr± przypiszemy
-parametrowi formalnemu, i umieszczamy w niej wartość zmiennej
+parametrowi formalnemu, i umieszczamy w niej warto¶æ zmiennej
-(<math>x_2</math> w regule poniżej) będącej parametrem aktualnym.
+(<math>x_2</math> w regule poni¿ej) bêd±cej parametrem aktualnym.
-Zasadnicza różnica widoczna jest po zakończeniu procedury: wartość z lokacji
+Zasadnicza ró¿nica widoczna jest po zakoñczeniu procedury: warto¶æ z lokacji
-<math>l</math> powinna zostać spowrotem przypisana zmiennej <math>x_2</math>.
+<math>l</math> powinna zostaæ spowrotem przypisana zmiennej <math>x_2</math>.
-Oto reguła:
+Oto regu³a:
 <math>
@@ Linia 566: / Linia 562: @@
 \quad \mbox{ o ile }
 E(x_2) = l_2 \in \mathbf{Loc} \mbox{ i }
-s(l_2) \mbox{ jest określone i }
+s(l_2) \mbox{ jest okre¶lone i }
 E(x_1) = \langle x, I, E' \rangle \in \mathbf{Proc} \mbox{ i }
 l = \mathtt{newloc}(s)
@@ Linia 578: / Linia 574: @@
-==== Zadanie 1 ====
+{{cwiczenie|1|cw1.dom|
+Zaadaptuj semantykê ,,deklaracji równoleg³ych"
+dla rekurencji wzajemnej wewn±trz jednej deklaracji równoleg³ej.
+To znaczy, ¿e procedury zadeklarowane w jednej deklaracji równoleg³ej
+mog± siê wzajemniej wywo³ywaæ bez ¿adnych ograniczeñ.
+}}
-Zaadaptuj semantykę ,,deklaracji równoległych"
-dla rekurencji wzajemnej wewnątrz jednej deklaracji równoległej.
-To znaczy, że procedury zadeklarowane w jednej deklaracji równoległej
-mogą się wzajemniej wywoływać bez żadnych ograniczeń.
+{{cwiczenie|2|cw2.dom|
-==== Zadanie 2 ====
+Zamiast procedur, rozwa¿ funkcje z pojedynczym parametrem
+przekazywanym przez zmienn±.
-Zamiast procedur, rozważ funkcje z pojedynczym parametrem
+Wywo³anie funkcji mo¿e teraz pojawiæ siê wewn±trz wyra¿enia:
-przekazywanym przez zmienną.
-Wywołanie funkcji może teraz pojawić się wewnątrz wyrażenia:
 <math>
 e \, ::= \,\,
            \ldots \,\,|\,\,
-           \mathbf{call}\, x_1(x_2)
+           \mathbf{call}\, x_1(x_2).
 </math>
 Uwaga na efekty uboczne!
+}}
-==== Zadanie 3 ====
+{{cwiczenie|3|cw3.dom|
-Rozważ następujące warianty:
+Rozwa¿ nastêpuj±ce warianty:
-* wiązanie zmiennych jest statyczne a procedur dynamiczne
+* wi±zanie zmiennych jest statyczne a procedur dynamiczne
-* wiązanie zmiennych jest dymamiczne a procedur statyczne
+* wi±zanie zmiennych jest dymamiczne a procedur statyczne.
+}}
-==== Zadanie 4 ====
+{{cwiczenie|4|cw4.dom|
-Rozszerz semantykę procedur tak, aby parametrem aktualnym procedury
+Rozszerz semantykê procedur tak, aby parametrem aktualnym procedury
-mogła byc procedura.
+mog³a byæ procedura.
+}}