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.
-Rozszerzymy język Tiny o deklaracje zmiennych i procedur z jednym
+Rozszerzymy język TINY o deklaracje zmiennych i procedur z jednym parametrem.
-parametrem.
+Rozważymy statyczną i dynamiczną widoczność (wiązanie) identyfikatorów oraz różne mechanizmy przekazywania parametrów.
-Rozważymy statyczną i dynamiczną widoczność (wiązanie)
-identyfikatorów oraz różne mechanizmy przekazywania
-parametrów.
 Pracujemy ze środowiskami i stanami.
-== Zadania z rozwiązaniami ==
+== Semantyka naturalna procedur ==
-==== Zadanie 1 (procedury) ====
+{{cwiczenie|1 (procedury)|cw1|
-Rozważmy język Small, będący
+Rozszerzmy język TINY o deklaracje i wywołania procedur:
-rozszerzeniem języka Tiny o deklaracje i wywołania procedur:
 <math>
@@ Linia 34: / Linia 28: @@
 </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>.
-<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>
-a parametrem aktualnym <math> x_2 </math>.
-==== Rozwiązanie ====
+<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">
-Użyjemu środowisk <math> E \in \mathbf{Env} </math> i stanów <math> s \in \mathbf{State} </math>:
+Użyjemy środowisk <math>E \in \mathbf{Env}</math> i stanów <math>s \in \mathbf{Store}</math>:
 <math>
-\mathbf{State} = \mathbf{Loc} \to_{\mathrm{fin}} \mathbf{Num}
+\mathbf{Store} = \mathbf{Loc} \to_{\mathrm{fin}} \mathbf{Num}
 \quad \quad \quad
-\mathbf{Env}= \mathbf{Var} \to_{\mathrm{fin}} (\mathbf{Loc} \cup PROC).
+\mathbf{Env}= \mathbf{Var} \to_{\mathrm{fin}} (\mathbf{Loc} \cup \mathbf{Proc})</math>
-</math>
-Nowym elementem jest zbiór <math> 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.
-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> 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> PROC = \mathbf{Var} \times \mathbf{Stmt} \times \mathbf{Env} </math>.
+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.
+Czyli znów zbiór <math>\mathbf{Env}</math> zadany jest przez równanie.
 Nasze tranzycje będą następujących postaci:
@@ Linia 89: / Linia 74: @@
 </math>
-Na uwagę zasłyguje 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>.
-Zaczniemy od nowych semantyki dla nowych konstrukcji języka, natomiast
-semantykę samego języka Tiny opartą na środowiskach i stanach
-przedyskutujemy krótko na końcu rozwiązania.
 Zajmijmy się najpierw deklaracjami zmiennych:
@@ Linia 102: / Linia 81: @@
 <math>
 \frac{E \,\vdash\, e, s \,\longrightarrow\, n}
-      {E \,\vdash\, \mathbf{var}\, x=e, s \,\longrightarrow\, (E', s')
+      {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],\,
+                     s' = s[l \mapsto n],\,
-                           l = \mathtt{new}(s)}
+                     l = \mathtt{newloc}(s)
 </math>
@@ Linia 113: / 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óznieniu 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
-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:
@@ Linia 133: / 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?
@@ Linia 146: / 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ść
-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:
@@ Linia 174: / Linia 140: @@
       {E \,\vdash\, \mathbf{call}\, x_1(x_2), s \,\longrightarrow\, s'}
 \quad \mbox{ o ile }
-E(x_1) = \langle x, I, E' \rangle \in PROC \mbox{ i }
+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
+'''Pytanie:''' czy powyższa reguła dopuszcza rekurencyjne wywołania procedury?
-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.
-E'[x \mapsto l] 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 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 204: / Linia 156: @@
       {E \,\vdash\, \mathbf{call}\, x_1(x_2), s \,\longrightarrow\, s'}
 \quad \mbox{ o ile }
-E(x_1) = \langle x, I, E' \rangle \in PROC \mbox{ i }
+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ę,
-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 <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ść:
@@ Linia 228: / Linia 174: @@
       {E \,\vdash\, \mathbf{call}\, x_1(x_2), s \,\longrightarrow\, s'}
 \quad \mbox{ o ile }
-E(x_1) = \langle x, I, E' \rangle \in PROC \mbox{ i }
+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?
@@ Linia 236: / Linia 181: @@
 Okazuje się, że tak nie jest, oto dwa kontrprzykłady:
-<math>
-\mathbf{begin}\,\\
-\quad \mathbf{Var} y = 7;\\
-\quad proc x(x);\, x := x+1;\\
-\ \\
-\quad x(y);\\
-\,\mathbf{end}
-</math>
-<math>
+ <math>\mathbf{begin}\ </math>,
-\mathbf{begin}\,\\
+   <math>\mathbf{var}\ </math>, y = 7;
-\quad \mathbf{Var} y = 7;\\
+   <math>\mathbf{proc}\ </math>, x(x); x := x+1;
-\quad proc x(x);\, \mathbf{if}\,
-\quad \quad \mathbf{if}\, y > 0 \,\mathbf{then}\, y := y-1;\, \mathbf{call}\, x(y) \,\mathbf{else}\, \mathbf{skip};\\
+   <math>\mathbf{call}\ </math>, x(y);
-\ \\
+ <math>\,\mathbf{end}</math>
-\quad x(y);\\
-\,\mathbf{end}
-</math>
+ <math>\mathbf{begin}\ </math>,
+   <math>\mathbf{var}\ </math>, y = 7;
+   <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{call}\ </math>, x(y);
+ <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żen 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.
+<br>
+'''Wariant (dealokacja)'''
+<br>
-===== 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 <math>d</math>.
-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 <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 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.
-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 298: / Linia 237: @@
 </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 = \dom(s'') \setminus \dom(s) </math>:
 <math>
@@ Linia 307: / Linia 245: @@
        s'', L \,\longrightarrow\, \bar{s}}
       {E \,\vdash\, \mathbf{begin}\, d;\, I \,\mathbf{end}, s \,\longrightarrow\, \bar{s}}
-\quad \mbox{ gdzie } L = \dom(s'') \setminus \dom(s)
+\quad \mbox{ gdzie } L = \mathrm{dom}(s'') \setminus \mathrm{dom}(s)
 </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>,
-dodatkowo zbiór <math> L </math>.
 Oto poprawione reguły dla deklaracji:
@@ Linia 320: / Linia 256: @@
 \frac{E \,\vdash\, e, s \,\longrightarrow\, n}
       {E \,\vdash\, \mathbf{var}\, x=e, s \,\longrightarrow\, (E', s', \{ l \})
-       \quad \mbox{ gdzie } E' = E[x mapsto l],\,
+       \quad \mbox{ gdzie } E' = E[x \mapsto l],\,
                             s' = s[l \mapsto n],\,
-                            l = \mathtt{new}(s)}
+                            l = \mathtt{newloc}(s)}
 </math>
@@ Linia 328: / 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 344: / 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}}
 </math>
+</div></div>
+{{cwiczenie|2 (wiązanie dynamiczne)|cw2|
+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.
+}}
+{{przyklad|||
+Spójrzmy na kilka prostych programów.
+}}
+ <math>\mathbf{begin}\ </math>,
+   <math>\mathbf{var}\ </math>, x = 1;
+   <math>\mathbf{proc}\ </math>, p(y); y := y+x;
+   <math>\mathbf{begin}\ </math>,
+     <math>\mathbf{var}\ </math>, x = 10; <math>\mathbf{var}\ </math>, z = 0;
+     <math>\mathbf{call}\ </math>, p(z);
+   <math>\,\mathbf{end}</math>
+ <math>\,\mathbf{end}</math>
+Wartość końcowa zmiennej <math>z = 10</math>.
+Gdyby wiązanie zmiennej <math>x</math> było statyczne, to wartość ta wynosiłaby <math>1</math>. Podobnie dla procedur:
-==== Zadanie 2 (wiązanie dynamiczne) ====
-Zastanówmy się, jakich modyfikacji wymaga nasza semantyka,
+ <math>\mathbf{begin}\ </math>,
-aby wiązanie identyfikatorów było dynamiczne, zamiast statycznego.
+   <math>\mathbf{proc}\ </math>, q(x); x := x+1;
-Rozumiemy przez to, że w przypadku odwołania do zmiennej
+   <math>\mathbf{proc}\ </math>, p(y); <math>\mathbf{call}\ </math>, q(y); <math>\mathbf{call}\ </math>, q(y);
-wewnątrz procedury, odwułujemy się do środowiska w miejscu
-wywołania tej procedury, zamiast do środowiska z miejsca
+   <math>\mathbf{begin}\ </math>,
-deklaracji jak dotychczas.
+     <math>\mathbf{proc}\ </math>, q(x); x := x+x;
-Tak samo powinno być w przypadku wywołania innej procedury
+     <math>\mathbf{var}\ </math>, z = 2;
-wewnątrz procedury, czyli wiązanie dynamiczne dotyczy i zmiennych
-i procedur.
+     <math>\mathbf{call}\ </math>, p(z);
-Oto przykład:
+   <math>\,\mathbf{end}</math>
+ <math>\,\mathbf{end}</math>
-<math>
-\mathbf{begin}\,\\
-\quad \mathbf{var}\, x = 1;\\
-\quad \mathbf{proc}\, p(y);\, y := y+x;\\
-\ \\
-\quad \mathbf{begin}\,\\
-\quad \quad \mathbf{var}\, x = 10;\\
-\quad \quad \mathbf{var}\, z = 0;\\
-\ \\
-\quad \quad \mathbf{call}\, p(z);
-\quad \,\mathbf{end}\\
-\,\mathbf{end}
-</math>
-Wartość końcowa zmiennej <math> z = 10 </math>.
+Wartość końcowa zmiennej <math>z = 8</math>.
-Gdyby wiązanie zmiennej <math> x </math> było statyczne, to wartość ta
+Gdyby widoczność procedury <math>q</math> była statyczna, to wartość ta wynosiłaby <math>4</math>.
-wynosiłaby <math> 1 </math>. Podobnie dla procedur:
+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}\,\\
-\quad \mathbf{proc}\, q(x);\, x := x+1;\\
-\quad \mathbf{proc}\, p(y);\, \mathbf{call}\, q(y); \mathbf{call}\, q(y);\\
-\ \\
-\quad \mathbf{begin}\,\\
-\quad \quad \mathbf{proc}\, q(x);\, x := x+x;\\
-\quad \quad \mathbf{var}\, z = 2;\\
-\ \\
-\quad \quad \mathbf{call}\, p(z);
-\quad \,\mathbf{end}\\
-\,\mathbf{end}
-</math>
-Wartość końcowa zmiennej <math> z = 8 </math>.
+ <math>\mathbf{begin}\ </math>,
-Gdyby widoczność procedury <math> q </math> była statyczna, to wartość ta
+   <math>\mathbf{proc}\ </math>, q(x); <math>\mathbf{call}\ </math>, r(x);
-wynosiłaby <math> 4 </math>.
+   <math>\mathbf{proc}\ </math>, p(y);
-A oto przykład programu, który nie wykonałby się poprawnie
+     <math>\mathbf{begin}\ </math>,
-przy wiązaniu statycznych, a wykonuje się poprawnie przy
+       <math>\mathbf{proc}\ </math>, r(x); x := x+x;
-dynamicznym:
+       <math>\mathbf{call}\ </math>, q(x);
+     <math>\,\mathbf{end}</math>
+   <math>\mathbf{var}\ </math>, z = 7;
+   <math>\mathbf{call}\ </math>, p(z);
+ <math>\,\mathbf{end}</math>
-<math>
-\mathbf{begin}\,\\
-\quad \mathbf{proc}\, q(x);\, \mathbf{call}\, r(x);\\
-\quad \mathbf{proc}\, p(y);\\
-\quad \quad \mathbf{begin}\,\\
-\quad \quad \quad \mathbf{proc}\, r(x);\, x := x+x;\\
-\ \\
-\quad \quad \quad q(x);
-\quad \quad \,\mathbf{end}\\
-\quad \mathbf{var}\, z = 7;
-\ \\
-\quad \mathbf{call}\, p(z);
-\,\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, 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>, która
-przy widoczności statycznej byłaby lokalna, a teraz nie jest.
-==== Rozwiązanie ====
+<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">
 Spójrzmy na regułę dla wywołania procedury:
@@ Linia 431: / Linia 362: @@
       {E \,\vdash\, \mathbf{call}\, x_1(x_2), s \,\longrightarrow\, s'}
 \quad \mbox{ o ile }
-E(x_1) = \langle x, I, E' \rangle \in PROC \mbox{ i }
+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 445: / Linia 372: @@
       {E \,\vdash\, \mathbf{call}\, x_1(x_2), s \,\longrightarrow\, s'}
 \quad \mbox{ o ile }
-E(x_1) = \langle x, I, E' \rangle \in PROC \mbox{ i }
+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 459: / Linia 384: @@
       {E \,\vdash\, \mathbf{call}\, x_1(x_2), s \,\longrightarrow\, s'}
 \quad \mbox{ o ile }
-E(x_1) = \langle x, I \rangle \in PROC \mbox{ i }
+E(x_1) = \langle x, I \rangle \in \mathbf{Proc} \mbox{ i }
 E(x_2) = l \in \mathbf{Loc}
 </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{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{call}\ </math>, p(z);
+ <math>\,\mathbf{end}</math>
-<math>
+ponieważ w momencie wywołania rekurencyjnego <math>\mathbf{call}\, p(x)</math>, w środowisku jest już informacja nt. procedury <math>p</math>!
-\mathbf{begin}\,\\
-\quad \mathbf{proc}\, p(x);\, \mathbf{if}\, x < 100 \,\mathbf{then}\, x := x+x; \mathbf{call}\, p(x) \,\mathbf{else}\, \mathbf{skip};\\
-\quad \mathbf{var}\, z = 8;
-\ \\
-\quad \mathbf{call}\, p(z);
-\,\mathbf{end}
-</math>
-ponieważ w momencie wywołania rekurencyjnego <math> \mathbf{call}\, p(x) </math>,
+</div></div>
-w środowisku jest już informacja nt. procedury <math> p </math>!
-==== Zadanie 3 (różne mechanizmy przekazywana parametru) ====
+{{cwiczenie|3 (różne mechanizmy przekazywana parametru)|cw3|
-Rozważ inne mechanizmy przekazywania parametru w języku Small
+Rozważ inne mechanizmy przekazywania parametru (wiązanie statyczne):
-(wiązanie statyczne):
 * przez wartość
@@ Linia 496: / Linia 418: @@
 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.
+}}
-==== Rozwiązanie ====
-===== Przekazywanie przez wartość =====
+<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ż popzrzednio:
 <math>
@@ Linia 520: / Linia 437: @@
 </math>
-Przed wywołaniem procedury należy zaakolować 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>
 \frac{E \,\vdash\, e, s \,\longrightarrow\, n
-       \quad \quad
+       \quad
        E'[x' \mapsto l] \,\vdash\, I, s[l \mapsto n] \,\longrightarrow\, s'}
       {E \,\vdash\, \mathbf{call}\, x(e), s \,\longrightarrow\, s'}
 \quad \mbox{ o ile }
-E(x) = \langle x', I, E' \rangle \in PROC \mbox{ i }
+E(x) = \langle x', I, E' \rangle \in \mathbf{Proc} \mbox{ i }
-l = \mathtt{new}(s)
+l = \mathtt{newloc}(s)
 </math>
+</div></div>
-===== Przekazywanie in-out =====
+<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 in-out)</span>
+<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 parametrowi formalnemu i umieszczamy w niej wartość zmiennej  (<math>x_2</math> w regule poniżej) będącej parametrem aktualnym.
-wartość: alokujemy nową lokację <math> l </math>, którą przypiszemy
+Zasadnicza różnica widoczna jest po zakończeniu procedury: wartość z lokacji <math>l</math> powinna zostać spowrotem przypisana zmiennej <math>x_2</math>.
-parametrowi formalnemu, i umieszczamy w niej wartość zmiennej
-(<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
-<math> l </math> powinna zostać spowrotem przypisana zmiennej <math> x_2 </math>.
 Oto reguła:
 <math>
 \frac{E'[x \mapsto l] \,\vdash\, I, s[l \mapsto s(l_2)] \,\longrightarrow\, s'}
-      {E \,\vdash\, \mathbf{call}\, x_1(x_2), s \,\longrightarrow\, s'[l_2 \mapsto s(l)]}
+      {E \,\vdash\, \mathbf{call}\, x_1(x_2), s \,\longrightarrow\, s'[l_2 \mapsto s'(l)]}
 \quad \mbox{ o ile }
 E(x_2) = l_2 \in \mathbf{Loc} \mbox{ i }
 s(l_2) \mbox{ jest określone i }
-E(x_1) = \langle x, I, E' \rangle \in PROC \mbox{ i }
+</math>
-l = \mathtt{new}(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 ==
-==== Zadanie 1 ====
+{{cwiczenie|1|cw1.dom|
-Zaadaptuj semantykę języka Small z ,,deklaracjami równoległymi"
+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, procedury zadeklarowane w jednej deklaracji równoległej
+}}
-mogą się wzajemniej wywoływać bez żadnych ograniczeń.
-==== Zadanie 2 ====
+{{cwiczenie|2|cw2.dom|
-Zamiast procedur, rozważ w języku Small 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:
@@ Linia 577: / Linia 491: @@
 e \, ::= \,\,
            \ldots \,\,|\,\,
-           \mathbf{call}\, x_1(x_2)
+           \mathbf{call}\, x_1(x_2)</math>
-</math>
+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!
+}}
+{{cwiczenie|3|cw3.dom|
+Rozważ następujące warianty:
+* wiązanie zmiennych jest statyczne, a procedur dynamiczne
+* wiązanie zmiennych jest dynamiczne, a procedur statyczne.
+}}
-==== Zadanie 3 ====
-Rozważ warianty semantyki języka Small, w którym
+{{cwiczenie|4|cw4.dom|
-* wiązanie zmiennych jest statyczne a procedur dynamiczne
+Rozszerz semantykę procedur tak, aby parametrem aktualnym procedury mogła być procedura.
-* wiązanie zmiennych jest dymamiczne a procedur statyczne
+}}