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

Aktualna wersja na dzień 21:39, 11 wrz 2023

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

Użyjemy środowisk $E \in 𝐄 𝐧 𝐯$ i stanów $s \in 𝐒 𝐭 𝐨 𝐫 𝐞$ :

$𝐒 𝐭 𝐨 𝐫 𝐞 = 𝐋 𝐨 𝐜 \to_{f i n} 𝐍 𝐮 𝐦 𝐄 𝐧 𝐯 = 𝐕 𝐚 𝐫 \to_{f i n} (𝐋 𝐨 𝐜 \cup 𝐏 𝐫 𝐨 𝐜)$

Nowym elementem jest zbiór $𝐏 𝐫 𝐨 𝐜$ , potrzebny nam do przechowywania informacji o procedurach. Informacja na temat procedury, którą musimy przechowywać, to:

nazwa parametru formalnego,
ciało procedury (instrukcja $I \in 𝐒 𝐭 𝐦 𝐭$ ) oraz
środowisko, w którym procedura została zadeklarowana.

Zauważmy, że nie musimy (i nie powinniśmy) pamiętać stanu z momentu deklaracji, czyli konkretnych wartości zmiennych wówczas zadeklarowanych. Pamiętamy tylko środowisko, które wyznacza nam wiązanie identyfikatorów (nazw zmiennych i procedur) występujących w ciele procedury z lokacjami (lub opisami procedur z $𝐏 𝐫 𝐨 𝐜$ ), a więc z konkretnymi zmiennymi (lub procedurami). Widać tutaj jasno, jak elegancki i wygodny jest podział na środowisko i stan.

Zatem niech $𝐏 𝐫 𝐨 𝐜 = 𝐕 𝐚 𝐫 \times 𝐒 𝐭 𝐦 𝐭 \times 𝐄 𝐧 𝐯$ . Czyli znów zbiór $𝐄 𝐧 𝐯$ zadany jest przez równanie.

Nasze tranzycje będą następujących postaci:

$E ⊢ e, s ⟶ n E ⊢ b, s ⟶ l$

$E ⊢ I, s ⟶ s^{'} E ⊢ d, s ⟶ (E^{'}, s^{'})$

Na uwagę zasługuje ostatnia postać tranzycji: deklaracja, w odróżnieniu od instrukcji, może zmieniać środowisko. Umówmy się, że środowisko $E^{'}$ będzie rozszerzało $E$ o informację o nowych identyfikatorach, tzn. tych zadeklarowanych w $d$ .

Zajmijmy się najpierw deklaracjami zmiennych:

$\frac{E ⊢ e, s ⟶ n}{E ⊢ 𝐯 𝐚 𝐫 x = e, s ⟶ (E^{'}, s^{'})} gdzie E^{'} = E [x \mapsto l], s^{'} = s [l \mapsto n], l = n e w l o c (s)$

i procedur:

$E ⊢ 𝐩 𝐫 𝐨 𝐜 x_{1} (x_{2}); I, s ⟶ (E^{'}, s) gdzie E^{'} = E [x_{1} \mapsto ⟨ x_{2}, I, E ⟩]$

Zauważmy, że deklaracja procedury nie zmienia stanu, tylko środowisko, w odróżnieniu od deklaracji zmiennej. W środowisku pamiętamy trójkę $⟨ x_{2}, I, E ⟩$ zawierającą nazwę parametru formalnego, ciało procedury oraz środowisko deklaracji procedury. To ostatnie determinuje statyczne wiązanie identyfikatorów: wiązanie identyfikatorów występujących w ciele procedury jest jakby "zamrożone" (ustalone) w momencie deklaracji procedury. Aby dokończyć semantykę deklaracji potrzebujemy jeszcze jednej reguły:

$\frac{E ⊢ d_{1}, s ⟶ (E^{'}, s^{'}) E^{'} ⊢ d_{2}, s^{'} ⟶ (E^{″}, s^{″})}{E ⊢ d_{1}; d_{2}, s ⟶ (E^{″}, s^{″})}$

która opisuje sekwencyjną "kumulację" modyfikacji dokonanych w deklaracjach.

Pytanie: czy kolejność poszczególnych deklaracji ma znaczenie?

Teraz określimy semantykę bloku:

$\frac{E ⊢ d, s ⟶ (E^{'}, s^{'}) E^{'} ⊢ I, s^{'} ⟶ s^{″}}{E ⊢ 𝐛 𝐞 𝐠 𝐢 𝐧 d; I 𝐞 𝐧 𝐝, s ⟶ s^{″}}$

Czyli instrukcja wewnętrzna wykonywana jest w środowisku (i stanie) wytworzonym (rozszerzonym) przez deklarację $d$ . Stan końcowy po wykonaniu bloku to po prostu stan końcowy $s^{″}$ po wykonaniu instrukcji wewnętrznej. Może się to wydawać niepokojące, gdyż oznacza, że nowe lokacje, powołane podczas deklaracji $d$ , zachowują przechowywaną wartość również po wyjściu z bloku. Na szczęście wykonanie bloku nie ma wpływu na środowisko, a to ono decyduje, które identyfikatory są widoczne (zadeklarowane) i ogólniej, które lokacje są przypisane identyfikatorom. A więc deklaracja $d$ nie ma wpływu na środowisko, w którym zostaną wykonane kolejne instrukcje. Widać to jasno w regule dla złożenia sekwencyjnego:

$\frac{E ⊢ I_{1}, s ⟶ s^{'} E, ⊢ I_{2}, s^{'} ⟶ s^{″}}{E ⊢ I_{1}; I_{2}, s ⟶ s^{″}}$

Pozostało nam jeszcze określenie semantyki wywołania procedury:

$\frac{E^{'} [x \mapsto l] ⊢ I, s ⟶ s^{'}}{E ⊢ 𝐜 𝐚 𝐥 𝐥 x_{1} (x_{2}), s ⟶ s^{'}} o ile E (x_{1}) = ⟨ x, I, E^{'} ⟩ \in 𝐏 𝐫 𝐨 𝐜 i E (x_{2}) = l \in 𝐋 𝐨 𝐜$

Czyli uruchamiane jest ciało $I$ procedury, w środowisku $E^{'}$ z miejsca deklaracji tej procedury zmodyfikowanym o przypisanie $x \mapsto l$ lokacji $l$ do parametru formalnego $x$ procedury. Stan, w którym uruchomione jest $I$ , to po prostu stan bieżący z miejsca wołania procedury; o prawidłowe wiązanie identyfikatorów "troszczy" się wyłącznie środowisko $E^{'}$ .

Pytanie: czy powyższa reguła dopuszcza rekurencyjne wywołania procedury?

Okazuje się, że niestety nie, gdyż w środowisku $E^{'} [x \mapsto l]$ nie ma informacji o procedurze $x_{1}$ , którą właśnie wołamy. Może się zdarzyć, że $E^{'} [x \mapsto l] \in 𝐏 𝐫 𝐨 𝐜$ , ale oznacza to tylko, że w miejscu deklaracji procedury $x_{1}$ była już wcześniej (statycznie) zadeklarowana inna procedura o tej samej nazwie. Aby umożliwić rekurencję, powinniśmy zadbać sami o to, aby środowisko, w którym wykonujemy $I$ zawierało informację o naszej procedurze:

$\frac{E^{'} [x \mapsto l] [x_{1} \mapsto ⟨ x, I, E^{'} ⟩] ⊢ I, s ⟶ s^{'}}{E ⊢ 𝐜 𝐚 𝐥 𝐥 x_{1} (x_{2}), s ⟶ s^{'}} o ile E (x_{1}) = ⟨ x, I, E^{'} ⟩ \in 𝐏 𝐫 𝐨 𝐜 i E (x_{2}) = l \in 𝐋 𝐨 𝐜$

Zauważmy, że przypisanie $x_{1} \mapsto ⟨ x, I, E^{'} ⟩$ dodane do $E^{'}$ wystarcza na tylko jedno wywołanie rekurencyjne (licząc w głąb). Ale każde kolejne wywołanie dodaje tę informację, czyli każde wywołanie procedury przygotowuje środowisko dla następnego. I to jest wystarczające.

Pytanie: czy możliwa jest rekurencja wzajemna?

Pozostaje jeszcze jedna kwestia: dodajemy do środowiska $E^{'}$ dwa przypisania: $x \mapsto l$ oraz $x_{1} \mapsto ⟨ x, I, E^{'} ⟩$ , ale dlaczego w takiej kolejności?

Pytanie: co się stanie, gdy zamienimy tę kolejność:

$\frac{E^{'} [x_{1} \mapsto ⟨ x, I, E^{'} ⟩] [x \mapsto l] ⊢ I, s ⟶ s^{'}}{E ⊢ 𝐜 𝐚 𝐥 𝐥 x_{1} (x_{2}), s ⟶ s^{'}} o ile E (x_{1}) = ⟨ x, I, E^{'} ⟩ \in 𝐏 𝐫 𝐨 𝐜 i E (x_{2}) = l \in 𝐋 𝐨 𝐜$

Czy obydwie semantyki są sobie równoważne?

Okazuje się, że tak nie jest, oto dwa kontrprzykłady:

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

   $𝐜 𝐚 𝐥 𝐥$ , x(y);
 $𝐞 𝐧 𝐝$

 $𝐛 𝐞 𝐠 𝐢 𝐧$ ,
   $𝐯 𝐚 𝐫$ , y = 7;
   $𝐩 𝐫 𝐨 𝐜$ , x(x);
     $𝐢 𝐟$ , y > 0  $𝐭 𝐡 𝐞 𝐧$ , y := y-1;  $𝐜 𝐚 𝐥 𝐥$ , x(y)  $𝐞 𝐥 𝐬 𝐞 𝐬 𝐤 𝐢 𝐩$ ;

   $𝐜 𝐚 𝐥 𝐥$ , x(y);
 $𝐞 𝐧 𝐝$

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.

Rozważmy na koniec problem dealokacji.

Wariant (dealokacja)

Chcemy, aby "posprzątano" po zakończeniu wykonania 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. Oznacza to, że powinniśmy przywrócić nieokreśloność stanu dla wszystkich tych lokacji, które były użyte podczas deklaracji $d$ .

Jest wiele możliwości wyrażenia tego dodatkowego warunku, np. możemy dodać do powyższej reguły

$\frac{E ⊢ d, s ⟶ (E^{'}, s^{'}) E^{'} ⊢ I, s^{'} ⟶ s^{″}}{E ⊢ 𝐛 𝐞 𝐠 𝐢 𝐧 d; I 𝐞 𝐧 𝐝, s ⟶ \bar{s}}$

dodatkowy warunek postaci: $gdzie \bar{s} = \dots$ . Proponujemy tu rozwiązanie ciut bardziej eleganckie. Zacznijmy od tranzycji dokonujących dealokacji, które mogą być np. postaci $s^{″}, L ⟶ \bar{s}$ . Zakładamy tutaj, że znamy zbiór nowo zaalokowanych lokacji $L \subseteq 𝐋 𝐨 𝐜$ .

$s, \emptyset ⟶ s \frac{s ∖ {(l, s (l))}, L ∖ {l} ⟶ s^{'}}{s, L ⟶ s^{'}} o ile l \in L i s (l) jest określone$

Teraz albo napiszemy w dodatkowym warunku, że $L = d o m (s^{″}) ∖ d o m (s)$ :

$\frac{E ⊢ d, s ⟶ (E^{'}, s^{'}) E^{'} ⊢ I, s^{'} ⟶ s^{″} s^{″}, L ⟶ \bar{s}}{E ⊢ 𝐛 𝐞 𝐠 𝐢 𝐧 d; I 𝐞 𝐧 𝐝, s ⟶ \bar{s}} gdzie L = d o m (s^{″}) ∖ d o m (s)$

albo możemy poprosić o pomoc w posprzątaniu tego, kto "nabałaganił", czyli deklarację $d$ . Niech deklaracja zwraca, oprócz pary $(E^{'}, s^{'})$ , dodatkowo zbiór $L$ . Oto poprawione reguły dla deklaracji:

$\frac{E ⊢ e, s ⟶ n}{E ⊢ 𝐯 𝐚 𝐫 x = e, s ⟶ (E^{'}, s^{'}, {l}) gdzie E^{'} = E [x \mapsto l], s^{'} = s [l \mapsto n], l = n e w l o c (s)}$

$E ⊢ 𝐩 𝐫 𝐨 𝐜 x_{1} (x_{2}); I, s ⟶ (E^{'}, s, \emptyset) gdzie E^{'} = E [x_{1} \mapsto ⟨ x_{2}, I, E ⟩]$

$\frac{E ⊢ d_{1}, s ⟶ (E^{'}, s^{'}, L^{'}) E^{'} ⊢ d_{2}, s^{'} ⟶ (E^{″}, s^{″}, L^{″})}{E ⊢ d_{1}; d_{2}, s ⟶ (E^{″}, s^{″}, L^{'} \cup L^{″})}$

Wtedy ostatecznie reguła dla bloku wygląda następująco:

$\frac{E ⊢ d, s ⟶ (E^{'}, s^{'}, L) E^{'} ⊢ I, s^{'} ⟶ s^{″} s^{″}, L ⟶ \bar{s}}{E ⊢ 𝐛 𝐞 𝐠 𝐢 𝐧 d; I 𝐞 𝐧 𝐝, s ⟶ \bar{s}}$

Ć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

Spójrzmy na regułę dla wywołania procedury:

$\frac{E^{'} [x \mapsto l] ⊢ I, s ⟶ s^{'}}{E ⊢ 𝐜 𝐚 𝐥 𝐥 x_{1} (x_{2}), s ⟶ s^{'}} o ile E (x_{1}) = ⟨ x, I, E^{'} ⟩ \in 𝐏 𝐫 𝐨 𝐜 i E (x_{2}) = l \in 𝐋 𝐨 𝐜$

O statyczności decyduje to, że wnętrze procedury $I$ wykonywane jest w środowisku zmiejsca deklaracji $E^{'}$ . Wystarczy więc, jeśli zignorujemy to środowisko, a zamiast niego użyjemy bieżącego środowiska $E$ (czyli środowiska z miejsca wywołania):

$\frac{E [x \mapsto l] ⊢ I, s ⟶ s^{'}}{E ⊢ 𝐜 𝐚 𝐥 𝐥 x_{1} (x_{2}), s ⟶ s^{'}} o ile E (x_{1}) = ⟨ x, I, E^{'} ⟩ \in 𝐏 𝐫 𝐨 𝐜 i E (x_{2}) = l \in 𝐋 𝐨 𝐜$

Oczywiście w takim przypadku w środowiskach wystarczy przechowywać dla procedur pary $⟨ x, I ⟩$ .

Zastanówmy się teraz, jak uwzględnić rekurencję? Moglibyśmy postąpić tak jak poprzednio, np.

$\frac{E [x \mapsto l] [x_{1} \mapsto ⟨ x, I ⟩] ⊢ I, s ⟶ s^{'}}{E ⊢ 𝐜 𝐚 𝐥 𝐥 x_{1} (x_{2}), s ⟶ s^{'}} o ile E (x_{1}) = ⟨ x, I ⟩ \in 𝐏 𝐫 𝐨 𝐜 i E (x_{2}) = l \in 𝐋 𝐨 𝐜$

ale jeśli uważnie przyjrzymy się tej regule, to okazuje się, że "przelewamy z pustego w próżne". Sciślej, dodajemy do $E$ parę $x_{1} \mapsto ⟨ x, I ⟩$ , która już tam tak naprawdę jest! Okazuje się, że dzięki dynamicznemu wiązaniu identyfikatorów "za darmo" otrzymujemy rekurencje! Tak jest na przykład w programie:

 $𝐛 𝐞 𝐠 𝐢 𝐧$ ,
   $𝐩 𝐫 𝐨 𝐜$ , p(x);  $𝐢 𝐟$ , x < 100  $𝐭 𝐡 𝐞 𝐧$ , x := x+x;  $𝐜 𝐚 𝐥 𝐥$ , p(x)  $𝐞 𝐥 𝐬 𝐞 𝐬 𝐤 𝐢 𝐩$ ;
   $𝐯 𝐚 𝐫$ , z = 8;

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

ponieważ w momencie wywołania rekurencyjnego $𝐜 𝐚 𝐥 𝐥 p (x)$ , w środowisku jest już informacja nt. procedury $p$ !

Ć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 z powrotem 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ść)

Omówimy tylko instrukcję wywołania procedury, której składnia jest teraz szersza niż poprzednio:

$I : : = \dots | 𝐜 𝐚 𝐥 𝐥 x (e)$

Przed wywołaniem procedury należy zaalokować nową lokację, którą przypiszemy parametrowi formalnemu; następnie obliczamy wartość parametru aktualnego i umieszczamy ją w tej lokacji:

$\frac{E ⊢ e, s ⟶ n E^{'} [x^{'} \mapsto l] ⊢ I, s [l \mapsto n] ⟶ s^{'}}{E ⊢ 𝐜 𝐚 𝐥 𝐥 x (e), s ⟶ s^{'}} o ile E (x) = ⟨ x^{'}, I, E^{'} ⟩ \in 𝐏 𝐫 𝐨 𝐜 i l = n e w l o c (s)$

Rozwiązanie (przekazywanie parametru in-out)

Początkowo postępujemy tak jak w przypadku przekazywania przez wartość: alokujemy nową lokację $l$ , którą przypiszemy parametrowi formalnemu i umieszczamy w niej wartość zmiennej ( $x_{2}$ w regule poniżej) będącej parametrem aktualnym. Zasadnicza różnica widoczna jest po zakończeniu procedury: wartość z lokacji $l$ powinna zostać spowrotem przypisana zmiennej $x_{2}$ . Oto reguła:

$\frac{E^{'} [x \mapsto l] ⊢ I, s [l \mapsto s (l_{2})] ⟶ s^{'}}{E ⊢ 𝐜 𝐚 𝐥 𝐥 x_{1} (x_{2}), s ⟶ s^{'} [l_{2} \mapsto s^{'} (l)]} o ile E (x_{2}) = l_{2} \in 𝐋 𝐨 𝐜 i s (l_{2}) jest określone i$ $E (x_{1}) = ⟨ x, I, E^{'} ⟩ \in 𝐏 𝐫 𝐨 𝐜 i l = n e w l o c (s)$

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})$

Wewnątrz funkcji jej nazwą można posługiwać się jak zmienną lokalną. Wynik zwracany przez funkcję to wartość tej zmiennej w momencie wyjścia 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 dynamiczne, 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

Aktualna wersja na dzień 21:39, 11 wrz 2023

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ść ==
+Ostatnie zajęcia poświęcone semantyce naturalnej.
-== Zawarto¶æ ==
+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.
-Ostatnie zajêcia po¶wiêcone semantyce naturalnej.
+Pracujemy ze środowiskami i stanami.
-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.
@@ Linia 17: / Linia 12: @@
 {{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 28: @@
 </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>.
-<math>x_1</math>, której parametrem formalnym jest <math>x_2</math>.
+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).
-Zak³adamy statyczne wi±zanie identyfikatorów i przekazywanie
+Instrukcja <math>\mathbf{call}\, x_1(x_2)</math> wywołuje procedurę <math>x_1</math> z parametrem aktualnym <math>x_2</math>.
-parametrów przez zmienn± (to znaczy, ¿e w momencie wywo³ania
-procedury, powinna zostaæ
-przekazana lokacja odpowiadaj±ca parametrowi aktualnemu).
-Instrukcja <math>\mathbf{call}\, x_1(x_2)</math> wywo³uje procedurê <math>x_1</math>
-z parametrem aktualnym <math>x_2</math>.
 }}
-{{rozwiazanie||roz1|
+<div class="mw-collapsible mw-made=collapsible mw-collapsed">
+<span class="mw-collapsible-toogle mw-collapsible-toogle-default style="font-variant:small-caps">Rozwiązanie</span>
+<div class="mw-collapsible-content" style="display:none">
-<div class="mw-collapsible mw-made=collapsible mw-collapsed"><div class="mw-collapsible-content" style="display:none">
+Użyjemy ś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>
 \mathbf{Store} = \mathbf{Loc} \to_{\mathrm{fin}} \mathbf{Num}
 \quad \quad \quad
-\mathbf{Env}= \mathbf{Var} \to_{\mathrm{fin}} (\mathbf{Loc} \cup \mathbf{Proc}).
+\mathbf{Env}= \mathbf{Var} \to_{\mathrm{fin}} (\mathbf{Loc} \cup \mathbf{Proc})</math>
-</math>
-Nowym elementem jest zbiór <math>\mathbf{Proc}</math>, potrzebny nam do
+Nowym elementem jest zbiór <math>\mathbf{Proc}</math>, potrzebny nam do przechowywania informacji o procedurach.
-przechowywania informacji o procedurach.
+Informacja na temat 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.
-wówczas zadeklarowanych. Pamiêtamy tylko ¶rodowisko,
+Pamiętamy tylko środowisko, które wyznacza nam ''wiązanie'' identyfikatorów (nazw zmiennych i procedur) występujących w ciele procedury z lokacjami (lub opisami procedur z <math>\mathbf{Proc}</math>), a więc z konkretnymi zmiennymi (lub procedurami).
-które wyznacza nam ''wi±zanie'' identyfikatorów (nazw
+Widać tutaj jasno, jak elegancki i wygodny jest podział na środowisko i stan.
-zmiennych i procedur) wystêpuj±cych w ciele procedury z
-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
-i stan.
 Zatem niech <math>\mathbf{Proc} = \mathbf{Var} \times \mathbf{Stmt} \times \mathbf{Env}</math>.
 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 74: @@
 </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ę o nowych identyfikatorach, tzn. tych zadeklarowanych w <math>d</math>.
-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>
 \frac{E \,\vdash\, e, s \,\longrightarrow\, n}
       {E \,\vdash\, \mathbf{var}\, x=e, s \,\longrightarrow\, (E', s')}
-\quad \mbox{ gdzie } E' = E[x mapsto l],\,
+\quad \mbox{ gdzie } E' = E[x \mapsto l],\,
                       s' = s[l \mapsto n],\,
                       l = \mathtt{newloc}(s)
@@ Linia 111: / Linia 92: @@
 E \,\vdash\, \mathbf{proc}\, x_1(x_2);\, I, s \,\longrightarrow\, (E', s)
 \quad \mbox{ gdzie }
-E' = E[x_1 \mapsto \langle x_2, I, E \rangle].
+E' = E[x_1 \mapsto \langle x_2, I, E \rangle]</math>
-</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ą nazwę parametru formalnego, ciało procedury oraz ''środowisko deklaracji procedury''.
-W ¶rodowisku pamiêtamy trójkê <math>\langle x_2, I, E \rangle</math> zawieraj±c±
+To ostatnie determinuje statyczne wiązanie identyfikatorów: wiązanie identyfikatorów występujących w ciele procedury jest jakby "zamrożone" (ustalone) w momencie deklaracji procedury.
-nazwê parametru formalnego, cia³o procedury oraz ''¶rodowisko
+Aby dokończyć semantykę deklaracji potrzebujemy jeszcze jednej reguły:
-deklaracji procedury''.
-To ostatnie determinuje statyczne wi±zanie identyfikatorów:
-wi±zanie identyfikatorów wystêpuj±cuch w ciele procedury jest
-jakby ,,zamro¿one'' (ustalone) w momencie deklaracji procedury.
-Aby dokoñczyæ semantykê deklaracji potrzebujemy jeszcze jednej regu³y:
 <math>
@@ Linia 131: / Linia 106: @@
 </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 119: @@
 </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> po wykonaniu instrukcji wewnętrznej.
-Stan koñcowy po wykonaniu bloku to po prostu stan koñcowy <math>s''</math>
+Może się to wydawać niepokojące, gdyż oznacza, że nowe lokacje, powołane podczas deklaracji <math>d</math>, zachowują przechowywaną wartość również po wyjściu z bloku.
-po wykonaniu instrukcji wewnêtrznej.
+Na szczęście wykonanie bloku nie ma wpływu na środowisko, a to ono decyduje, które identyfikatory są widoczne (zadeklarowane) i ogólniej, które lokacje są przypisane identyfikatorom.
-Mo¿e siê to wydawaæ niepokoj±ce, gdy¿ oznacza, ¿e nowe lokacje,
+A więc deklaracja <math>d</math> nie ma wpływu na środowisko, w którym zostaną wykonane kolejne instrukcje.
-powo³ane podczas deklaracji <math>d</math>, zachowuj± przechowywan± warto¶æ
+Widać to jasno w regule dla złożenia sekwencyjnego:
-równie¿ po wyj¶ciu z bloku. Na szczê¶cie wykonanie
-bloku nie ma wp³ywu na ¶rodowisko, a to ono decyduje, które
-identyfikatory s± widoczne (zadeklarowane) i ogólniej, które lokacje
-s± przypisane identyfikatorom. A wiêc deklaracja <math>d</math>
-nie ma wp³ywu na ¶rodowisko, w którym zostan± wykonane kolejne
-instrukcje.
-Widaæ to jasno w regule dla z³o¿enia sekwencyjnego:
 <math>
@@ Linia 166: / Linia 134: @@
-Pozosta³o nam jeszcze okre¶lenie semantyki wywo³ania procedury:
+Pozostało nam jeszcze określenie semantyki wywołania procedury:
 <math>
@@ Linia 173: / Linia 141: @@
 \quad \mbox{ o ile }
 E(x_1) = \langle x, I, E' \rangle \in \mathbf{Proc} \mbox{ i }
-E(x_2) = l \in \mathbf{Loc}
+E(x_2) = l \in \mathbf{Loc}</math>
-</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 zmodyfikowanym o przypisanie <math>x \mapsto l</math> lokacji <math>l</math> do parametru formalnego <math>x</math> procedury.
-w ¶rodowisku <math>E'</math> z miejsca deklaracji tej procedury
+Stan, w którym uruchomione jest <math>I</math>, to po prostu stan bieżący z miejsca wołania procedury; o prawidłowe wiązanie identyfikatorów "troszczy" się wyłącznie środowisko <math>E'</math>.
-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
-wi±zanie identyfikatorów ,,troszczy" siê wy³±cznie
-¶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ą właśnie wołamy.
-<math>E'[x \mapsto l]</math> nie ma informacji o procedurze <math>x_1</math>, któr±
+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> była już wcześniej (statycznie) zadeklarowana inna procedura o tej samej nazwie.
-w³a¶nie wo³amy. Mo¿e siê zdarzyæ, ¿e <math>E'[x \mapsto l] \in \mathbf{Proc}</math>, ale
+Aby umożliwić rekurencję, powinniśmy zadbać sami o to, aby środowisko, w którym wykonujemy <math>I</math> zawierało informację o naszej procedurze:
-oznacza to tylko, ¿e w miejscu deklaracji procedury <math>x_1</math>
-by³a ju¿ wcze¶niej (statycznie) zadeklarowana inna procedura
-o tej samej nazwie.
-Aby umo¿liwiæ rekurencjê, powinni¶my zadbaæ sami o to, aby
-¶rodowisko, w którym wykonujemy <math>I</math> zawiera³o informacjê
-o naszej procedurze:
 <math>
@@ Linia 202: / Linia 157: @@
 \quad \mbox{ o ile }
 E(x_1) = \langle x, I, E' \rangle \in \mathbf{Proc} \mbox{ i }
-E(x_2) = l \in \mathbf{Loc}
+E(x_2) = l \in \mathbf{Loc}</math>
-</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 (licząc w głąb).
-dodane  do <math>E'</math> wystarcza na tylko jedno wywo³anie rekurencyjne
+Ale każde kolejne wywołanie dodaje tę informację, czyli każde wywołanie procedury przygotowuje środowisko dla następnego.
-(licz±c w g³±b). Ale ka¿de kolejne wywo³anie dodaje tê informacjê,
+I to jest wystarczające.
-czyli ka¿de wywo³anie procedury przygotowuje ¶rodowisko dla
-nastêpnego.
-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:
-dwa przypisania:
+<math>x \mapsto l</math> oraz <math>x_1 \mapsto \langle x, I, E' \rangle</math>, ale dlaczego w takiej kolejności?
-<math>x \mapsto l</math> oraz <math>x_1 \mapsto \langle x, I, E' \rangle</math>,
-ale dlaczego w takiej kolejno¶ci.
-'''Pytanie:''' co siê stanie, gdy zamienimy tê kolejno¶æ:
+'''Pytanie:''' co się stanie, gdy zamienimy tę kolejność:
 <math>
@@ Linia 226: / Linia 175: @@
 \quad \mbox{ o ile }
 E(x_1) = \langle x, I, E' \rangle \in \mathbf{Proc} \mbox{ i }
-E(x_2) = l \in \mathbf{Loc}
+E(x_2) = l \in \mathbf{Loc}</math>
-</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:
-  <math>\mathbf{begin}\,</math>
+  <math>\mathbf{begin}\ </math>,
-    <math>\mathbf{var}\,</math> y = 7;
+    <math>\mathbf{var}\ </math>, y = 7;
-    <math>\mathbf{proc}\,</math> x(x); x := x+1;
+    <math>\mathbf{proc}\ </math>, x(x); x := x+1;
-    <math>\mathbf{call}\,</math> x(y);
+    <math>\mathbf{call}\ </math>, x(y);
-  \,\mathbf{end}
+  <math>\,\mathbf{end}</math>
-  \mathbf{begin}\,
+  <math>\mathbf{begin}\ </math>,
-    <math>\mathbf{var}\,</math> y = 7;
+    <math>\mathbf{var}\ </math>, y = 7;
-    <math>\mathbf{proc}\,</math> x(x);
+    <math>\mathbf{proc}\ </math>, x(x);
-      <math>\mathbf{if}\,</math> y > 0 <math>\,\mathbf{then}\,</math> y := y-1; <math>\mathbf{call}\,</math> x(y) <math>\,\mathbf{else}\, \mathbf{skip}</math>;
+      <math>\mathbf{if}\ </math>, y > 0 <math>\,\mathbf{then}\ </math>, y := y-1; <math>\mathbf{call}\ </math>, x(y) <math>\,\mathbf{else}\, \mathbf{skip}</math>;
-    <math>\mathbf{call}\,</math> x(y);
+    <math>\mathbf{call}\ </math>, x(y);
-  \,\mathbf{end}
+  <math>\,\mathbf{end}</math>
-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.
-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.
 <br>
@@ Linia 266: / Linia 212: @@
 <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 i w związku z tym nie będą już potrzebne.
-tzn. aby zwolniono te lokacje, które by³y u¿ywane tylko w tym bloku
+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>.
-i w zwi±zku z tym nie bêd± ju¿ potrzebne.
-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>.
-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 282: / Linia 224: @@
 </math>
-dodatkowy warunek postaci <math>\mbox{ gdzie } \bar{s} = \ldots</math>.
+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 zbiór nowo zaalokowanych lokacji <math>L \subseteq \mathbf{Loc}</math>.
-Zak³adamy tutaj, ¿e znamy
-zbiór nowo zaalokowanych lokacji <math>L \subseteq \mathbf{Loc}</math>.
 <math>
@@ Linia 294: / Linia 234: @@
 \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>:
-<math>L = \mathrm{dom}(s'') \setminus \mathrm{dom}(s)</math>:
 <math>
@@ Linia 309: / Linia 248: @@
 </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>.
-Niech deklaracja zwraca, oprócz pary <math>(E', s')</math>,
+Oto poprawione reguły dla deklaracji:
-dodatkowo zbiór <math>L</math>.
-Oto poprawione regu³y dla deklaracji:
@@ Linia 327: / Linia 264: @@
 E \,\vdash\, \mathbf{proc}\, x_1(x_2);\, I, s \,\longrightarrow\, (E', s, \emptyset)
 \quad \mbox{ gdzie }
-E' = E[x_1 \mapsto \langle x_2, I, E \rangle].
+E' = E[x_1 \mapsto \langle x_2, I, E \rangle]</math>
-</math>
 <math>
@@ Linia 337: / Linia 273: @@
 </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 343: / Linia 279: @@
        \quad \quad
        E' \,\vdash\, I, s' \,\longrightarrow\, s''
+      \quad \quad
        s'', L \,\longrightarrow\, \bar{s}}
       {E \,\vdash\, \mathbf{begin}\, d;\, I \,\mathbf{end}, s \,\longrightarrow\, \bar{s}}
@@ Linia 348: / Linia 285: @@
 </div></div>
-}}
-{{cwiczenie|2 (wi±zanie dynamiczne)|cw2|
-Zastanówmy siê, jakich modyfikacji wymaga nasza semantyka,
+{{cwiczenie|2 (wiązanie dynamiczne)|cw2|
-aby wi±zanie identyfikatorów by³o dynamiczne, zamiast statycznego.
-Rozumiemy przez to, ¿e w przypadku odwo³ania do zmiennej
+Zastanówmy się, jakich modyfikacji wymaga nasza semantyka, aby wiązanie identyfikatorów było dynamiczne zamiast statycznego.
-wewn±trz procedury, odwo³ujemy siê do ¶rodowiska w miejscu
+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.
-wywo³ania tej procedury, zamiast do ¶rodowiska z miejsca
+Tak samo powinno być w przypadku wywołania innej procedury wewnątrz procedury, czyli wiązanie dynamiczne dotyczy i zmiennych i procedur.
-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.
 }}
@@ Linia 368: / Linia 299: @@
 }}
-  <math>\mathbf{begin}\,</math>
+  <math>\mathbf{begin}\ </math>,
-    <math>\mathbf{var}\,</math> x = 1;
+    <math>\mathbf{var}\ </math>, x = 1;
-    <math>\mathbf{proc}\,</math> p(y); y := y+x;
+    <math>\mathbf{proc}\ </math>, p(y); y := y+x;
-    <math>\mathbf{begin}\,</math>
+    <math>\mathbf{begin}\ </math>,
-      <math>\mathbf{var}\,</math> x = 10; <math>\mathbf{var}\,</math> z = 0;
+      <math>\mathbf{var}\ </math>, x = 10; <math>\mathbf{var}\ </math>, z = 0;
-      <math>\mathbf{call}\,</math> p(z);
+      <math>\mathbf{call}\ </math>, p(z);
     <math>\,\mathbf{end}</math>
   <math>\,\mathbf{end}</math>
-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:
-  <math>\mathbf{begin}\,</math>
+  <math>\mathbf{begin}\ </math>,
-    <math>\mathbf{proc}\,</math> q(x); x := x+1;
+    <math>\mathbf{proc}\ </math>, q(x); x := x+1;
-    <math>\mathbf{proc}\,</math> p(y); <math>\mathbf{call}\,</math> q(y); <math>\mathbf{call}\,</math> q(y);
+    <math>\mathbf{proc}\ </math>, p(y); <math>\mathbf{call}\ </math>, q(y); <math>\mathbf{call}\ </math>, q(y);
-    <math>\mathbf{begin}\,</math>
+    <math>\mathbf{begin}\ </math>,
-      <math>\mathbf{proc}\,</math> q(x); x := x+x;
+      <math>\mathbf{proc}\ </math>, q(x); x := x+x;
-      <math>\mathbf{var}\,</math> z = 2;
+      <math>\mathbf{var}\ </math>, z = 2;
-      <math>\mathbf{call}\,</math> p(z);
+      <math>\mathbf{call}\ </math>, p(z);
     <math>\,\mathbf{end}</math>
   <math>\,\mathbf{end}</math>
-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 przy wiązaniu statycznych, a wykonuje się poprawnie przy dynamicznym:
-A oto przyk³ad programu, który nie wykona³by siê poprawnie
-przy wi±zaniu statycznych, a wykonuje siê poprawnie przy
-dynamicznym:
-  <math>\mathbf{begin}\,</math>
+  <math>\mathbf{begin}\ </math>,
-    <math>\mathbf{proc}\,</math> q(x); <math>\mathbf{call}\,</math> r(x);
+    <math>\mathbf{proc}\ </math>, q(x); <math>\mathbf{call}\ </math>, r(x);
-    <math>\mathbf{proc}\,</math> p(y);
+    <math>\mathbf{proc}\ </math>, p(y);
-      <math>\mathbf{begin}\,</math>
+      <math>\mathbf{begin}\ </math>,
-        <math>\mathbf{proc}\,</math> r(x); x := x+x;
+        <math>\mathbf{proc}\ </math>, r(x); x := x+x;
-        <math>\mathbf{call}\,</math> q(x);
+        <math>\mathbf{call}\ </math>, q(x);
       <math>\,\mathbf{end}</math>
-    <math>\mathbf{var}\,</math> z = 7;
+    <math>\mathbf{var}\ </math>, z = 7;
-    <math>\mathbf{call}\,</math> p(z);
+    <math>\mathbf{call}\ </math>, p(z);
   <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>q</math>,
+Procedura <math>p</math> wywołuje procedurę <math>q</math> "przekazując" jej również środowisko z miejsca wołania, zawierające informację o procedurze <math>r</math>.
-,,przekazuj±c" jej równie¿ ¶rodowisko z miejsca wo³ania,
+Ta ostatnia przy widoczności statycznej byłaby lokalna, a teraz nie jest.
-zawieraj±ce informacjê o procedurze <math>r</math>. Ta ostatnia
-przy widoczno¶ci statycznej by³aby lokalna, a teraz nie jest.
-{{rozwiazanie||roz2|
+<div class="mw-collapsible mw-made=collapsible mw-collapsed">
+<span class="mw-collapsible-toogle mw-collapsible-toogle-default style="font-variant:small-caps">Rozwiązanie</span>
+<div class="mw-collapsible-content" style="display:none">
-<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 438: / Linia 363: @@
 \quad \mbox{ o ile }
 E(x_1) = \langle x, I, E' \rangle \in \mathbf{Proc} \mbox{ i }
-E(x_2) = l \in \mathbf{Loc}
+E(x_2) = l \in \mathbf{Loc}</math>
-</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 niego użyjemy bieżącego środowiska <math>E</math> (czyli środowiska z miejsca wywołania):
-Wystarczy wiêc, je¶li zignorujemy to ¶rodowisko, a zamiast
-niego u¿yjemy bie¿±cego ¶rodowiska <math>E</math> (czyli ¶rodowiska
-z miejsca wywo³ania):
 <math>
@@ Linia 452: / Linia 373: @@
 \quad \mbox{ o ile }
 E(x_1) = \langle x, I, E' \rangle \in \mathbf{Proc} \mbox{ i }
-E(x_2) = l \in \mathbf{Loc}
+E(x_2) = l \in \mathbf{Loc}</math>
-</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ę?
-mogliby¶my post±piæ tak jak poprzednio, np.
+Moglibyśmy postąpić tak jak poprzednio, np.
 <math>
@@ Linia 469: / Linia 388: @@
 </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".
-¿e ,,przelewamy z pustego w pró¿ne". Sci¶lej,
+Sciślej, dodajemy do <math>E</math> parę <math>x_1 \mapsto \langle x, I \rangle</math>, która już tam tak naprawdę jest!
-dodajemy do <math>E</math> parê <math>x_1 \mapsto \langle x, I \rangle</math>,
+Okazuje się, że dzięki dynamicznemu wiązaniu identyfikatorów "za darmo" otrzymujemy rekurencje! Tak jest na przykład w programie:
-która ju¿ tam tak naprawdê jest!
-Okazuje siê, ¿e dziêki dynamicznemu wi±zaniu identyfikatorów ,,za
-darmo" otrzymujemy rekurencje! Tak jest na przyk³ad w programie:
-  <math>\mathbf{begin}\,</math>
+  <math>\mathbf{begin}\ </math>,
-    <math>\mathbf{proc}\,</math> p(x); <math>\mathbf{if}\,</math> x < 100 <math>\,\mathbf{then}\,</math> x := x+x; <math>\mathbf{call}\,</math> p(x) <math>\,\mathbf{else}\, \mathbf{skip}</math>;
+    <math>\mathbf{proc}\ </math>, p(x); <math>\mathbf{if}\ </math>, x < 100 <math>\,\mathbf{then}\ </math>, x := x+x; <math>\mathbf{call}\ </math>, p(x) <math>\,\mathbf{else}\, \mathbf{skip}</math>;
-    <math>\mathbf{var}\,</math> z = 8;
+    <math>\mathbf{var}\ </math>, z = 8;
-    <math>\mathbf{call}\,</math> p(z);
+    <math>\mathbf{call}\ </math>, p(z);
   <math>\,\mathbf{end}</math>
-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>
-}}
-{{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).
-przypisywana parametrowi formalnemu (tak jak przy przekazywaniu
+Ale po zakończeniu procedury, wartość parametru formalnego, która mogła zmienić się w czasie dzialania procedury, jest z powrotem przypisywana na zmienną będącą parametrem aktualnym (a więc podobnie do przekazywania przez zmienną).
-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.
 }}
-{{rozwiazanie|(przekazywanie parametru przez warto¶æ)|roz1|
-<div class="mw-collapsible mw-made=collapsible mw-collapsed"><div class="mw-collapsible-content" style="display:none">
+<div class="mw-collapsible mw-made=collapsible mw-collapsed">
+<span class="mw-collapsible-toogle mw-collapsible-toogle-default style="font-variant:small-caps">Rozwiązanie (przekazywanie parametru przez wartość)</span>
+<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 437: @@
 </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 wartość parametru aktualnego i umieszczamy ją w tej lokacji:
-któr± przypiszemy parametrowi formalnemu; nastêpnie obliczamy
-warto¶æ parametru aktualnego i umieszczamy j± w tej lokacji:
 <math>
@@ Linia 543: / Linia 450: @@
 </div></div>
-}}
-{{rozwiazanie|(przekazywanie parametru in-out)|roz3.2|
-<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
+<div class="mw-collapsible mw-made=collapsible mw-collapsed">
-warto¶æ: alokujemy now± lokacjê <math>l</math>, któr± przypiszemy
+<span class="mw-collapsible-toogle mw-collapsible-toogle-default style="font-variant:small-caps">Rozwiązanie (przekazywanie parametru in-out)</span>
-parametrowi formalnemu, i umieszczamy w niej warto¶æ zmiennej
+<div class="mw-collapsible-content" style="display:none">
-(<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
+Początkowo postępujemy tak jak w przypadku przekazywania przez wartość: alokujemy nową lokację <math>l</math>, którą przypiszemy parametrowi formalnemu i umieszczamy w niej wartość zmiennej  (<math>x_2</math> w regule poniżej) będącej parametrem aktualnym.
-<math>l</math> powinna zostaæ spowrotem przypisana zmiennej <math>x_2</math>.
+Zasadnicza różnica widoczna jest po zakończeniu procedury: wartość z lokacji <math>l</math> powinna zostać spowrotem przypisana zmiennej <math>x_2</math>.
-Oto regu³a:
+Oto reguła:
 <math>
@@ Linia 562: / Linia 466: @@
 \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 }
+</math>
-l = \mathtt{newloc}(s)
+<math>
-</math>
+E(x_1) = \langle x, I, E' \rangle \in \mathbf{Proc} \mbox{ i } l = \mathtt{newloc}(s)</math>
 </div></div>
-}}
 == Zadania domowe ==
@@ Linia 576: / Linia 478: @@
 {{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 mogą się wzajemniej wywoływać bez żadnych ograniczeń.
-To znaczy, ¿e procedury zadeklarowane w jednej deklaracji równoleg³ej
-mog± siê wzajemniej wywo³ywaæ bez ¿adnych ograniczeñ.
 }}
@@ Linia 585: / Linia 485: @@
 {{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>
 e \, ::= \,\,
            \ldots \,\,|\,\,
-           \mathbf{call}\, x_1(x_2).
+           \mathbf{call}\, x_1(x_2)</math>
-</math>
-Wewnatrz funkcji jej nazwa mozna poslugiwac sie jak
+Wewnątrz funkcji jej nazwą można posługiwać się jak zmienną lokalną.
-zmienna lokalna.
+Wynik zwracany przez funkcję to wartość tej zmiennej w momencie wyjścia z funkcji.
-Wynik zwracany przez funkcje <math>x_1</math> to wartosc
-tej zmiennej w momencie wyjscia z funkcji.
 Uwaga na efekty uboczne!
@@ Linia 606: / Linia 502: @@
 {{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 dynamiczne, a procedur statyczne.
 }}
@@ Linia 615: / Linia 511: @@
 {{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.
 }}