SEMANTYKA I WERYFIKACJA - Zadanie domowe nr 1
Napisz semantykę operacyjną, zarówno małych jak i dużych kroków, instruk- cji języka o następującej gramatyce:
N um 3 n ::= 0 | 1 | −1 | 2 | −2 | · · · V ar 3 x ::= x | y | · · ·
Expr 3 e ::= n | x | e1+ e2| e1∗ e2| e1− e2
BExpr 3 b ::= true | false | e1< e2| e1= e2| b1∧ b2| ¬b Instr 3 I ::= skip | x := e | I1; I2| if b then I1 else I2| while b do I | catch e in I | escape-with e
Wyliczanie wyrażeń arytmetycznych i logicznych odbywa się standardowo. Można założyć, że semantyka wyrażeń jest dana.
Instrukcja catch e in I wykonuje się tak jak instrukcja I, ale najpierw ustala koszt ucieczki z instrukcji I na aktualną wartość wyrażenia e.
Instrukcja escape-with e próbuje przerwać wykonywanie jednej lub więcej otaczających ją instrukcji catch. Aktualna wartość wyrażenia e to cena, jaką jest gotowa za to zapłacić, a każda kolejna instrukcja catch pobiera z tej war- tości swój ustalony wcześniej koszt. Jeżeli pozostająca cena jest mniejsza od kosztu kolejnej ucieczki, to ta ucieczka nie następuje.
Przykładowo, rozważmy fragment programu z := 0;
catch 1 in catch 2 in
catch 3 in escape-with x;
z := z+1;
z := z+10;
z := z+100;
Jeżeli x < 3, to na końcu z = 111. Jeżeli x = 5, to na końcu z = 100. Jeżeli x ≥ 6, to na końcu z = 0.
Inny przykład: po wykonaniu programu x := 10; y := 0; z := 0;
catch x in while true do
y := y+1;
catch x in escape-with y;
z := z+1
zmienna y przyjmie wartość 20, a zmienna z wartość 9.
Pozostałe konstrukcje mają standardową semantykę. Można założyć, że in- strukcja escape-with będzie wykonywana tylko wewnątrz co najmniej jednej instrukcji catch. Zakładamy też, że w instrukcjach catch e i escape-with e, wyrażenie e będzie przyjmować tylko wartości nieujemne.
1
SZKIC PRZYKŁADOWEGO ROZWIĄZANIA
Załóżmy, że dana jest denotacyjna semantyka wyrażeń arytmetycznych i logicznych, tzn. funkcje
[[_]] : Expr → State → Num
[[_]] : BExpr → State → {true, false}
Semantyka małych kroków. Do zwykłych konfiguracji dodajemy nowy składnik: liczbę naturalną, która oznacza koszt ucieczki z najbliższej instrukcji catch:
State ∪ Instr × State × N z przejściami postaci
n ` I, s → I0, s0 lub n ` I, s → s0 Reguły dla catch i escape-with są następujące:
[[e]]s = n
k ` catch e in I, s → catch n in I0, s0 n ` I, s → I0, s0
k ` catch n in I, s → catch n in I0, s0 n ` I, s → s0
k ` catch n in I, s → s0 m ≥ n
k ` catch n in escape-with m, s → escape-with m − n, s m < n
k ` catch n in escape-with m, s → I, s
Trzeba jeszcze dodać reguły dla sekwencji, aby ucieczka z instrukcji przerywała ją:
[[e]]s ≥ k
k ` escape-with e; I, s → escape-with e, s [[e]]s < k
k ` escape-with e, s → s
Reguły dla skip, przypisania, sekwencji, if i while są takie jak podano na wy- kładzie, z oczywistym uwzględnieniem dodatkowego komponentu konfiguracji.
Semantyka dużych kroków. Rozbudujmy konfiguracje początkowe o liczby naturalne, które określają koszt ucieczki z najbliższej instrukcji catch:
Instr × State × N.
2
Konfiguracje końcowe także rozszerzmy o liczby naturalne, które będą ozna- czać cenę jaką instrukcja jest gotowa zapłacić za dalszą ucieczkę po ucieczce z najbliższej pętli:
State × N, czyli przejścia będą postaci
I, s, n → s0, m.
Reguły dla catch i escape-with:
I, s, n → s0, m
catch n in I, s, k → s0, k − m
escape-with e, s, n → s, n − [[e]]s i zmienione reguły dla sekwencji:
S1, s, n → s0, k k ≥ 0 S1; S2, s, n → s0, k
S1, s, n → s0, k k < 0 S2, s0, n → s00, k0 S1; S2, s, n → s00, k0
Reguły dla pozostałych konstrukcji są standardowe, z tym że trzeba je uzu- pełnić o dodatkowe składniki w trywialny sposób.
3
