21 czerwca 2004

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{do} e \underline{times} c gdzie n ∈ {…, −1, 0, 1, …}–zbiór liczb całkowitych, a t ∈ {tt, ff}–zbór stałych logicznych.

Zakładaj _{}ac, że semantyka operacyjna wyrażeń arytmetycznych i boolowskich oraz instrukcji pustej, przypisania i złożenia instrukcji jest standardowa i dane s _{}a dla nich reguły (patrz wykład), zdefiniować za pomoc _{}a semantyki operacyjnej konstrukcj_{}e \underline{do} e \underline{times} c. Znaczenie tej konstrukcji ma być nast_{}epuj _{}ace: instrukcja c wykonuje si_{}e tyle razy, ile wskazuje wartość wyrażenia e. Podać reguły przy założeniu, że

1. wartość wyrażenia e wyliczana jest tylko raz przed pierwszym wykonaniem p_{}etli;

2. wartość wyrażenia e wyliczana jest przed każdym wykonaniem p_{}etli. W obu przypadkach uwzgl_{}ednić możliwość powstania bł_{}edów (np. e < 0).

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

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

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

• d ::= \underline{var} v | \underline{eqv} (v, v′) | d; d′

• c ::= \underline{skip} | v := e | c; c′ | \underline{begin} d; c \underline{end} Dziedziny semantyczne

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

• Sv = N

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

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

• Env = [Ide → Dv]

• new : S → Loc × S dla s ∈ S

new(s) = \{ \begin{matrix}(l_{i}, s[0/l_{i}]) & ∃j.s(l_{j}) = \underline{wolna} ∧ \\ & i = min\{j | s(l_{j}) = \underline{wolna} \} \\ (l_{0}, s[0/l_{0}]) & w p.p. \end{matrix}

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

Równania semantyczne A[[n]] = λρ ∈ Env.λs ∈ S.n A[[v]] = λρ ∈ Env.λs ∈ S.if ρv ∈ Loc then s(ρv) else ⊥_{N} A[[e + e′]] = λρ ∈ Env.λs ∈ S.if A[[e]]ρs = ⊥_{N} then ⊥_{N} else

if A[[e′]]ρs = ⊥_{N} then ⊥_{N} else (A[[e]]ρs + A[[e′]]ρs)

D[[ \underline{var} v]] = λρ ∈ Env.λs ∈ S.(ρ[(new(s))_{1}/v], (new(s))_{2}) D[[ \underline{eqv} (v, v′)]] = λρ ∈ Env.λs ∈ S.(ρ[ρv′/v], s) D[[d; d′]] = λρ ∈ Env.λs ∈ S.D[[d′]](D[[d]]ρs)_{1}(D[[d]]ρs)_{2} C[[\underline{skip}]] = λρ ∈ Env.λs ∈ S.s

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[[ \underline{begin} d; c \underline{end} ]] = λρ ∈ Env.λs ∈ S.C[[c]](D[[d]]ρs)_{1}(D[[d]]ρs)_{2}

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

Podaj wartości zmiennych x, y i z we wskazanych momentach programu:

(a)

\underline{begin} \underline{var} x; \underline{var} y; x:=1; y:=2; \underline{begin}

\underline{var} z; \underline{eqv} (y,x)

y:=8; z:=x+y

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

\underline{end} ;

(b)

\underline{begin} \underline{var} x; \underline{var} y; \underline{var} z; y:=2; z:=3; \underline{begin}

\underline{eqv} (y,x);

y:=x+z;

{y= , x= }

\underline{begin} \underline{var} x; x:=3; z:=x+y;

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

\underline{end} ; Zadanie 3 Udowodnij poprawność programu wzgl_{}edem danej specyfikacji wstawiaj _{}ac stosowne asercje w nawiasy klamrowe.

{X > 1 ∧ Y ≥ 0}

{                                                    }
x:=X;
y:=Y;
z:=1;
{                                                     }
while y<>0 do
{                                                     }
    begin
    {                                                 }
    while 2|y do
    {                                                 }
       begin
       {                                              }
       x:=x*x;
       y:=y/2;
       {                                                }
       end;
    {                                                   }
    {                                                   }
    y:=y-1;
    z:=z*x
{                                                       }
    end;

{z = X^{Y} }