Semantyka i weryfikacja programów/Ćwiczenia 10

Funkcje

Zadanie 1

Zdefiniuj semantykę denotacyjną następującego języka:

$n::=0|1|\dots$

$x::=\dots (identyfikatory)\dots$

$e::=n|x|e_1+e_2|\mathbf{𝐜}\mathbf{𝐚}\mathbf{𝐥}\mathbf{𝐥}F(x)$

$b::=e_1=e_2|\mathbf{𝐧}\mathbf{𝐨}\mathbf{𝐭}b|b_1\mathbf{𝐨}\mathbf{𝐫}{b}_2$

$i::=x:=e|i_1;i_2|\mathbf{𝐢}\mathbf{𝐟}b\mathbf{𝐭}\mathbf{𝐡}\mathbf{𝐞}\mathbf{𝐧}{i}_1\mathbf{𝐞}\mathbf{𝐥}\mathbf{𝐬}\mathbf{𝐞}{i}_2|\mathbf{𝐬}\mathbf{𝐤}\mathbf{𝐢}\mathbf{𝐩}|\mathbf{𝐰}\mathbf{𝐡}\mathbf{𝐢}\mathbf{𝐥}\mathbf{𝐞}b\mathbf{𝐝}\mathbf{𝐨}i|\mathbf{𝐛}\mathbf{𝐞}\mathbf{𝐠}\mathbf{𝐢}\mathbf{𝐧}d;i\mathbf{𝐞}\mathbf{𝐧}\mathbf{𝐝}$

$d::=\mathbf{𝐯}\mathbf{𝐚}\mathbf{𝐫}x:=e|d_1;d_2|\mathbf{𝐟}\mathbf{𝐮}\mathbf{𝐧}F(x);i\mathbf{𝐞}\mathbf{𝐧}\mathbf{𝐝}\mathbf{𝐟}\mathbf{𝐮}\mathbf{𝐧}$

Deklaracja $\mathbf{𝐟}\mathbf{𝐮}\mathbf{𝐧}F(x);i\mathbf{𝐞}\mathbf{𝐧}\mathbf{𝐝}\mathbf{𝐟}\mathbf{𝐮}\mathbf{𝐧}$ wprowadza funkcję o nazwie $F$ z jednym parametrem $x$ przekazywanym przez zmienną. Wykonanie funkcji polega na wykonaniu instrukcji $i$, która powinna zawierać przypisanie na identyfikator $F$. Takie przypisanie ustala wartość funkcji ale nie kończy wykonania instrukcji i.

Kontynuacje instrukcji

Zadanie 2

Powróćmy do języka TINY. Dodajmy do niego następujące instrukcje:

$i::=x:=e|i_1;i_2|\mathbf{𝐢}\mathbf{𝐟}b\mathbf{𝐭}\mathbf{𝐡}\mathbf{𝐞}\mathbf{𝐧}{i}_1\mathbf{𝐞}\mathbf{𝐥}\mathbf{𝐬}\mathbf{𝐞}{i}_2|\mathbf{𝐬}\mathbf{𝐤}\mathbf{𝐢}\mathbf{𝐩}|\mathbf{𝐚}\mathbf{𝐛}\mathbf{𝐨}\mathbf{𝐫}\mathbf{𝐭}|\mathbf{𝐰}\mathbf{𝐡}\mathbf{𝐢}\mathbf{𝐥}\mathbf{𝐞}b\mathbf{𝐝}\mathbf{𝐨}i|\mathbf{𝐫}\mathbf{𝐞}\mathbf{𝐩}\mathbf{𝐞}\mathbf{𝐚}\mathbf{𝐭}i\mathbf{𝐮}\mathbf{𝐧}\mathbf{𝐭}\mathbf{𝐢}\mathbf{𝐥}b$

Zdefiniuj semantykę kontynuacyjną powyższych instrukcji. Możesz przy tym korzystać z gotowych już funkcji semantycznych dla pozostałych kategorii (w semantyce bezpośredniej) syntaktycznych.

Zadanie 3

Rozszerz język z poprzedniego zadania o konstrukcje

$i::=\mathbf{𝐥}\mathbf{𝐨}\mathbf{𝐨}\mathbf{𝐩}i\mathbf{𝐞}\mathbf{𝐧}\mathbf{𝐝}\mathbf{𝐥}\mathbf{𝐨}\mathbf{𝐨}\mathbf{𝐩}|\mathbf{𝐛}\mathbf{𝐫}\mathbf{𝐞}\mathbf{𝐚}\mathbf{𝐤}|\mathbf{𝐜}\mathbf{𝐨}\mathbf{𝐧}\mathbf{𝐭}\mathbf{𝐢}\mathbf{𝐧}\mathbf{𝐮}\mathbf{𝐞}$

Zadanie 4

Uzupełnij definicję języka o bloki, deklaracje zmiennych i procedur oraz wywołanie procedury.

Zadanie 5

Zdefiniuj semantykę denotacyjną następującego języka:

$n::=0|1|\dots$

$x::=\dots (identyfikatory)\dots$

$e::=n|x|e_1+e_2|\mathbf{𝐜}\mathbf{𝐚}\mathbf{𝐥}\mathbf{𝐥}F(x)$

$i::=x:=e|i_1;i_2|\mathbf{𝐬}\mathbf{𝐤}\mathbf{𝐢}\mathbf{𝐩}|\mathbf{𝐢}\mathbf{𝐟}{e}_1=e_2\mathbf{𝐭}\mathbf{𝐡}\mathbf{𝐞}\mathbf{𝐧}{i}_1\mathbf{𝐞}\mathbf{𝐥}\mathbf{𝐬}\mathbf{𝐞}{i}_2|\mathbf{𝐛}\mathbf{𝐫}\mathbf{𝐞}\mathbf{𝐚}\mathbf{𝐤}|\mathbf{𝐫}\mathbf{𝐨}\mathbf{𝐥}\mathbf{𝐥}\mathbf{𝐛}\mathbf{𝐚}\mathbf{𝐜}\mathbf{𝐤}|\mathbf{𝐚}\mathbf{𝐠}\mathbf{𝐚}\mathbf{𝐢}\mathbf{𝐧}$

$p::=\mathbf{𝐛}\mathbf{𝐞}\mathbf{𝐠}\mathbf{𝐢}\mathbf{𝐧}i\mathbf{𝐞}\mathbf{𝐧}\mathbf{𝐝}$

Program i instukcje postaci $\mathbf{𝐛}\mathbf{𝐞}\mathbf{𝐠}\mathbf{𝐢}\mathbf{𝐧}i\mathbf{𝐞}\mathbf{𝐧}\mathbf{𝐝}$ są blokami. Instrukcja break powoduje natychmiastowe wyjście z bloku i wznowienie wykonania od następnej instrukcji po bloku. Instrukcja again to skok do pierwszej instrukcji w najbardziej zagnieżdżonym bloku, w którym wystąpiła. Instrukcja rollback działa podobnie jak break, ale anuluje wszystkie zmiany dokonane od ostatniego wejścia do bloku, w którym wystąpiła.

Wykonanie programu:

 begin
   x := 2;
   begin
     x := x + 1;
     if x = 5 then rollback else again
   end
 end

zakończy się ze zmienną $x$ równą 2. Choć środowiska wydają się tu niepotrzebne, spróbuj wykorzystać je do przechowywania pewnych potrzebnych informacji.