首页 >
> 详细

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

) ∧ (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

联系我们

- QQ：99515681
- 邮箱：99515681@qq.com
- 工作时间：8:00-23:00
- 微信：codinghelp2

- 代写data留学生作业、代做analysis课程作业、代写python，C+ 2020-09-30
- 代写data Analysis作业、代做python，Java程序语言作业、 2020-09-30
- Program课程作业代写、代做python，Java，C++程序语言作业、 2020-09-30
- 代做sit202课程作业、Networks作业代做、Java，C++程序设计 2020-09-30
- 代写data留学生作业、代做c++课程设计作业、C++程序语言作业调试代写留 2020-09-30
- 159100留学生作业代做、代写programming作业、C++编程语言作 2020-09-29
- Engineering作业代做、代写html/Css语言作业、代写web程序 2020-09-29
- 代写kit206/506作业、代做system课程作业、代写sql程序设计作 2020-09-29
- Lab 2 Jsf作业代做、Java编程语言作业调试、Java实验作业代写、 2020-09-29
- 代写mis275留学生作业、代做analytics作业、代做python，J 2020-09-28
- Html留学生作业代做、代写css/Java编程语言作业、代做java实验作 2020-09-28
- Comp3278作业代写、Database作业代做、代写sql实验作业、Sq 2020-09-28
- Macm 204课程作业代做、C/C++，Java，Python程序设计作业 2020-09-28
- Cis 484作业代做、代写sql编程语言作业、代做sql课程设计作业、代写 2020-09-27
- 代写kit206课程作业、代做software留学生作业、代写c++程序语言 2020-09-27
- Comp2100作业代做、代写programming作业、C/C++编程设计 2020-09-27
- Msbd5015作业代写、Python编程语言作业调试、代写python课程 2020-09-27
- Programming作业代写、Java程序设计作业调试、代做algorit 2020-09-27
- Cisc 360作业代做、代写java程序设计作业、Python，C++语言 2020-09-27
- Cs 570留学生作业代做、Java程序语言作业调试、代写java课程设计作 2020-09-27