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.

Zadania z rozwiązaniami

Ćwiczenie 1 (procedury)

Rozszerzmy języka 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)$ deklaraje 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, 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::=\dots |\mathbf{𝐜}\mathbf{𝐚}\mathbf{𝐥}\mathbf{𝐥}{x}_1(x_2)$

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.