SEMANTYKA I WERYFIKACJA - Zadanie egzaminacyjne nr 1

(1)

SEMANTYKA I WERYFIKACJA - Zadanie egzaminacyjne nr 1

Napisz semantykę operacyjną dużych kroków języka o następującej grama- tyce:

N um 3 n ::= 0 | 1 | −1 | 2 | −2 | · · · V ar 3 x ::= x | y | · · ·

XN ame 3 w ::= w | v | · · ·

Expr 3 e ::= n | x | e1+ e2| e1∗ e2| e1− e2

BExpr 3 b ::= true | false | e1< e2| e1= e2| b1∨ b2| not b | thrown w(e) Decl 3 d ::= var x := e | d1; d₂

Jest to język z wyjątkami, które mają argumenty liczbowe (wagi) oraz są podnoszone jedynie wtedy, kiedy wiadomo że będą obsłużone.

Instrukcja try I1 catch w(e) I2 rozpoczyna się od obliczenia wartości wy- rażenia e. Następnie wykonuje się instrukcja I1, przy czym deklaruje się w niej, że wyjątek w podniesiony z wagą mniejszą lub równą obliczonej na wstępie war- tości e będzie obsłużony instrukcją I2. Wyjątki o innych nazwach, oraz wyjątki w z większymi wagami, nie są przez tę instrukcję przechwytywane.

Wyrażenie logiczne thrown w(e) podnosi wyjątek w z wagą równą wartości wyrażenia arytmetycznego e, ale tylko jeśli ten wyjątek będzie gdzieś przechwy- cony. Jeżeli nie ma żadnej zadeklarowanej metody obsługi tego wyjątku o tej (lub większej) wadze, to wyjątek nie jest podnoszony a wyrażenie zwraca war- tość false.

Pozostałe konstrukcje mają standardową semantykę.

Na przykład po wykonaniu fragmentu programu x := 0; y := 10;

try

while not (thrown w(y)) do x := x+1; y := y-1 catch w(y-9) x := x+1

zmienna x ma wartość 10, a zmienna y wartość 1.

1

(2)

ROZWIĄZANIE:

Dziedziny semantyczne (funkcje są częściowe bez ostrzeżenia):

s ∈ Store = Loc → Num ρ ∈ Env = Var → Loc χ ∈ XEnv = XName → Num Ogólne postaci stwierdzeń semantycznych:

ρ ` e, s → n wyrażenia arytmetyczne χ, ρ ` b, s → {tt , ff } wyrażenia logiczne χ, ρ ` b, s → w, n

χ, ρ ` I, s → s⁰ instrukcje χ, ρ ` I, s → s⁰, w, n instrukcje d, ρ, s → ρ⁰, s⁰ deklaracje

Reguły dla wyrażeń arytmetycznych są standardowe.

Reguły dla wyrażeń logicznych są standardowe, poza tymi dla wyrażenia thrown. Poza tym trzeba opisać proces propagacji wyjątków i określić kolejność obliczania binarnych wyrażeń logicznych.

ρ ` true, s → tt ρ ` false, s → ff ρ ` e1, s → n1 ρ ` e2, s → n2 n1< n2

χ, ρ ` e₁< e₂, s → tt

ρ ` e1, s → n1 ρ ` e2, s → n2 n1≥ n2

χ, ρ ` e₁< e₂, s → ff ρ ` e₁, s → n₁ ρ ` e₂, s → n₂ n₁= n₂

χ, ρ ` e1= e2, s → tt

ρ ` e₁, s → n₁ ρ ` e₂, s → n₂ n₁6= n₂ χ, ρ ` e1= e2, s → ff

χ, ρ ` b → tt χ, ρ ` not b → ff

χ, ρ ` b → ff χ, ρ ` not b → tt

χ, ρ ` b → w, n χ, ρ ` not b → w, n χ, ρ ` b1, s → tt χ, ρ ` b2, s → tt

χ, ρ ` b₁∨ b2, s → tt

χ, ρ ` b1, s → tt χ, ρ ` b2, s → ff χ, ρ ` b₁∨ b2, s → tt χ, ρ ` b1, s → ff χ, ρ ` b2, s → tt

χ, ρ ` b1∨ b2, s → tt

χ, ρ ` b1, s → ff χ, ρ ` b2, s → ff χ, ρ ` b1∨ b2, s → ff χ, ρ ` b1, s → tt χ, ρ ` b2, s → w, n

χ, ρ ` b₁∨ b₂, s → w, n

χ, ρ ` b1, s → ff χ, ρ ` b2, s → w, n χ, ρ ` b₁∨ b₂, s → w, n χ, ρ ` b₁, s → w, n

χ, ρ ` b1∨ b2, s → w, n ρ ` e, s → n χ(n) ≥ n

χ, ρ ` thrown w(e) → w, n

ρ ` e, s → n undef(χ(n)) χ, ρ ` thrown w(e) → ff

ρ ` e, s → n χ(n) < n χ, ρ ` thrown w(e) → ff Reguły dla instrukcji: wszystkie są standardowe poza tymi dla instrukcji

try-catch. Trzeba też zdefiniować reguły propagowania wyjątków.

2

(3)

Poniżej zmienna θ przebiega zarówno po stanach s jak i po trójkach s, w, n.

χ, ρ ` skip, s → s ρ ` e, s → n

χ, ρ ` x := e, s → s[ρ(x) 7→ n]

χ, ρ ` I₁, s → s⁰ χ, ρ ` I₂, s⁰→ θ χ, ρ ` I1; I2, s → θ

χ, ρ ` I₁, s → s⁰, w, n χ, ρ ` I1; I2, s → s⁰, w, n χ, ρ ` b, s → tt χ, ρ ` I₁, s → θ

χ, ρ ` if b then I1else I2, s → θ χ, ρ ` b, s → ff χ, ρ ` I2, s → θ χ, ρ ` if b then I1else I2, s → θ

χ, ρ ` b, s → w, n

χ, ρ ` if b then I1 else I₂, s → s, w, n

χ, ρ ` b, s → tt χ, ρ ` I, s → s⁰ χ, ρ ` while b do I, s⁰ → θ χ, ρ ` while b do I, s → θ

χ, ρ ` b, s → tt χ, ρ ` I, s → s⁰, w, n χ, ρ ` while b do I, s → s⁰, w, n

χ, ρ ` b, s → w, n χ, ρ ` while b do I, s → s, w, n χ, ρ ` b, s → ff

χ, ρ ` while b do I, s → s d, ρ, π, s → ρ⁰, π⁰, s⁰ χ, ρ⁰ ` I, s⁰ → θ

χ, ρ ` begin d; I end, s → θ

Wszędzie poniżej, χ⁰=

χ[w 7→ n] jeśli undef(χ(w)) lub χ(w) > n χ wpp.

ρ ` e, s → n χ⁰, ρ ` I₁, s → s⁰ χ, ρ ` try I1catch w(e) I2, s → s⁰

ρ ` e, s → n χ⁰, ρ ` I₁, s → v, m s⁰, v 6= w χ, ρ ` try I1 catch w(e) I2, s → s⁰, v, m ρ ` e, s → n χ⁰, ρ ` I1, s → s⁰, w, m m > n

χ, ρ ` try I1 catch w(e) I2, s → s⁰, w, m

ρ ` e, s → n χ⁰, ρ ` I1, s → s⁰, w, m m ≤ n χ, ρ ` I2, s⁰→ θ χ, ρ ` try I1 catch w(e) I2, s → θ

Reguły dla deklaracji są standardowe.

3