4 grudnia 2003

Zadanie 1 Dany jest j_{}ezyk programowania: Składnia

• e ::= n | v | (e + e′) | (e − e′)

• b ::= t | b∨b′ | e = e′ | e <= e′ | ¬b ^{1}

• c ::= \underline{skip} | v := e | c; c′ | \underline{if} e \underline{then} c1, c2 gdzie n ∈ {…, −1, 0, 1, …}–zbiór liczb całkowitych, a t ∈ {tt, ff}–zbór stałych logicznych.

Zakładaj _{}ac, że dana jest semantyka operacyjna wyrażeń arytmetycznych i boolowskich oraz zdefiniowane s _{}a reguły dla instrukcji pustej, przypisania i złożenia instrukcji, podać reguły dla konstrukcji

\underline{if} e \underline{then} c1, c2

której znaczenie jest nast_{}epuj _{}ace^{2}:

1. jeśli wartość wyrażenia e ≥ 0, to wykonywana jest instrukcja c1

2. jeśli wartość wyrażenia e ≤ 0, to wykonywana jest instrukcja c2 a nast_{}epnie zdefiniowac semantyk_{}e operacyjn _{}a instrukcji.

1Maj _{}ac zdefiniowane =, <= i¬ możemy uznać, że zdefiniowane s _{}a wszystkie relacje pochodne, tzn. <, >, >=, <>

2Zauważmy, że jest ona niedeterministyczna.

Zadanie 2 J_{}ezyk programowania zdefiniowany jest nast_{}epuj _{}aco: Składnia

• e ::= m | v | (e + e′)

• d ::= \underline{var} v | \underline{proc} P (v); c \underline{endproc} | d1; d2

• c ::= v := e | c; c′ | \underline{begin} d; c \underline{end} | \underline{call} P (e) Dziedziny semantyczne

• Loc = {l_{0}, l_{1}, …} – zbiór lokacji (nieskończony).

• Sv = N

• S = [Loc → Sv + \{ \underline{wolna} \}]

• P roc = [Loc → [S → S_{⊥}]]

• Dv = Loc + P roc + \{ \underline{puste} \}

• Env = [Ide → Dv]

• new : S → Loc × S dla s ∈ S new(s) = (l_{i}, s[0/l_{i}]), gdzie i = min\{j | s(l_{j}) = \underline{wolna} ∧ i ≥ 0\}

Funkcje semantyczne A : Aexp → [Env → [S → N_{⊥}]] D : Decl → [Env → [S → Env × S]] C : Com → [Env → [S → S_{⊥}]]

Równania semantyczne Aexp

A[[n]] = λρ ∈ Env.λs ∈ S.n

A[[v]] = λρ ∈ Env.λs ∈ S.if ρv ∉ Loc then ⊥_{N} else if s(ρv) = ⊥_{N} then ⊥_{N}

else s(ρv)

A[[e_{0} + e_{1}]] = λρ ∈ Env.λs ∈ S.if A[[e_{0}]]ρs = ⊥_{N} then ⊥_{N} else

if A[[e_{1}]]ρs = ⊥_{N} then ⊥_{N} else (A[[e_{0}]]ρs + A[[e_{1}]]ρs)

Decl D[[ \underline{var} v]] = λρ ∈ Env.λs ∈ S.(ρ[(new(s))_{1}/v], (new(s))_{2}) D[[d_{1}; d_{2}]] = λρ ∈ Env.λs ∈ S.D[[d_{2}]](D[[d_{1}]]ρs)_{1}(D[[d_{1}]]ρs)_{2} D[[ \underline{proc} P (v); c \underline{endproc} ]] = λρ ∈ Env.λs ∈ S.(ρ[f/P], s) gdzie f ∈ P roc jest zdefiniowana nast_{}epuj _{}aco:

f = λl ∈ Loc.λs′ ∈ S.if l ∉ Loc then ⊥_{s} else C[[c]]ρ[l/v]s′ Com

C[[v := e]] = λρ ∈ Env.λs ∈ S.if ρv ∉ Loc then ⊥_{S} else if A[[e]]ρs = ⊥_{N} then ⊥_{S} else s[A[[e]]ρs/ρv]

C[[c_{1}; c_{2}]] = λρ ∈ Env.λs ∈ S.if C[[c_{1}]]ρs = ⊥_{S} then ⊥_{S} else C[[c_{2}]]ρ(C[[c_{1}]]ρs)

C[[ \underline{begin} d; c \underline{end} ]] = λρ ∈ Env.λs ∈ S.C[[c]](D[[d]]ρs)_{1}(D[[d]]ρs)_{2}

C[[ \underline{call} P (e)]] = λρ ∈ Env.λs ∈ S.if ρP ∉ P roc then ⊥_{S} else if A[[e]]ρ ∈ Loc then (ρP)(A[[e]]ρ)s else if A[[e]]ρs ∈ Sv then (let(l′′, s′′) = new(s) in ρP (l′′)(s′′[A[[e]]ρs/l′′]) else ⊥_{S}.

Podaj wartość zmiennych x, y po wykonaniu programu:

(a)

\underline{begin} \underline{var} x; \underline{var} y; \underline{proc} P(a);a:=a+1; x:=x+a \underline{endproc} ; x:=5; y:=2; P(y); P(x+y)

{x= ,y= } \underline{end} ;

(b)

\underline{begin} \underline{var} x; \underline{var} y; \underline{proc} P(a); x:=x+a ; a:=x+1 \underline{endproc} x:=5; y:=2; P(y); P(7)

{x= ,y= } \underline{end} ; Zadanie 3 Uzasadnij poprawność cz_{}eściow _{}a programu wzgl_{}edem danej specyfikacji wstawiaj _{}ac stosowne asercje w nawiasy klamrowe.

{a ∈ N ∧ d ∈ N ∧ a ≥ 0 ∧ d > 0}

{                                                    }
r:=a; q:=0;
{                                                  }
while r>=d do
{                                                  }
begin
{                                                  }
dd:=d;
qq:=1;
{                                                  }
while r>= dd do
{                                                  }
   begin
   {                                               }
   r:=r-dd;
   dd:=dd+dd;
   q:=q+qq;
   qq:=qq+qq
   {                                               }
   end
{                                                  }
end;

{d ∗ q + r = a ∧ 0 <= r < d}