辅导program留学生、Python，Java，c++程序语言调试、data讲解
- 首页 >> Python编程 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 i2. {(s = 2i
) ∧ (i ≤ n)} while iExercise 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 (zy := 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 (zy := 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
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
) ∧ (i ≤ n)} while i
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
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
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