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

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

Ćwiczenie 4

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