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

Z Studia Informatyczne
Przejdź do nawigacjiPrzejdź do wyszukiwania
następna edycja →
WizualnieWikikod
Sl (dyskusja | edycje)
101 edycji
Nie podano opisu zmian
 
Sl (dyskusja | edycje)
101 edycji
Nie podano opisu zmian
Linia 15: Linia 15:




==== Zadanie 1 (procedury) ====
{{cwiczenie|1 (procedury)|cw1|


Rozważmy język Small, będący
Rozszerzmy języka Tiny o deklaracje i wywołania procedur:
rozszerzeniem języka Tiny o deklaracje i wywołania procedur:


<math>
<math>
Linia 30: Linia 29:
d \, ::= \,\,
d \, ::= \,\,
     \mathbf{var}\, x = e \,\,|\,\,
     \mathbf{var}\, x = e \,\,|\,\,
     \mathbf{proc}\, x_1(x_2);\, I \,\,|\,\,
     \mathbf{Proc}\, x_1(x_2);\, I \,\,|\,\,
     d_1; \, d_2
     d_1; \, d_2
</math>   
</math>   


Konstrukcja <math> \mathbf{proc}\, x_1(x_2) </math> deklaraje procedurę o nazwie
Konstrukcja <math>\mathbf{Proc}\, x_1(x_2)</math> deklaraje 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
Zakładamy statyczne wiązanie identyfikatorów i przekazywanie
parametrów przez zmienną (to znaczy, że w momencie wywołania
parametrów przez zmienną (to znaczy, że w momencie wywołania
procedury, powinna zostać
procedury, powinna zostać
przekazana lokacja odpowiadająca parametrowi aktualnemu).
przekazana lokacja odpowiadająca parametrowi aktualnemu).
Instrukcja <math> \mathbf{call}\, x_1(x_2) </math> wywołuje procedurę <math> x_1 </math>
Instrukcja <math>\mathbf{call}\, x_1(x_2)</math> wywołuje procedurę <math>x_1</math>
a parametrem aktualnym <math> x_2 </math>.
z parametrem aktualnym <math>x_2</math>.
}}




==== Rozwiązanie ====
{{rozwiazanie||roz1|


Użyjemu środowisk <math> E \in \mathbf{Env} </math> i stanów <math> s \in \mathbf{State} </math>:
<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>:


<math>
<math>
\mathbf{State} = \mathbf{Loc} \to_{\mathrm{fin}} \mathbf{Num}  
\mathbf{Store} = \mathbf{Loc} \to_{\mathrm{fin}} \mathbf{Num}  
\quad \quad \quad
\quad \quad \quad
\mathbf{Env}= \mathbf{Var} \to_{\mathrm{fin}} (\mathbf{Loc} \cup PROC).
\mathbf{Env}= \mathbf{Var} \to_{\mathrm{fin}} (\mathbf{Loc} \cup PROC).
</math>
</math>


Nowym elementem jest zbiór <math> PROC </math>, potrzebny nam do
Nowym elementem jest zbiór <math>PROC</math>, potrzebny nam do
przechowywania informacji o procedurach.  
przechowywania informacji o procedurach.  
Informacja nt procedury, którą musimy przechowywać, to:
Informacja nt procedury, którą musimy przechowywać, to:


* nazwa parametru formalnego,
* 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.


Linia 67: Linia 69:
które wyznacza nam ''wiązanie'' identyfikatorów (nazw
które wyznacza nam ''wiązanie'' identyfikatorów (nazw
zmiennych i procedur) występujących w ciele procedury z  
zmiennych i procedur) występujących w ciele procedury z  
lokacjami (lub opisami procedur z <math> PROC </math>), a więc z konkretnymi  
lokacjami (lub opisami procedur z <math>PROC</math>), a więc z konkretnymi  
zmiennymi (lub procedurami).
zmiennymi (lub procedurami).
Widać tutaj jasno, jak elegancki i wygodny jest podział na środowisko
Widać tutaj jasno, jak elegancki i wygodny jest podział na środowisko
i stan.
i stan.


Zatem niech <math> PROC = \mathbf{Var} \times \mathbf{Stmt} \times \mathbf{Env} </math>.
Zatem niech <math>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:
Nasze tranzycje będą następujących postaci:
Linia 89: Linia 91:
</math>
</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ę
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>.
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:
Zajmijmy się najpierw deklaracjami zmiennych:
Linia 102: Linia 100:
<math>
<math>
\frac{E \,\vdash\, e, s \,\longrightarrow\, n}
\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>
</math>


Linia 111: Linia 109:


<math>
<math>
E \,\vdash\, \mathbf{proc}\, x_1(x_2);\, I, s \,\longrightarrow\, (E', s)
E \,\vdash\, \mathbf{Proc}\, x_1(x_2);\, I, s \,\longrightarrow\, (E', s)
\quad \mbox{ gdzie }
\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].
Linia 117: Linia 115:


Zauważmy, że deklaracja procedury nie zmienia stanu, tylko środowisko,
Zauważmy, że deklaracja procedury nie zmienia stanu, tylko środowisko,
w odróznieniu od deklaracji zmiennej.
w odróżnieniu od deklaracji zmiennej.
W środowisku pamiętamy trójkę <math> \langle x_2, I, E \rangle </math> zawierającą
W środowisku pamiętamy trójkę <math>\langle x_2, I, E \rangle</math> zawierającą
nazwę parametru formalnego, ciało procedury oraz ''środowisko
nazwę parametru formalnego, ciało procedury oraz ''środowisko
deklaracji procedury''.
deklaracji procedury''.
Linia 147: Linia 145:


Czyli instrukcja wewnętrzna wykonywana jest w środowisku (i stanie)
Czyli instrukcja wewnętrzna wykonywana jest w środowisku (i stanie)
''wytworzonym'' (rozszerzonym) przez deklarację <math> d </math>.
''wytworzonym'' (rozszerzonym) przez deklarację <math>d</math>.
Stan końcowy po wykonaniu bloku to po prostu stan końcowy <math> s'' </math>
Stan końcowy po wykonaniu bloku to po prostu stan końcowy <math>s''</math>
po wykonaniu instrukcji wewnętrznej.
po wykonaniu instrukcji wewnętrznej.
Może się to wydawać niepokojące, gdyż oznacza, że nowe lokacje,
Może się to wydawać niepokojące, gdyż oznacza, że nowe lokacje,
powołane podczas deklaracji <math> d </math>, zachowują przechowywaną wartość
powołane podczas deklaracji <math>d</math>, zachowują przechowywaną wartość
również po wyjściu z bloku. Na szczęście wykonanie  
również po wyjściu z bloku. Na szczęście wykonanie  
bloku nie ma wpływu na środowisko, a to ono decyduje, które
bloku nie ma wpływu na środowisko, a to ono decyduje, które
identyfikatory są widoczne (zadeklarowane) i ogólniej, które lokacje
identyfikatory są widoczne (zadeklarowane) i ogólniej, które lokacje
są przypisane identyfikatorom. A więc deklaracja <math> d </math>
są przypisane identyfikatorom. A więc deklaracja <math>d</math>
nie ma wpływu na środowisko, w którym zostaną wykonane kolejne
nie ma wpływu na środowisko, w którym zostaną wykonane kolejne
instrukcje.  
instrukcje.  
Linia 178: Linia 176:
</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
w środowisku <math>E'</math> z miejsca deklaracji tej procedury
zmodyfikowanym o przypisanie <math> x \mapsto l </math>
zmodyfikowanym o przypisanie <math>x \mapsto l</math>
lokacji <math> l </math> do parametru formalnego <math> x </math> procedury.
lokacji <math>l</math> do parametru formalnego <math>x</math> procedury.
Stan, w którym uruchomione jest <math> I </math> to po prostu
Stan, w którym uruchomione jest <math>I</math> to po prostu
stan bieżący z miejsca wołania procedury; o prawidłowe
stan bieżący z miejsca wołania procedury; o prawidłowe
wiązanie identyfikatorów ,,troszczy" się wyłącznie
wiązanie identyfikatorów ,,troszczy" się wyłącznie
środowisko <math> E' </math>.  
środowisko <math>E'</math>.  


'''Pytanie:''' czy powyższa reguła dopuszcza rekurencyjne
'''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
E'[x \mapsto l] nie ma informacji o procedurze <math> x_1 </math>, którą
<math>E'[x \mapsto l]</math> nie ma informacji o procedurze <math>x_1</math>, którą
właśnie wołamy. Może się zdarzyć, że <math> E'[x \mapsto l] \in PROC </math>, ale
właśnie wołamy. Może się zdarzyć, że <math>E'[x \mapsto l] \in PROC</math>, ale
oznacza to tylko, że w miejscu deklaracji procedury <math> x_1 </math>
oznacza to tylko, że w miejscu deklaracji procedury <math>x_1</math>
była już wcześniej (statycznie) zadeklarowana inna procedura
była już wcześniej (statycznie) zadeklarowana inna procedura
o tej samej nazwie.  
o tej samej nazwie.  
Aby umożliwić rekurencję, powinniśmy zadbać sami o to, aby
Aby umożliwić rekurencję, powinniśmy zadbać sami o to, aby
środowisko, w którym wykonujemy <math> I </math> zawierało informację
środowisko, w którym wykonujemy <math>I</math> zawierało informację
o naszej procedurze:
o naszej procedurze:


Linia 208: Linia 205:
</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
dodane  do <math>E'</math> wystarcza na tylko jedno wywołanie rekurencyjne
(licząc w głąb). Ale każde kolejne wywołanie dodaje tę informację,
(licząc w głąb). Ale każde kolejne wywołanie dodaje tę informację,
czyli każde wywołanie procedury przygotowuje środowisko dla
czyli każde wywołanie procedury przygotowuje środowisko dla
Linia 217: Linia 214:
'''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>,
<math>x \mapsto l</math> oraz <math>x_1 \mapsto \langle x, I, E' \rangle</math>,
ale dlaczego w takiej kolejności.
ale dlaczego w takiej kolejności.


Linia 236: Linia 233:
Okazuje się, że tak nie jest, oto dwa kontrprzykłady:
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);
\ \\
\,\mathbf{end}
\quad x(y);\\
 
\,\mathbf{end}
 
</math>
 
\mathbf{begin}\,
  <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);
\,\mathbf{end}
 


Każdy z tych programów uruchomi się poprawnie w dokładnie
Każdy z tych programów uruchomi się poprawnie w dokładnie
Linia 260: Linia 257:
'''Pytanie:''' Który w którym?
'''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.
Rozważmy na koniec problem dealokacji.




===== Wariant (dealokacja) =====
<br>
'''Wariant (dealokacja)'''
<br>


Chcemy, aby ,,posprzątano" po zakończeniu wykonania bloku,
Chcemy, aby ,,posprzątano" po zakończeniu wykonania bloku,
Linia 271: Linia 270:
i w związku z tym nie będą już potrzebne.
i w związku z tym nie będą już potrzebne.
Oznacza to, że powinniśmy przywrócić nieokreśloność stanu dla
Oznacza to, że powinniśmy przywrócić nieokreśloność stanu dla
wszystkich tych lokacji, które były użyte podczas deklaracji <math> d </math>.
wszystkich tych lokacji, które były użyte podczas deklaracji <math>d</math>.


Jest wiele możliwości wyrażenia tego dodatkowego warunku,
Jest wiele możliwości wyrażenia tego dodatkowego warunku,
Linia 283: Linia 282:
</math>
</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
Zakładamy tutaj, że znamy
zbiór nowo zaalokowanych lokacji <math> L \subseteq \mathbf{Loc} </math>.
zbiór nowo zaalokowanych lokacji <math>L \subseteq \mathbf{Loc}</math>.


<math>
<math>
Linia 299: Linia 298:


Teraz albo napiszemy w dodatkowym warunku, że  
Teraz albo napiszemy w dodatkowym warunku, że  
<math> L = \dom(s'') \setminus \dom(s) </math>:
<math>L = \mathrm{dom}(s'') \setminus \mathrm{dom}(s)</math>:


<math>
<math>
Linia 307: Linia 306:
       s'', L \,\longrightarrow\, \bar{s}}
       s'', L \,\longrightarrow\, \bar{s}}
     {E \,\vdash\, \mathbf{begin}\, d;\, I \,\mathbf{end}, s \,\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>
</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>,
Niech deklaracja zwraca, oprócz pary <math>(E', s')</math>,
dodatkowo zbiór <math> L </math>.
dodatkowo zbiór <math>L</math>.
Oto poprawione reguły dla deklaracji:
Oto poprawione reguły dla deklaracji:


Linia 320: Linia 319:
\frac{E \,\vdash\, e, s \,\longrightarrow\, n}
\frac{E \,\vdash\, e, s \,\longrightarrow\, n}
     {E \,\vdash\, \mathbf{var}\, x=e, s \,\longrightarrow\, (E', s', \{ l \})  
     {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],\,   
                           s' = s[l \mapsto n],\,   
                           l = \mathtt{new}(s)}
                           l = \mathtt{newloc}(s)}
</math>
</math>


<math>
<math>
E \,\vdash\, \mathbf{proc}\, x_1(x_2);\, I, s \,\longrightarrow\, (E', s, \emptyset)
E \,\vdash\, \mathbf{Proc}\, x_1(x_2);\, I, s \,\longrightarrow\, (E', s, \emptyset)
\quad \mbox{ gdzie }
\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].
Linia 348: Linia 347:
</math>
</math>


</div></div>
}}


==== Zadanie 2 (wiązanie dynamiczne) ====
{{cwiczenie|2 (wiązanie dynamiczne)|cw2|


Zastanówmy się, jakich modyfikacji wymaga nasza semantyka,
Zastanówmy się, jakich modyfikacji wymaga nasza semantyka,
Linia 360: Linia 361:
wewnątrz procedury, czyli wiązanie dynamiczne dotyczy i zmiennych
wewnątrz procedury, czyli wiązanie dynamiczne dotyczy i zmiennych
i procedur.
i procedur.
Oto przykład:
}}
 
 
{{przyklad|||
 
<math>\mathbf{begin}\,</math>
  <math>\mathbf{var}\,</math> x = 1;
  <math>\mathbf{Proc}\,</math> p(y); y := y+x;


<math>
  <math>\mathbf{begin}\,</math>
\mathbf{begin}\,\\
    <math>\mathbf{var}\,</math> x = 10;
\quad \mathbf{var}\, x = 1;\\
    <math>\mathbf{var}\,</math> z = 0;
\quad \mathbf{proc}\, p(y);\, y := y+x;\\
 
\ \\
    <math>\mathbf{call}\,</math> p(z);
\quad \mathbf{begin}\,\\
  <math>\,\mathbf{end}</math>
\quad \quad \mathbf{var}\, x = 10;\\
<math>\,\mathbf{end}</math>
\quad \quad \mathbf{var}\, z = 0;\\
 
\ \\
 
\quad \quad \mathbf{call}\, p(z);
Wartość końcowa zmiennej <math>z = 10</math>.
\quad \,\mathbf{end}\\
Gdyby wiązanie zmiennej <math>x</math> było statyczne, to wartość ta
\,\mathbf{end}
wynosiłaby <math>1</math>. Podobnie dla procedur:
</math>
 
 
<math>\mathbf{begin}\,</math>
  <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{begin}\,</math>
    <math>\mathbf{Proc}\,</math> <math>\mathbf{call}\,</math>q(x); x := x+x;
    <math>\mathbf{var}\,</math> z = 2;


Wartość końcowa zmiennej <math> z = 10 </math>.
    <math>\mathbf{call}\,</math> p(z);
Gdyby wiązanie zmiennej <math> x </math> było statyczne, to wartość ta
  <math>\,\mathbf{end}</math>
wynosiłaby <math> 1 </math>. Podobnie dla procedur:
<math>\,\mathbf{end}</math>


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


<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>.
<math>\mathbf{begin}\,</math>
Procedura <math> p </math> wywołuje procedurę <math> r </math>,
  <math>\mathbf{Proc}\,</math> q(x); \mathbf{call}\, r(x);
  <math>\mathbf{Proc}\,</math> p(y);
    <math>\mathbf{begin}\,</math>
      <math>\mathbf{Proc}\,</math> r(x); x := x+x;
 
      <math>\mathbf{call}\,</math> q(x);
    <math>\,\mathbf{end}</math>
  <math>\mathbf{var}\,</math> z = 7;
\ \\
  <math>\mathbf{call}\,</math> p(z);
\,\mathbf{end}
 
 
Wartość końcowa zmiennej <math>z</math> wynosi <math>14</math>.
Procedura <math>p</math> wywołuje procedurę <math>r</math>,
,,przekazując" jej również środowisko z miejsca wołania,
,,przekazując" jej również środowisko z miejsca wołania,
zawierające informację o procedurze <math> r </math>, która
zawierające informację o procedurze <math>r</math>, która
przy widoczności statycznej byłaby lokalna, a teraz nie jest.
przy widoczności statycznej byłaby lokalna, a teraz nie jest.
}}




==== Rozwiązanie ====
{{rozwiazanie||roz2|
 
<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:
Linia 435: Linia 441:
</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
Wystarczy więc, jeśli zignorujemy to środowisko, a zamiast
niego użyjemy bieżącego środowiska <math> E </math> (czyli środowiska
niego użyjemy bieżącego środowiska <math>E</math> (czyli środowiska
z miejsca wywołania):
z miejsca wywołania):


Linia 450: Linia 456:


Oczywiście w takim przypadku w środowiskach
Oczywiście w takim przypadku w środowiskach
wystarczy przechowywać dla procedur pary <math> \langle x, I \rangle </math>.
wystarczy przechowywać dla procedur pary <math>\langle x, I \rangle</math>.


Zastanówmy się teraz, jak uwzględnić rekurencję? Oczywiście  
Zastanówmy się teraz, jak uwzględnić rekurencję? Oczywiście  
Linia 465: Linia 471:
ale jeśli uważnie przyjrzymy się tej regule, to okazuje się,
ale jeśli uważnie przyjrzymy się tej regule, to okazuje się,
że ,,przelewamy z pustego w próżne". Sciślej,  
że ,,przelewamy z pustego w próżne". Sciślej,  
dodajemy do <math> E </math> parę <math> x_1 \mapsto \langle x, I \rangle </math>,
dodajemy do <math>E</math> parę <math>x_1 \mapsto \langle x, I \rangle</math>,
która już tam tak naprawdę jest!
która już tam tak naprawdę jest!
Okazuje się, że dzięki dynamicznemu wiązaniu identyfikatorów ,,za
Okazuje się, że dzięki dynamicznemu wiązaniu identyfikatorów ,,za
darmo" otrzymujemy rekurencje! Tak jest na przykład w programie:
darmo" otrzymujemy rekurencje! Tak jest na przykład w programie:


<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>,
<math>\mathbf{begin}\,</math>
w środowisku jest już informacja nt. procedury <math> p </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>
 
 
ponieważ w momencie wywołania rekurencyjnego <math>\mathbf{call}\, p(x)</math>,
w środowisku jest już informacja nt. procedury <math>p</math>!
 
</div></div>
}}




==== 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ść
* przez wartość
Linia 504: Linia 512:
(a więc podobnie do przekazywania przez zmienną).
(a więc podobnie do przekazywania przez zmienną).
Parametr formalny jest traktowany jak zmienna lokalna procedury.
Parametr formalny jest traktowany jak zmienna lokalna procedury.
}}




==== Rozwiązanie ====
{{rozwiazanie||roz3|




===== Przekazywanie przez wartość =====
'''Przekazywanie przez wartość'''
 
<div class="mw-collapsible mw-made=collapsible mw-collapsed"><div class="mw-collapsible-content" style="display:none">


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


<math>
<math>
Linia 520: Linia 531:
</math>
</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
którą przypiszemy parametrowi formalnemu; następnie obliczamy
wartość parametru aktualnego i umieszczamy ją w tej lokacji:
wartość parametru aktualnego i umieszczamy ją w tej lokacji:
Linia 526: Linia 537:
<math>
<math>
\frac{E \,\vdash\, e, s \,\longrightarrow\, n
\frac{E \,\vdash\, e, s \,\longrightarrow\, n
       \quad \quad
       \quad
       E'[x' \mapsto l] \,\vdash\, I, s[l \mapsto n] \,\longrightarrow\, s'}
       E'[x' \mapsto l] \,\vdash\, I, s[l \mapsto n] \,\longrightarrow\, s'}
     {E \,\vdash\, \mathbf{call}\, x(e), s \,\longrightarrow\, s'}
     {E \,\vdash\, \mathbf{call}\, x(e), s \,\longrightarrow\, s'}
\quad \mbox{ o ile }
\quad \mbox{ o ile }
E(x) = \langle x', I, E' \rangle \in PROC \mbox{ i }
E(x) = \langle x', I, E' \rangle \in PROC \mbox{ i }
l = \mathtt{new}(s)
l = \mathtt{newloc}(s)
</math>  
</math>  


</div></div>
'''Przekazywanie in-out'''


===== Przekazywanie in-out =====
<div class="mw-collapsible mw-made=collapsible mw-collapsed"><div class="mw-collapsible-content" style="display:none">


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


<math>
<math>
\frac{E'[x \mapsto l] \,\vdash\, I, s[l \mapsto s(l_2)] \,\longrightarrow\, s'}
\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 }
\quad \mbox{ o ile }
E(x_2) = l_2 \in \mathbf{Loc} \mbox{ i }
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 PROC \mbox{ i }
E(x_1) = \langle x, I, E' \rangle \in PROC \mbox{ i }
l = \mathtt{new}(s)
l = \mathtt{newloc}(s)
</math>  
</math>  
</div></div>
}}




Linia 562: Linia 580:




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, procedury zadeklarowane w jednej deklaracji równoległej
To znaczy, że procedury zadeklarowane w jednej deklaracji równoległej
mogą się wzajemniej wywoływać bez żadnych ograniczeń.
mogą się wzajemniej wywoływać bez żadnych ograniczeń.


Linia 570: Linia 588:
==== Zadanie 2 ====
==== Zadanie 2 ====


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:
Wywołanie funkcji może teraz pojawić się wewnątrz wyrażenia:
Linia 585: Linia 603:
==== Zadanie 3 ====
==== Zadanie 3 ====


Rozważ warianty semantyki języka Small, w którym
Rozważ następujące warianty:


* wiązanie zmiennych jest statyczne a procedur dynamiczne
* wiązanie zmiennych jest statyczne a procedur dynamiczne
* wiązanie zmiennych jest dymamiczne a procedur statyczne
* wiązanie zmiennych jest dymamiczne a procedur statyczne
==== Zadanie 4 ====
Rozszerz semantykę procedur tak, aby parametrem aktualnym procedury
mogła byc procedura.

Wersja z 08:50, 8 sie 2006


Zawartość

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


Zadania z rozwiązaniami

Ćwiczenie 1 (procedury)

Rozszerzmy języka Tiny o deklaracje i wywołania procedur:

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

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

Konstrukcja 𝐏𝐫𝐨𝐜x1(x2) deklaraje 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, odwuł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

{{{3}}}


Rozwiązanie

{{{3}}}


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

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

  • przez wartość
  • in-out

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


Rozwiązanie

{{{3}}}


Zadania domowe

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


Zadanie 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)

Uwaga na efekty uboczne!


Zadanie 3

Rozważ następujące warianty:

  • wiązanie zmiennych jest statyczne a procedur dynamiczne
  • wiązanie zmiennych jest dymamiczne a procedur statyczne


Zadanie 4

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

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