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


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
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.
Pracujemy ze środowiskami i stanami.


Linia 33: Linia 30:
</math>   
</math>   


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


Linia 56: Linia 48:
</math>
</math>


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


Linia 64: Linia 55:
* ''środowisko'', w którym procedura została zadeklarowana.
* ''środowisko'', w którym procedura została zadeklarowana.


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


Zatem niech <math>\mathbf{Proc} = \mathbf{Var} \times \mathbf{Stmt} \times \mathbf{Env}</math>.
Zatem niech <math>\mathbf{Proc} = \mathbf{Var} \times \mathbf{Stmt} \times \mathbf{Env}</math>.
Linia 91: Linia 77:
</math>
</math>


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


Zajmijmy się najpierw deklaracjami zmiennych:
Zajmijmy się najpierw deklaracjami zmiennych:
Linia 101: Linia 85:
\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{newloc}(s)
                     l = \mathtt{newloc}(s)
Linia 114: Linia 98:
</math>
</math>


Zauważmy, że deklaracja procedury nie zmienia stanu, tylko środowisko,
Zauważmy, że deklaracja procedury nie zmienia stanu, tylko środowisko, w odróżnieniu od deklaracji zmiennej.
w odróżnieniu od deklaracji zmiennej.
W środowisku pamiętamy trójkę <math>\langle x_2, I, E \rangle</math> zawierającą nazwę parametru formalnego, ciało procedury oraz ''środowisko deklaracji procedury''.
W środowisku pamiętamy trójkę <math>\langle x_2, I, E \rangle</math> zawierającą
To ostatnie determinuje statyczne wiązanie identyfikatorów: wiązanie identyfikatorów występującuch 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:
Aby dokończyć semantykę deklaracji potrzebujemy jeszcze jednej reguły:


Linia 144: Linia 123:
</math>
</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:
Widać to jasno w regule dla złożenia sekwencyjnego:


Linia 173: Linia 145:
\quad \mbox{ o ile }
\quad \mbox{ o ile }
E(x_1) = \langle x, I, E' \rangle \in \mathbf{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 wywołania procedury?
'''Pytanie:''' czy powyższa reguła dopuszcza rekurencyjne wywołania procedury?


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


<math>
<math>
Linia 202: Linia 162:
\quad \mbox{ o ile }
\quad \mbox{ o ile }
E(x_1) = \langle x, I, E' \rangle \in \mathbf{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.
I to jest wystarczające.


'''Pytanie:''' czy możliwa jest rekurencja wzajemna?
'''Pytanie:''' czy możliwa jest rekurencja wzajemna?


Pozostaje jeszcze jedna kwestia: dodajemy do środowiska <math>E'</math>
Pozostaje jeszcze jedna kwestia: dodajemy do środowiska <math>E'</math> dwa przypisania:  
dwa przypisania:  
<math>x \mapsto l</math> oraz <math>x_1 \mapsto \langle x, I, E' \rangle</math>, ale dlaczego w takiej kolejności?
<math>x \mapsto l</math> oraz <math>x_1 \mapsto \langle x, I, E' \rangle</math>,
ale dlaczego w takiej kolejności.


'''Pytanie:''' co się stanie, gdy zamienimy tę kolejność:
'''Pytanie:''' co się stanie, gdy zamienimy tę kolejność:
Linia 226: Linia 181:
\quad \mbox{ o ile }
\quad \mbox{ o ile }
E(x_1) = \langle x, I, E' \rangle \in \mathbf{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 239: Linia 194:
   
   
   <math>\mathbf{call}\,</math> x(y);
   <math>\mathbf{call}\,</math> x(y);
  \,\mathbf{end}
  <math>\,\mathbf{end}</math>






  \mathbf{begin}\,
  <math>\mathbf{begin}\,</math>
   <math>\mathbf{var}\,</math> y = 7;
   <math>\mathbf{var}\,</math> y = 7;
   <math>\mathbf{proc}\,</math> x(x);
   <math>\mathbf{proc}\,</math> x(x);
Linia 249: Linia 204:


   <math>\mathbf{call}\,</math> x(y);
   <math>\mathbf{call}\,</math> x(y);
  \,\mathbf{end}
  <math>\,\mathbf{end}</math>




Każdy z tych programów uruchomi się poprawnie w dokładnie
Każdy z tych programów uruchomi się poprawnie w dokładnie jednym z wariantów semantyki.  
jednym z wariantów semantyki.  


'''Pytanie:''' Który w którym?
'''Pytanie:''' Który w którym?
Linia 260: Linia 214:


Rozważmy na koniec problem dealokacji.
Rozważmy na koniec problem dealokacji.


<br>
<br>
Linia 266: Linia 219:
<br>
<br>


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


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


<math>
<math>
Linia 282: Linia 231:
</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 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>
<math>
Linia 297: Linia 244:
</math>
</math>


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


<math>
<math>
Linia 309: Linia 255:
</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>, 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 343: Linia 287:
       \quad \quad
       \quad \quad
       E' \,\vdash\, I, s' \,\longrightarrow\, s''
       E' \,\vdash\, I, s' \,\longrightarrow\, s''
      \quad \quad
       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}}
Linia 352: Linia 297:
{{cwiczenie|2 (wiązanie dynamiczne)|cw2|
{{cwiczenie|2 (wiązanie dynamiczne)|cw2|


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


Linia 381: Linia 320:


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




Linia 399: Linia 337:


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




Linia 421: Linia 356:


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




Linia 438: Linia 371:
\quad \mbox{ o ile }
\quad \mbox{ o ile }
E(x_1) = \langle x, I, E' \rangle \in \mathbf{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>
<math>
Linia 452: Linia 382:
\quad \mbox{ o ile }
\quad \mbox{ o ile }
E(x_1) = \langle x, I, E' \rangle \in \mathbf{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>
<math>
Linia 469: Linia 398:
</math>
</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:




Linia 485: Linia 411:




ponieważ w momencie wywołania rekurencyjnego <math>\mathbf{call}\, p(x)</math>,
ponieważ w momencie wywołania rekurencyjnego <math>\mathbf{call}\, p(x)</math>, w środowisku jest już informacja nt. procedury <math>p</math>!
w środowisku jest już informacja nt. procedury <math>p</math>!


</div></div>
</div></div>
Linia 504: 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
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 spowrotem 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.
Parametr formalny jest traktowany jak zmienna lokalna procedury.
}}
}}
Linia 519: Linia 439:
<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">


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


<math>
<math>
Linia 528: Linia 447:
</math>
</math>


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


<math>
<math>
Linia 549: Linia 466:
<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
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:
Oto reguła:


Linia 563: Linia 476:
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 \mathbf{Proc} \mbox{ i }
</math>
l = \mathtt{newloc}(s)
<math>
E(x_1) = \langle x, I, E' \rangle \in \mathbf{Proc} \mbox{ i } l = \mathtt{newloc}(s).
</math>  
</math>  


Linia 576: Linia 490:
{{cwiczenie|1|cw1.dom|
{{cwiczenie|1|cw1.dom|


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


Linia 585: Linia 497:
{{cwiczenie|2|cw2.dom|
{{cwiczenie|2|cw2.dom|


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


Linia 595: Linia 506:
</math>
</math>


Wewnatrz funkcji jej nazwa mozna poslugiwac sie jak
Wewnątrz funkcji jej nazwą można posługiwać się jak zmienną lokalną.
zmienna lokalna.
Wynik zwracany przez funkcję to wartość tej zmiennej w momencie wyjścia z funkcji.
Wynik zwracany przez funkcje to wartosc
tej zmiennej w momencie wyjscia z funkcji.


Uwaga na efekty uboczne!
Uwaga na efekty uboczne!
Linia 615: Linia 524:
{{cwiczenie|4|cw4.dom|
{{cwiczenie|4|cw4.dom|


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

Wersja z 08:35, 11 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.


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 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 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=14910”