Semantyka i weryfikacja programów/Ćwiczenia 6

Zawarto¶æ

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

Semantyka naturalna procedur

Ćwiczenie 1 (procedury)

Rozszerzmy jêzyk Tiny o deklaracje i wywo³ania procedur:

$I::=\dots |\mathbf{𝐛}\mathbf{𝐞}\mathbf{𝐠}\mathbf{𝐢}\mathbf{𝐧}d;I\mathbf{𝐞}\mathbf{𝐧}\mathbf{𝐝}|\mathbf{𝐜}\mathbf{𝐚}\mathbf{𝐥}\mathbf{𝐥}{x}_1(x_2)$

$d::=\mathbf{𝐯}\mathbf{𝐚}\mathbf{𝐫}x=e|\mathbf{𝐩}\mathbf{𝐫}\mathbf{𝐨}\mathbf{𝐜}{x}_1(x_2);I|d_1;d_2$

Konstrukcja $\mathbf{𝐩}\mathbf{𝐫}\mathbf{𝐨}\mathbf{𝐜}{x}_1(x_2)$ deklaruje procedurê o nazwie $x_1$, której parametrem formalnym jest $x_2$. Zak³adamy statyczne wi±zanie identyfikatorów i przekazywanie parametrów przez zmienn± (to znaczy, ¿e w momencie wywo³ania procedury, powinna zostaæ przekazana lokacja odpowiadaj±ca parametrowi aktualnemu). Instrukcja $\mathbf{𝐜}\mathbf{𝐚}\mathbf{𝐥}\mathbf{𝐥}{x}_1(x_2)$ wywo³uje procedurê $x_1$ z parametrem aktualnym $x_2$.

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.

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

  $\mathbf{𝐛}\mathbf{𝐞}\mathbf{𝐠}\mathbf{𝐢}\mathbf{𝐧}$
    $\mathbf{𝐯}\mathbf{𝐚}\mathbf{𝐫}$ x = 10; $\mathbf{𝐯}\mathbf{𝐚}\mathbf{𝐫}$ z = 0;

    $\mathbf{𝐜}\mathbf{𝐚}\mathbf{𝐥}\mathbf{𝐥}$ p(z);
  $\mathbf{𝐞}\mathbf{𝐧}\mathbf{𝐝}$
$\mathbf{𝐞}\mathbf{𝐧}\mathbf{𝐝}$

Warto¶æ koñcowa zmiennej $z=10$. Gdyby wi±zanie zmiennej $x$ by³o statyczne, to warto¶æ ta wynosi³aby $1$. Podobnie dla procedur:

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

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

    $\mathbf{𝐜}\mathbf{𝐚}\mathbf{𝐥}\mathbf{𝐥}$ p(z);
  $\mathbf{𝐞}\mathbf{𝐧}\mathbf{𝐝}$
$\mathbf{𝐞}\mathbf{𝐧}\mathbf{𝐝}$

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:

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

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

  $\mathbf{𝐜}\mathbf{𝐚}\mathbf{𝐥}\mathbf{𝐥}$ p(z);
$\mathbf{𝐞}\mathbf{𝐧}\mathbf{𝐝}$

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::=\dots |\mathbf{𝐜}\mathbf{𝐚}\mathbf{𝐥}\mathbf{𝐥}{x}_1(x_2).$

Wewnatrz funkcji jej nazwa mozna poslugiwac sie jak zmienna lokalna. Wynik zwracany przez funkcje to wartosc tej zmiennej w momencie wyjscia 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.