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

Wersja z 08:11, 10 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}) .$

Wewnatrz funkcji jej nazwa mozna poslugiwac sie jak zmienna lokalna. Wynik zwracany przez funkcje to wartosc tej zmiennej w momencie wyjscia z funkcji.

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:11, 10 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.
@@ Linia 17: / Linia 17: @@
 {{cwiczenie|1 (procedury)|cw1|
-Rozszerzmy jêzyk 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> deklaruje 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, odwo³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 380: / 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 398: / 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:
@@ Linia 420: / Linia 420: @@
-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>q</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>. Ta ostatnia
+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 431: / 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 441: / 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 455: / 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 469: / 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 485: / 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 492: / 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|(przekazywanie parametru przez warto¶æ)|roz1|
+{{rozwiazanie|(przekazywanie parametru przez wartość)|roz1|
 <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 528: / 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 549: / Linia 549: @@
 <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 562: / 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 576: / Linia 576: @@
 {{cwiczenie|1|cw1.dom|
-Zaadaptuj semantykê ,,deklaracji równoleg³ych"
+Zaadaptuj semantykę ,,deklaracji równoległych"
-dla rekurencji wzajemnej wewn±trz jednej deklaracji równoleg³ej.
+dla rekurencji wzajemnej wewnątrz jednej deklaracji równoległej.
-To znaczy, ¿e procedury zadeklarowane w jednej deklaracji równoleg³ej
+To znaczy, że procedury zadeklarowane w jednej deklaracji równoległej
-mog± siê wzajemniej wywo³ywaæ bez ¿adnych ograniczeñ.
+mogą się wzajemniej wywoływać bez żadnych ograniczeń.
 }}
@@ Linia 585: / Linia 585: @@
 {{cwiczenie|2|cw2.dom|
-Zamiast procedur, rozwa¿ funkcje z pojedynczym parametrem
+Zamiast procedur, rozważ funkcje z pojedynczym parametrem
-przekazywanym przez zmienn±.
+przekazywanym przez zmienną.
-Wywo³anie funkcji mo¿e teraz pojawiæ siê wewn±trz wyra¿enia:
+Wywołanie funkcji może teraz pojawić się wewnątrz wyrażenia:
 <math>
@@ Linia 606: / Linia 606: @@
 {{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.
 }}
@@ Linia 615: / Linia 615: @@
 {{cwiczenie|4|cw4.dom|
-Rozszerz semantykê procedur tak, aby parametrem aktualnym procedury
+Rozszerz semantykę procedur tak, aby parametrem aktualnym procedury
-mog³a byæ procedura.
+mogła być procedura.
 }}