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
Sl (dyskusja | edycje)
101 edycji
Nie podano opisu zmian
Linia 29: 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
Linia 53: Linia 53:
\mathbf{Store} = \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 \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 nt procedury, którą musimy przechowywać, to:
Informacja nt procedury, którą musimy przechowywać, to:
Linia 69: 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>\mathbf{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>\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.


Linia 109: 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 172: Linia 172:
     {E \,\vdash\, \mathbf{call}\, x_1(x_2), s \,\longrightarrow\, s'}
     {E \,\vdash\, \mathbf{call}\, x_1(x_2), s \,\longrightarrow\, s'}
\quad \mbox{ o ile }
\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>
Linia 189: Linia 189:
Okazuje się, że niestety nie, gdyż w środowisku
Okazuje się, że niestety nie, gdyż w środowisku
<math>E'[x \mapsto l]</math> nie ma informacji o procedurze <math>x_1</math>, którą
<math>E'[x \mapsto l]</math> nie ma informacji o procedurze <math>x_1</math>, którą
właśnie wołamy. Może się zdarzyć, że <math>E'[x \mapsto l] \in PROC</math>, ale
właśnie wołamy. Może się zdarzyć, że <math>E'[x \mapsto l] \in \mathbf{Proc}</math>, ale
oznacza to tylko, że w miejscu deklaracji procedury <math>x_1</math>
oznacza to tylko, że w miejscu deklaracji procedury <math>x_1</math>
była już wcześniej (statycznie) zadeklarowana inna procedura
była już wcześniej (statycznie) zadeklarowana inna procedura
Linia 201: Linia 201:
     {E \,\vdash\, \mathbf{call}\, x_1(x_2), s \,\longrightarrow\, s'}
     {E \,\vdash\, \mathbf{call}\, x_1(x_2), s \,\longrightarrow\, s'}
\quad \mbox{ o ile }
\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>
Linia 225: Linia 225:
     {E \,\vdash\, \mathbf{call}\, x_1(x_2), s \,\longrightarrow\, s'}
     {E \,\vdash\, \mathbf{call}\, x_1(x_2), s \,\longrightarrow\, s'}
\quad \mbox{ o ile }
\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>
Linia 236: Linia 236:
  <math>\mathbf{begin}\,</math>
  <math>\mathbf{begin}\,</math>
   <math>\mathbf{var}\,</math> y = 7;
   <math>\mathbf{var}\,</math> y = 7;
   <math>\mathbf{Proc}\,</math> x(x); x := x+1;
   <math>\mathbf{proc}\,</math> x(x); x := x+1;
   
   
   <math>\mathbf{call}\,</math> x(y);
   <math>\mathbf{call}\,</math> x(y);
Linia 245: Linia 245:
  \mathbf{begin}\,
  \mathbf{begin}\,
   <math>\mathbf{var}\,</math> y = 7;
   <math>\mathbf{var}\,</math> y = 7;
   <math>\mathbf{Proc}\,</math> x(x);
   <math>\mathbf{proc}\,</math> x(x);
     <math>\mathbf{if}\,</math> y > 0 <math>\,\mathbf{then}\,</math> y := y-1; <math>\mathbf{call}\,</math> x(y) <math>\,\mathbf{else}\, \mathbf{skip}</math>;
     <math>\mathbf{if}\,</math> y > 0 <math>\,\mathbf{then}\,</math> y := y-1; <math>\mathbf{call}\,</math> x(y) <math>\,\mathbf{else}\, \mathbf{skip}</math>;


Linia 325: Linia 325:


<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 365: Linia 365:


{{przyklad|||
{{przyklad|||
Spójrzmy na kilka prostych programów.
}}


  <math>\mathbf{begin}\,</math>
  <math>\mathbf{begin}\,</math>
   <math>\mathbf{var}\,</math> x = 1;
   <math>\mathbf{var}\,</math> x = 1;
   <math>\mathbf{Proc}\,</math> p(y); y := y+x;
   <math>\mathbf{proc}\,</math> p(y); y := y+x;


   <math>\mathbf{begin}\,</math>
   <math>\mathbf{begin}\,</math>
Linia 385: Linia 387:


  <math>\mathbf{begin}\,</math>
  <math>\mathbf{begin}\,</math>
   <math>\mathbf{Proc}\,</math> q(x); x := x+1;
   <math>\mathbf{proc}\,</math> q(x); x := x+1;
   <math>\mathbf{Proc}\,</math> p(y); <math>\mathbf{call}\,</math> q(y); <math>\mathbf{call}\,</math> q(y);
   <math>\mathbf{proc}\,</math> p(y); <math>\mathbf{call}\,</math> q(y); <math>\mathbf{call}\,</math> q(y);
  \ \\
  \ \\
   <math>\mathbf{begin}\,</math>
   <math>\mathbf{begin}\,</math>
     <math>\mathbf{Proc}\,</math> <math>\mathbf{call}\,</math>q(x); x := x+x;
     <math>\mathbf{proc}\,</math> <math>\mathbf{call}\,</math>q(x); x := x+x;
     <math>\mathbf{var}\,</math> z = 2;
     <math>\mathbf{var}\,</math> z = 2;


Linia 406: Linia 408:


  <math>\mathbf{begin}\,</math>
  <math>\mathbf{begin}\,</math>
   <math>\mathbf{Proc}\,</math> q(x); \mathbf{call}\, r(x);
   <math>\mathbf{proc}\,</math> q(x); \mathbf{call}\, r(x);
   <math>\mathbf{Proc}\,</math> p(y);
   <math>\mathbf{proc}\,</math> p(y);
     <math>\mathbf{begin}\,</math>
     <math>\mathbf{begin}\,</math>
       <math>\mathbf{Proc}\,</math> r(x); x := x+x;
       <math>\mathbf{proc}\,</math> r(x); x := x+x;


       <math>\mathbf{call}\,</math> q(x);
       <math>\mathbf{call}\,</math> q(x);
Linia 424: Linia 426:
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.
}}




Linia 437: Linia 438:
     {E \,\vdash\, \mathbf{call}\, x_1(x_2), s \,\longrightarrow\, s'}
     {E \,\vdash\, \mathbf{call}\, x_1(x_2), s \,\longrightarrow\, s'}
\quad \mbox{ o ile }
\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>
Linia 451: Linia 452:
     {E \,\vdash\, \mathbf{call}\, x_1(x_2), s \,\longrightarrow\, s'}
     {E \,\vdash\, \mathbf{call}\, x_1(x_2), s \,\longrightarrow\, s'}
\quad \mbox{ o ile }
\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>
Linia 465: Linia 466:
     {E \,\vdash\, \mathbf{call}\, x_1(x_2), s \,\longrightarrow\, s'}
     {E \,\vdash\, \mathbf{call}\, x_1(x_2), s \,\longrightarrow\, s'}
\quad \mbox{ o ile }
\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}
E(x_2) = l \in \mathbf{Loc}
</math>
</math>
Linia 478: Linia 479:


  <math>\mathbf{begin}\,</math>
  <math>\mathbf{begin}\,</math>
   <math>\mathbf{Proc}\,</math> p(x); <math>\mathbf{if}\,</math> x < 100 <math>\,\mathbf{then}\,</math> x := x+x; <math>\mathbf{call}\,</math> p(x) <math>\,\mathbf{else}\, \mathbf{skip}</math>;
   <math>\mathbf{proc}\,</math> p(x); <math>\mathbf{if}\,</math> x < 100 <math>\,\mathbf{then}\,</math> x := x+x; <math>\mathbf{call}\,</math> p(x) <math>\,\mathbf{else}\, \mathbf{skip}</math>;
   <math>\mathbf{var}\,</math> z = 8;
   <math>\mathbf{var}\,</math> z = 8;
   
   
Linia 541: Linia 542:
     {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 \mathbf{Proc} \mbox{ i }
l = \mathtt{newloc}(s)
l = \mathtt{newloc}(s)
</math>  
</math>  
Linia 566: Linia 567:
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 \mathbf{Proc} \mbox{ i }
l = \mathtt{newloc}(s)
l = \mathtt{newloc}(s)
</math>  
</math>  

Wersja z 08:54, 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

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); \mathbf{call}\, r(x);
  𝐩𝐫𝐨𝐜 p(y);
    𝐛𝐞𝐠𝐢𝐧
      𝐩𝐫𝐨𝐜 r(x); x := x+x;

      𝐜𝐚𝐥𝐥 q(x);
    𝐞𝐧𝐝
  𝐯𝐚𝐫 z = 7;
\ \\
  𝐜𝐚𝐥𝐥 p(z);
\,\mathbf{end}


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


Rozwiązanie

{{{3}}}


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

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

  • przez wartość
  • in-out

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


Rozwiązanie

{{{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=10803”