CSE Assignment 3 Solution

Description

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 ! ⁰ where (x) = 7, (y) = 2, ⁰ (x) = 7, ⁰ (y) = 9.

2. (10 pts) Which of the following results (i.e., Hoare triples) are valid?

2. 1. { true } x := 2 { true }

2. 2. { true } x := x { false }

2. 3. { false } x := 2 { true }

2. 4. { false } x := 2 { false }

2. 5. { true } while true do x := 2 { false }

2. 6. { true } x := x + 1 { x = x + 1 }

2. 7. { x = y } t := x; x := y; y := t { x = y }

2. 8. { x >= 0 } x := y { y >= 0 }

2. 9. { x = 0 } while x < 10 do x := x – 1 { x = x + 1 }

2. 10. { x = 0 } while x < 10 do x := x + 1 { x = x + 1 }

2. (5 pts) Consider the following valid triple

{true}

if x>y 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