Question 1 Hoare Logic Semantics For each of the parts below, justify your answer briefly. 1. For...

Question 1

Hoare Logic Semantics

For each of the parts below, justify your answer briefly. 1. For which programs S does {False} S {True} hold? 2. For which programs S does {True} S {False} hold? 3. For which programs S does [True] S [True] hold?

Question 2

Doubling Numbers

The following piece of code is called Half: x := 0; y := 0; while (x < a)=""> x := x + 2; y := y + 1;

We wish to use Hoare Logic to show that:

{True} Half {x = 2 ∗ y}

In the questions below (and your answers), we may refer to the loop code as Loop, the body of the loop (i.e. x:=x+2;y:=y+1;) as Body, and the initialisation assignments (i.e. x:=0;y:=0;) as Init.

1. Given the desired postcondition {x = 2 ∗ y}, what is a suitable invariant for Loop? (Hint: notice that the postcondition is independent of the value of a.)

2. Prove that your answer to the previous question is indeed a loop invariant. That is, if we call your invariant P , show that {P } Body {P }. Be sure to properly justify each step of your proof.

3. Using the previous result and some more proof steps show that

{True} Half {x = 2 ∗ y} Be sure to properly justify each step of your proof.

4. To prove total correctness of the program Half, identify and state a suitable variant for the loop. Using the same invariant P as above, the variant E should have the following two properties:

- it should be ≥ 0 when the loop is entered, i.e. P ∧ (x < a)="">→ E ≥ 0 - it should decrease every time the loop body is executed, i.e. [P ∧ (x < a)="">∧ E = k] Body [P ∧ E < k]="" 1="">

You just need to state the variant, and do not need to prove the two bullet points above (yet).

5. For the variant E you have identified above, give a proof of the premise of the while-rule for total correctness, i.e. give a Hoare-logic proof of [P ∧ (x < a)="">∧ E = k] Body [P ∧ E < k]="" and="" argue="" that="" p="">∧ (x < a)="">→ E ≥ 0.

Question 3

Counting Modulo 7

Consider the following code fragment that we refer to as Count below, and we refer to the body of the loop (i.e. the two assignments together with the if-statement) as Body.

while (y < n)=""> y := y + 1; x := x + 1; if (x = 7) then x := 0 else x := x

The goal of the exercise is to show that {x < 7}count{x="">< 7}="">

1. Given the desired postcondition, what is a suitable invariant P for the loop? You just need to state the invariant.

2. Give a Hoare Logic proof of the fact that your invariant above is indeed an invariant, i.e. prove the Hoare-triple {P }Body{P }.

3. Hence, or otherwise, give a Hoare-logic proof of the triple {x < 7}count{x="">< 7}.="">

4. Give an example of a precondition P so that the Hoare-triple {P }Count{x < 7}="" does="" not="" hold="" and="" justify="" your="" answer="" briefly.="">