2.4 Proving While Programs Correct

Question 1

What does correctness mean?

Answer 1

Syntactic well-formedness
Properly typed
Well-behaved
Semantic correctness
Termination

Question 2

How are intended or desired behaviours captured

Answer 2

Specification

Two Predicates: Precondition and post-condition.

Question 3

How do we test correctness?

Answer 3

Specification(Pre, Post) ⊆ Actual(P)

Question 4

How do we prove partial correctness?

Answer 4

Take the loop invariant. Show that it is consistent.
Consider what happens when the loop terminates
Add to loop invariant (Pre-condition). Is this the post-condition? Yes- Partially correct

Question 5

What is a loop invariant?

Answer 5

Something that is always true of states before and after the while loop

Question 6

How do we prove Total correctness?

Answer 6

We must show each while-loop will always terminate. To do this we find a loop variant. Combine with partial correctness proof

Question 7

What is a loop variant?

Answer 7

A quantity that strictly decreases on every iteration of the while loop and is bounded so that when it reaches a certain value, the loop terminates

Question 8

What is a hoare triple?

Answer 8

Two predicates and a statement.

partial correctness: {P}S{Q}

Question 9

What is an auxiliary variable?

Answer 9

keeps a record of the initial values.

Question 10

{false} S {Q} is always ….

Answer 10

true

Question 11

P S {false} is always false if … and always true if …..

Answer 11

always false if S terminates

always true if S does no terminate

Question 12

Proof of Hoare triple (no loops)?

Answer 12

{P} S {Q}

1. Apply the rules to decompose into smaller triples to get a sequence of assignments
2. If program contains if statements, we get multiple triples
3. Apply assignment rule backwards to get new precondition Q’
4. Try to prove implications P → Q’

Question 13

Proof of Hoare triple (loops)?

Answer 13

1. Find loop invariant
2. Show it was the invariant for the loop via rule for while
3. Connect loop invariant to pre and post conditions using rule of consequence

Question 14

Describe the rule of consequence

Answer 14

if P → P’
{P’} S {Q} = {P} S {Q}
if Q’ → Q
{P} S {Q’} = {P} S {Q}

Question 15

How do we find a loop invariant?

Answer 15

Start with something we already have. Start with precondition and weaken to get something that works
take {A} while b do S {A ∧¬B[[b]]}
find loop invariant R such that:
A → R
(R ∧ ¬b) → (A ∧ ¬b)
{R ∧ b} S {R}

Question 16

What is the loop variant?
x counts up to 100 and stops
What is the loop invariant?
E1 gets smaller and E2 gets bigger

Answer 16

-x

E1 - E2

Question 17

Give the Hoare triple for total correctness

Answer 17

[P] S [Q]