代写program留学生、Python，Java，c++程序语言调试、data代做

日期：2020-09-22 11:15

The Australian National University Semester 2, 2020

Research School of Computer Science Tutorial 6

Dirk Pattinson and Victor Rivera

Foundations of Computation

The tutorial contains a number of exercises designed for the students to practice the course content. During the lab,

the tutor will work through some of these exercises while the students will be responsible for completing the remaining

exercises in their own time. There is no expectation that all the exercises will be covered in lab time.

Covers: Lecture Material Week 6

At the end of this tutorial, you will be able to prove the partial and total correctness of imperative programs using Hoare

Logic.

Exercise 1 Hoare Logic: Simple Loops

Consider the Hoare triple

{P}while x>a do x:=x-1{x = 0}

where P is an (as of yet unspecified) predicate.

1. find the weakest precondition P (in terms of x and a) that makes this Hoare-triple true. Justify your answer briefly

(no formal proof required).

2. Give a proof of validity of this triple, using the precondition P that you have identified above.

Exercise 2 Find the Invariant

Consider the following Hoare triple, where n ≥ 0 is an unspecified integer:

{ i = 0 /\ s = 0 }

while (i < n) do

i := i + 1

s := s + i;

{ s = n * (n+1) / 2 }

1. Complete the table below

loop iteration 0 1 2 3 4

i 0

s 0

by filling in the values of i and s after the first, second, etc. iteration of the loop. The values for the 0th loop iteration

are the initial values of i and s that are given by the precondition.

2. Using the table above, derive an invariant I, that is, a relation between s and i, that holds both before the loop is

being entered, and after each iteration of the loop body.

3. Check whether the invariant that you have found is strong enough so that – together with the negation of the loop

condition – implies the desired postcondition, and if not, modify the invariant accordingly.

That is, verify whether I ∧ ?(i < n) → s = n ? (n + 1)/2, and modify the invariant if this is not the case.

4. Hence, or otherwise, give a Hoare Logic proof of the Hoare triple above.

Exercise 3 Find The Variant

Consider the following Hoare triple, but now formulated in terms of total correctness, where again n ≥ 0 is an unspecified

integer.

1

[ i = 0 /\ s = 0 ]

while (i < n) do

i := i + 1

s := s + i;

[ s = n * (n+1) / 2 ]

1. Identify and state a variant E for the loop. Using the same invariant I as in the previous exercise, the variant should

have the following two properties:

? it should be ≥ 0 when the loop is entered, i.e. I ∧ (i < n) → E ≥ 0

? it should decrease every time the loop body is executed, i.e. [I ∧ b ∧ E = k] body [I ∧ E < k]

where body stands for the body of the loop. You just need to state the variant, and do not need to prove the two

bullet points above (yet).

2. For the variant E that you have identified, give a proof of the premise of the while-rule for total correctness, i.e.

give a Hoare-logic proof of [I ∧ (i < n) ∧ E = k] body [I ∧ E < k], and argue that I ∧ (i < n) → E ≥ 0.

3. Hence, or otherwise, give a Hoare-logic proof of [I] while (i <= n) do body [I ∧ ?b].

Exercise 4 More While Loops

Give a proof of the following Hoare-triples, where you may use that we have established the validity of {s = 2i}

i:=i+1; s:=s*2 {s = 2i} in Tutorial 5.

1. {s = 2i} while i<n do i:=i+1; s:=s*2 {s = 2i}

2. {(s = 2i

) ∧ (i ≤ n)} while i<n do i:=i+1; s:=s*2 {s = 2n}

Exercise 5 Multiplication (Partial Correctness)

Consider the following (annotated) program that multiplies two numbers by means of repeated addition:

{n >= 1}

p := 0;

i := 1;

while (i <= n) do

p := p+m;

i := i+1

{p = m * n}

1. Identify the strongest mid-condition M for which the Hoare-triple

{n >= 1}

p := 0;

i := 1;

{ M }

is provable, and give a Hoare-logic proof of this fact.

2. Identify an invariant I for the loop. The invariant should have the following three properties:

? it should be strong enough to imply the postcondition if the loop condition is false: I ∧?(i ≤ n) → p = m?n

? it should be weak enough so that it is implied by the mid-condition M, that is M → I.

? it should be an invariant, i.e {I ∧ (i ≤ n)} body {I} should be provable.

State the invariant, and give a Hoare-Logic proof of {I ∧ (i < n)} body {I} where body is the body of the

while-loop.

3. Using the above, give a proof of the Hoare-triple given by the annotated program at the beginning of the exercise.

2

Exercise 6 Multiplication (Total Correctness)

We consider the same program fragment as above, but now the goal is to establish total correctness.

[n >= 1]

p := 0;

i := 1;

while (i <= n) do

p := p+m;

i := i+1

[p = m * n]

1. Identify and state a variant E for the loop. Using the same invariant I as in the previous exercise, the variant should

have the following two properties:

? it should be ≥ 0 when the loop is entered, i.e. I ∧ b → E ≥ 0

? it should decrease every time the loop body is executed, i.e. [I ∧ b ∧ E = k] body [I ∧ E < k]

where body stands for the body of the loop. You just need to state the variant, and do not need to prove the two

bullet points above (yet).

2. For the variant E that you have identified, give a proof of the premise of the while-rule for total correctness, i.e.

give a Hoare-logic proof of [I ∧ b ∧ E = k] body [I ∧ E < k], and argue that I ∧ b → E ≥ 0.

3. Hence, or otherwise, give a Hoare-logic proof of [I] while (i <= n) do body [I ∧ ?b].

Exercise 7 Fibonacci Numbers

Recall the Fibonacci numbers defined by f(0) = 0, f(1) = 1 and f(n) = f(n ? 2) + f(n ? 1) for n ≥ 2 and consider

the following code fragment that we have annotated with pre and postcondition.

{ x = 0 /\ y = 1 /\ z = 1 /\ n >= 1}

while (z<n) do

y := x+y;

x := y-x;

z := z+1

{ y = f(n) }

1. Identify an invariant I for the loop. The invariant should have the following three properties:

? it should be strong enough to imply the postcondition if the loop condition is false: I∧?(z < n) → y = f(n).

? it should be weak enough so that it is implied by the precondition, that is x = y ∧y = 1∧z = 1∧n ≥ 1 → I.

? it should be an invariant, i.e {I ∧(i ≤ n)} body {I} should be provable, where body is the body of the loop.

State the invariant, and give a Hoare-Logic proof of the fact that I is indeed an invariant, i.e. show that {I ∧ (z <

n)} y := x + y; x := y ? x; z := z + 1 {I} is provable in Hoare Logic.

Hint. At what positions in the Fibonacci sequence do x and y occur?

2. Hence, or otherwise, establish the validity of the Hoare triple given by the annotated program above.

Exercise 8 Total Correctness

Consider the program that computes Fibonacci numbers from the previous exercise, but from the perspective of total

correctness. That is, we want to establish provability of the following Hoare triple:

[ x = 0 /\ y = 1 /\ z = 1 /\ n >= 1 ]

while (z<n) do

y := x+y;

x := y-x;

z := z+1

[ y = f(n) ]

3

1. We use the same invariant I as above (which allows us to copy some of the steps). State the correct variant E for

the loop. The variant should have the following two properties:

? it should be ≥ 0 when the loop is entered, i.e. I ∧ (z < n) → E ≥ 0

? it should decrease every time the loop body is executed, i.e. [I ∧ b ∧ E = k] body [I ∧ E < k]

where body stands for the body of the loop as above.

2. 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 [I ∧ (z < n) ∧ E = k] body [I ∧ E < k] and argue that I ∧ b → E ≥ 0.

3. Hence, or otherwise, establish the provability of the Hoare-triple given by the annotated program at the beginning

of the exercise.

Exercise 9 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 I 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

{I}Body{I}.

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

4. Give an example of a precondition I so that the Hoare-triple {I}Count{x < 7} does not hold and justify your

answer briefly.

4

Appendix — Hoare Logic Rules

? Assignment:

{Q(e)} x := e {Q(x)}

? Precondition Strengthening:

Ps → Pw {Pw} S {Q}

{Ps} S {Q}

? Postcondition Weakening:

{P} S {Qs} Qs → Qw

{P} S {Qw}

? Sequence:

{P} S1 {Q} {Q} S2 {R}

{P} S1; S2 {R}

? Conditional:

{P ∧ b} S1 {Q} {I ∧ ?b} S2 {Q}

{P} if b then S1 else S2 {Q}

? While Loop:

{I ∧ b} S {I}

{I} while b do S {I ∧ ?b}

? While Loop (Total Correctness):

I ∧ b → E ≥ 0 [I ∧ b ∧ E = n] S [I ∧ E < n]

[I] while b do S [I ∧ ?b]

where n is an auxiliary variable not appearing anywhere else.

5