This assignment contains 3 questions, for a total of 20 points.
1. (5 pts) Consider the big-step operational semantics de ned in class. Show the entire
derivation tree for deriving hif x y then y := x + y else y := x y; i ! 0 where (x) = 7, (y) = 2, 0 (x) = 7, 0 (y) = 9.
2. (10 pts) Which of the following results (i.e., Hoare triples) are valid?
(a) { true } x := 2 { true }
(b) { true } x := x { false }
(c) { false } x := 2 { true }
(d) { false } x := 2 { false }
(e) { true } while true do x := 2 { false }
(f) { true } x := x + 1 { x = x + 1 }
(g) { x = y } t := x; x := y; y := t { x = y }
(h) { x = 0 } x := y { y = 0 }
(i) { x = 0 } while x < 10 do x := x - 1 { x = x + 1 }
(j) { x = 0 } while x < 10 do x := x + 1 { x = x + 1 }
3. (5 pts) Consider the following valid triple
{true}
if xy then z:=(y-x)-1 else z:=(x-y)-1;
z:=1-12*z
{ z=10 }
Show the entire derivation tree for deriving this triple, using the axiomatic semantics rules discussed in class. The \bottom" (i.e. root) of the tree should be this triple. A leaf of the tree is either (1) a triple that can be directly derived from an axiom, or (2) an implication ) used in the rule of consequence. You must show explicitly all implications ) you have used when applying the rule of consequence.
1
