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

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
← poprzednia edycjanastępna edycja →
WizualnieWikikod
Sl (dyskusja | edycje)
101 edycji
Nie podano opisu zmian
Dorota (dyskusja | edycje)
376 edycji
Nie podano opisu zmian
Linia 1: Linia 1:


== Zawartość ==
== Zawartość ==


Ostatnie zajęcia poświęcone semantyce naturalnej.
Ostatnie zajęcia poświęcone semantyce naturalnej.
Rozszerzymy język Tiny o deklaracje zmiennych i procedur z jednym parametrem.
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.
Rozważymy statyczną i dynamiczną widoczność (wiązanie) identyfikatorów oraz różne mechanizmy przekazywania parametrów.
Pracujemy ze środowiskami i stanami.
Pracujemy ze środowiskami i stanami.
Linia 14: Linia 13:
{{cwiczenie|1 (procedury)|cw1|
{{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>
<math>
Linia 31: Linia 30:


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>.
Konstrukcja <math>\mathbf{proc}\, x_1(x_2)</math> deklaruje procedurę o nazwie <math>x_1</math>, której parametrem formalnym jest <math>x_2</math>.
Zakładamy statyczne wiązanie identyfikatorów i przekazywanie 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 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>.
Instrukcja <math>\mathbf{call}\, x_1(x_2)</math> wywołuje procedurę <math>x_1</math> z parametrem aktualnym <math>x_2</math>.
}}
}}
Linia 40: Linia 39:
<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"><div class="mw-collapsible-content" style="display:none">


Użyjemu środowisk <math>E \in \mathbf{Env}</math> i stanów <math>s \in \mathbf{Store}</math>:
Użyjemy środowisk <math>E \in \mathbf{Env}</math> i stanów <math>s \in \mathbf{Store}</math>:


<math>
<math>
Linia 49: Linia 48:


Nowym elementem jest zbiór <math>\mathbf{Proc}</math>, potrzebny nam do przechowywania informacji o procedurach.  
Nowym elementem jest zbiór <math>\mathbf{Proc}</math>, potrzebny nam do przechowywania informacji o procedurach.  
Informacja nt procedury, którą musimy przechowywać, to:
Informacja na temat procedury, którą musimy przechowywać, to:


* nazwa parametru formalnego,
* nazwa parametru formalnego,
Linia 100: Linia 99:
Zauważmy, że deklaracja procedury nie zmienia stanu, tylko środowisko, w odróżnieniu od deklaracji zmiennej.
Zauważmy, że deklaracja procedury nie zmienia stanu, tylko środowisko, 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ą 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.
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:
Aby dokończyć semantykę deklaracji potrzebujemy jeszcze jednej reguły:


Linia 110: Linia 109:
</math>
</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?
Linia 149: Linia 148:


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.
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.
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>.  
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?
Linia 211: Linia 210:
'''Pytanie:''' Który w którym?
'''Pytanie:''' Który w którym?


Semantyka pozostałych instrukcji i wyrażeń języka Tiny pozostaje bez zmian.
Semantyka pozostałych instrukcji i wyrażeń języka TINY pozostaje bez zmian.


Rozważmy na koniec problem dealokacji.
Rozważmy na koniec problem dealokacji.
Linia 219: Linia 218:
<br>
<br>


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.
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>.
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>.


Linia 255: Linia 254:
</math>
</math>


albo możemy poprosić o pomoc w posprzątaniu tego, kto ,,nabałaganił", czyli deklarację <math>d</math>.
albo możemy poprosić o pomoc w posprzątaniu tego, kto "nabałaganił", czyli 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:
Oto poprawione reguły dla deklaracji:
Linia 297: Linia 296:
{{cwiczenie|2 (wiązanie dynamiczne)|cw2|
{{cwiczenie|2 (wiązanie dynamiczne)|cw2|


Zastanówmy się, jakich modyfikacji wymaga nasza semantyka, aby wiązanie identyfikatorów było dynamiczne, zamiast statycznego.
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.
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.
Tak samo powinno być w przypadku wywołania innej procedury wewnątrz procedury, czyli wiązanie dynamiczne dotyczy i zmiennych i procedur.
Linia 356: Linia 355:


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>, ,,przekazując" jej również środowisko z miejsca wołania, zawierające informację o procedurze <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>.  
Ta ostatnia przy widoczności statycznej byłaby lokalna, a teraz nie jest.
Ta ostatnia przy widoczności statycznej byłaby lokalna, a teraz nie jest.


Linia 398: Linia 397:
</math>
</math>


ale jeśli uważnie przyjrzymy się tej regule, to okazuje się, że ,,przelewamy z pustego w próżne".  
ale jeśli uważnie przyjrzymy się tej regule, to okazuje się, że "przelewamy z pustego w próżne".  
Sciślej, dodajemy do <math>E</math> parę <math>x_1 \mapsto \langle x, I \rangle</math>, która już tam tak naprawdę jest!
Sciślej, dodajemy do <math>E</math> parę <math>x_1 \mapsto \langle x, I \rangle</math>, 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:
Okazuje się, że dzięki dynamicznemu wiązaniu identyfikatorów "za darmo" otrzymujemy rekurencje! Tak jest na przykład w programie:




Linia 430: Linia 429:
Należy wyjaśnić ostatni mechanizm (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).
Parametrem aktualnym jest zmienna, której wartość jest przypisywana parametrowi formalnemu (tak jak przy przekazywaniu przez wartość, gdy parametrem aktualnym jest zmienna).
Ale po zakończeniu procedury, wartość parametru formalnego, która mogła zmienić się w czasie dzialania procedury, jest spowrotem przypisywana na zmienną będącą parametrem aktualnym (a więc podobnie do przekazywania przez zmienną).
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.
Parametr formalny jest traktowany jak zmienna lokalna procedury.
}}
}}
Linia 466: Linia 465:
<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"><div class="mw-collapsible-content" style="display:none">


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.
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.
Zasadnicza różnica widoczna jest po zakończeniu procedury: wartość z lokacji <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:
Linia 490: Linia 489:
{{cwiczenie|1|cw1.dom|
{{cwiczenie|1|cw1.dom|


Zaadaptuj semantykę ,,deklaracji równoległych" dla rekurencji wzajemnej wewnątrz jednej deklaracji równoległej.
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ń.
To znaczy, że procedury zadeklarowane w jednej deklaracji równoległej mogą się wzajemniej wywoływać bez żadnych ograniczeń.
}}
}}
Linia 517: Linia 516:
Rozważ następujące warianty:
Rozważ następujące warianty:


* wiązanie zmiennych jest statyczne a procedur dynamiczne
* wiązanie zmiennych jest statyczne, a procedur dynamiczne
* wiązanie zmiennych jest dymamiczne a procedur statyczne.
* wiązanie zmiennych jest dymamiczne, a procedur statyczne.
}}
}}


Wersja z 14:51, 29 wrz 2006

Zawartość

Ostatnie zajęcia poświęcone semantyce naturalnej. Rozszerzymy język TINY o deklaracje zmiennych i procedur z jednym parametrem. Rozważymy statyczną i dynamiczną widoczność (wiązanie) identyfikatorów oraz różne mechanizmy przekazywania parametrów. Pracujemy ze środowiskami i stanami.


Semantyka naturalna procedur

Ćwiczenie 1 (procedury)

Rozszerzmy język TINY o deklaracje i wywołania procedur:

I::=…|𝐛𝐞𝐠𝐢𝐧d;I𝐞𝐧𝐝|𝐜𝐚𝐥𝐥x1(x2)

d::=𝐯𝐚𝐫x=e|𝐩𝐫𝐨𝐜x1(x2);I|d1;d2

Konstrukcja 𝐩𝐫𝐨𝐜x1(x2) deklaruje procedurę o nazwie x1, której parametrem formalnym jest x2. 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 𝐜𝐚𝐥𝐥x1(x2) wywołuje procedurę x1 z parametrem aktualnym x2.


Rozwiązanie

{{{3}}}

Ćwiczenie 2 (wiązanie dynamiczne)

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


Przykład

Spójrzmy na kilka prostych programów. 

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

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

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


Wartość końcowa zmiennej z=10. Gdyby wiązanie zmiennej x było statyczne, to wartość ta wynosiłaby 1. Podobnie dla procedur: 


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

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

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


Wartość końcowa zmiennej z=8. Gdyby widoczność procedury q była statyczna, to wartość ta wynosiłaby 4. A oto przykład programu, który nie wykonałby się poprawnie przy wiązaniu statycznych, a wykonuje się poprawnie przy dynamicznym: 


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

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

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


Wartość końcowa zmiennej z wynosi 14. Procedura p wywołuje procedurę q "przekazując" jej również środowisko z miejsca wołania, zawierające informację o procedurze r. Ta ostatnia przy widoczności statycznej byłaby lokalna, a teraz nie jest.


Rozwiązanie

{{{3}}}


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

Rozważ inne mechanizmy przekazywania parametru (wiązanie statyczne):

  • przez wartość
  • in-out

Należy wyjaśnić ostatni mechanizm (in-out). Parametrem aktualnym jest zmienna, której wartość jest przypisywana parametrowi formalnemu (tak jak przy przekazywaniu przez wartość, gdy parametrem aktualnym jest zmienna). Ale po zakończeniu procedury, wartość parametru formalnego, która mogła zmienić się w czasie dzialania procedury, jest 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ść)

{{{3}}}

Rozwiązanie (przekazywanie parametru in-out)

{{{3}}}


Zadania domowe

Ćwiczenie 1

Zaadaptuj semantykę "deklaracji równoległych" dla rekurencji wzajemnej wewnątrz jednej deklaracji równoległej. To znaczy, że procedury zadeklarowane w jednej deklaracji równoległej mogą się wzajemniej wywoływać bez żadnych ograniczeń.


Ćwiczenie 2

Zamiast procedur, rozważ funkcje z pojedynczym parametrem przekazywanym przez zmienną. Wywołanie funkcji może teraz pojawić się wewnątrz wyrażenia:

e::=…|𝐜𝐚𝐥𝐥x1(x2).

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 dymamiczne, a procedur statyczne.


Ćwiczenie 4

Rozszerz semantykę procedur tak, aby parametrem aktualnym procedury mogła być procedura.

Źródło: „https://wazniak.mimuw.edu.pl/index.php?title=Semantyka_i_weryfikacja_programów/Ćwiczenia_6&oldid=59814”