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.