Program Correctness OOSC2 Chapter 11
EECS3311 M: Software Design Winter 2019
CHEN-WEI WANG
Motivating Examples (1)
Is this feature correct?
class FOO
i: INTEGER increment_by_9
require
do
i := i + 9 ensure
i > 13 end
end
i>3
Q: Is i > 3 is too weak or too strong?
A: Too weak
∵ assertion i > 3 allows value 4 which would fail postcondition.
3 of 45
Weak vs. Strong Assertions
● Describe each assertion as a set of satisfying value. x >3hassatisfyingvalues{x x >3}={4,5,6,7,…} x >4hassatisfyingvalues{x x >4}={5,6,7,…}
● An assertion p is stronger than an assertion q p’s set of satisfying values is a subset of q’s set of satisfying values.
○ Logically speaking, p being stronger than q (or, q being weaker
than p) means p ⇒ q. ○ e.g.,x >4⇒x >3
○ A weaker postcondition has more acceptable output values 2 of 45
● What’s the weakest assertion?
● What’s the strongest assertion?
● In :
[ TRUE ] [ FALSE ]
Design by Contract
○ A weaker has more acceptable object states
e.g., balance > 0 vs. balance > 100 as an invariant for ACCOUNT
if
invariant
○ A weaker precondition has more acceptable input values
Motivating Examples (2)
Is this feature correct?
class FOO
i: INTEGER increment_by_9
require
do
i := i + 9 ensure
i > 13 end
end
i>5
Q: Is i > 5 too weak or too strong?
A: Maybe too strong
∵ assertion i > 5 disallows 5 which would not fail postcondition.
Whether 5 should be allowed depends on the requirements.
4 of 45
Software Correctness
● Correctness is a relative notion:
consistency ofimplementationwithrespecttospecification.
⇒ This assumes there is a specification!
● We introduce a formal and systematic way for formalizing a
program S and its (pre-condition Q and post-condition R) as a : {Q} S {R}
specification
○ e.g.,{i>3}i := i + 9{i>13} ○ e.g.,{i>5}i := i + 9{i>13}
Boolean predicate
○ If {Q} S {R} can be proved TRUE, then the S is correct. e.g.,{i>5}i := i + 9{i>13}canbeprovedTRUE.
○ If {Q} S {R} cannot be proved TRUE, then the S is incorrect.
e.g.,{i>3}i := i + 9{i>13}cannotbeprovedTRUE. 5 of 45
Hoare Logic and Software Correctness
Consider the of a feature f (whose body of
implementation is S) as a
{Q} S {R} Qisthe precondition off.
S is the implementation of f . Risthe postcondition off.
:
7 of 45
All inputs/outputs are valid (No contracts) [ Least informative ]
contract view
○ {true} S {R}
All input values are valid
[ Most-user friendly ]
○ {false} S {R}
All input values are invalid
[ Most useless for clients ]
○ {Q} S {true}
Hoare Triple
All output values are valid [ Most risky for clients; Easiest for suppliers ]
○ {Q} S {false}
All output values are invalid [ Most challenging coding task ]
○ {true} S {true}
Hoare Logic
● Consider a program S with precondition Q and postcondition R.
○ {Q} S {R} is a correctness predicate for program S
○ {Q} S {R} is TRUE if program S starts executing in a state
satisfying the precondition Q, and then:
(a) The program S terminates.
(b) Given that program S terminates, then it terminates in a state satisfying the postcondition R.
● Separation of concerns (a) requires a proof of (b) requires a proof of Proofs of (a) + (b) imply
.
.
.
6 of 45
termination
partial correctness
total correctness
Proof of Hoare Triple using wp {Q}S{R} ≡ Q⇒wp(S,R)
● wp(S, R) is the weakest precondition for S to establish R .
● S can be:
○ Assignments (x := y)
8 of 45
○ Alternations (if … then … else … end) ○ Sequential compositions (S1 ; S2 )
○ Loops (from … until … loop … end)
● We will learn how to calculate the wp for the above programming constructs.
Hoare Logic A Simple Example
Given {??}n ∶= n + 9{n > 13}:
● n > 4 is the weakest precondition (wp) for the given implementation (n := n + 9) to start and establish the postcondition (n > 13).
● Any precondition that is equal to or stronger than the wp (n > 4) will result in a correct program.
e.g., {n > 5}n ∶= n + 9{n > 13} can be proved TRUE.
● Any precondition that is weaker than the wp (n > 4) will result
in an incorrect program.
e.g., {n > 3}n ∶= n + 9{n > 13} cannot be proved TRUE.
Counterexample: n = 4 satisfies precondition n > 3 but the output n = 13 fails postcondition n > 13.
9 of 45
wp Rule: Assignments (1)
wp(x := e, R)=R[x ∶=e]
R[x ∶= e] means to substitute all free occurrences of variable x in
postcondition R by expression e.
11 of 45
Denoting New and Old Values
In the , for a program variable x:
○ We write to denote its pre-state (old) value. ○ We write to denote its post-state (new) value.
postcondition
x0
x
10 of 45
Implicitly, in the precondition , all program variables have their pre-state values.
e.g.,{b0 >a}b := b – a{b=b0−a} ● Notice that:
○ We may choose to write “b” rather than “b0” in preconditions ∵ All variables are pre-state values in preconditions
○ We don’t write “b0” in program
∵ there might be multiple intermediate values of a variable due to sequential composition
wp Rule: Assignments (2)
Recall:
Howdoweprove{Q}x := e{R}?
12 of 45
{Q}S{R} ≡ Q⇒wp(S,R)
{Q}x := e{R} ⇐⇒ Q⇒ R[x∶=e]
wp(x := e,R)
wp Rule: Assignments (3) Exercise
What is the weakest precondition for a program x := x + 1 to
establish the postcondition x > x0?
{??}x := x + 1{x >x0}
For the above Hoare triple to be TRUE, it must be that ??⇒wp(x := x + 1,x>x0).
wp(x := x + 1,x>x0)
= {Rule of wp: Assignments}
True
Any precondition is OK.
13 of 45
x >x0[x ∶=x0 +1]
= {Replacing x by x0 + 1}
x0 + 1 > x0
= {1 > 0 always
true}
False is valid but not useful.
wp Rule: Alternations (1)
B⇒wp(S1,R) wp(if B then S1 else S2 end, R)= ∧¬B ⇒wp(S2,R)
The wp of an alternation is such that all branches are able to establish the postcondition R.
15 of 45
wp Rule: Assignments (4) Exercise
What is the weakest precondition for a program x := x + 1 to
establish the postcondition x > x0?
{??}x := x + 1{x =23}
For the above Hoare triple to be TRUE, it must be that ??⇒wp(x := x + 1,x=23).
x0 + 1}
wp(x := x + 1,x=23)
= {Rule of wp: Assignments}
x =23[x ∶=x0 +1]
= {Replacing x by
x0 + 1 = 23
= {arithmetic}
x0 = 22
Any precondition weaker than x = 22 is not OK. 14 of 45
wp Rule: Alternations (2) Recall: {Q} S {R} ≡ Q ⇒ wp(S, R)
How do we prove that {Q} if B then S1 else S2 end {R}?
{Q}
if B then
{Q∧B}S1 {R} else
{Q∧¬B}S2 {R} end
{R}
{Q}if B then S1 else S2 end{R}
{Q∧ B }S1 {R} (Q∧ B)⇒wp(S1,R)
⇐⇒ ∧{Q∧¬B }S2 {R} ⇐⇒ ∧(Q∧¬B)⇒wp(S2,R) 16 of 45
wp Rule: Alternations (3) Exercise Is this program correct?
{x > 0 ∧ y > 0} if x > y then
bigger := x ; smaller := y else
bigger := y ; smaller := x end
{bigger ≥ smaller}
{(x>0∧y>0)∧(x>y)} bigger := x ; smaller := y ∧ {bigger ≥ smaller }
{(x>0∧y>0)∧¬(x>y)} bigger := y ; smaller := x
{bigger ≥ smaller } 17 of 45
wp Rule: Sequential Composition (2)
Recall:
Howdoweprove{Q}S1 ;S2{R}?
19 of 45
{Q}S{R} ≡ Q⇒wp(S,R)
{Q}S1 ;S2{R}⇐⇒Q⇒wp(S1,wp(S2,R))
wp(S1 ; S2,R)
wp Rule: Sequential Composition (1)
wp(S1 ; S2, R) = wp(S1, wp(S2, R)) The wp of a sequential composition is such that the
establishes the wp for the to establish the postcondition R.
18 of 45
first phase
second phase
wp Rule: Sequential Composition (3) Exercise Is{True}tmp := x; x := y; y := tmp{x >y }correct?
IfandonlyifTrue⇒wp(tmp := x ; x := y ; y := tmp,x>y)
wp(tmp := x ; ,x>y) = {wp rule for seq. comp.}
wp(tmp := x,wp(x := y ; ,x>y)) = {wp rule for seq. comp.}
wp(tmp := x, wp(x := y, wp(y := tmp, x > ))) = {wp rule for assignment}
wp(tmp := x, wp(x := y, x > tmp)) = {wp rule for assignment}
wp(tmp := x,y> )
= {wp rule for assignment}
y>x
∵ True ⇒ y > x does not hold in general.
∴ The above program is not correct. 20 of 45
x := y ; y := tmp
y := tmp
y
tmp
Loops
● A loop is a way to compute a certain result by successive approximations.
e.g. computing the maximum value of an array of integers
[ termination ] [ partial correctness ] [ partial correctness ] [ partial correctness ]
● Loops are needed and powerful ● But loops very hard to get right:
21 of 45
○ Infinite loops
○ “off-by-one” error
○ Improper handling of borderline cases ○ Not establishing the desired condition
Correctness of Loops
How do we prove that the following loops are correct?
● In case of C/Java, ¬B denotes the stay condition.
● In case of Eiffel, B denotes the exit condition.
There is native, syntactic support for checking/proving the
total correctness of loops. 23 of 45
{Q} from
Sinit
until
B
loop
Sbody
end
{R}
{Q} Sinit
while(¬ B) {
Sbody
} {R}
Loops: Binary Search
22 of 45
4 implementations for binary search: published, but wrong!
See page 381 in Object Oriented Software Construction
Contracts for Loops: Syntax
from
Sinit
invariant
invariant_tag: I — Boolean expression for partial correctness until
B
loop
Sbody
variant
variant_tag: V — Integer expression for termination end
24 of 45
Contracts for Loops
● Use of loop invariants (LI) and loop variants (LV).
○ Invariants: expressions for partial correctness.
Boolean
● Typicallyaspecialcaseofthepostcondition. e.g., Given postcondition “
”:
”.
LI can be “
● Establishedbeforetheveryfirstiteration. ● MaintainedTRUEaftereachiteration.
○ Variants: expressions for termination
● Denotesthe
● Decreasedattheendofeachsubsequentiteration
Result is maximum of the array
Result is maximum of the part of array scanned so far
Integer
number of iterations remaining
● Maintainednon-negativeattheendofeachiteration.
● AssoonasvalueofLVreacheszero,meaningthatnomoreiterations
remaining, the loop must exit. ● Remember:
total correctness = partial correctness + termination 25 of 45
Contracts for Loops: Runtime Checks (2)
1 2 3 4 5 6 7 8 9
10
11
12
13
14
15
16
17
test
local
i: INTEGER
do from
i := 1 invariant
1 <= i and i <= 6 until
i>5 loop
io.put_string (“iteration ” + i.out + “%N”)
i := i + 1 variant
6-i end
end
L8: Change to 1 <= i and i <= 5 for a Loop Invariant Violation.
L10: Change to i > 0 to bypass the body of loop.
L15: Change to 5 – i for a Loop Variant Violation. 27 of 45
Contracts for Loops: Runtime Checks (1)
26 of 45
V 0 0
not B
Sinit
not I
I
B
Sbody
V < 0
Loop Invariant Violation
Loop Variant Violation
Contracts for Loops: Visualization
28 of 45 Digram Source: page 5 in Loop Invariants: Analysis, Classification, and Examples
Contracts for Loops: Example 1.1
find_max (a: ARRAY [INTEGER]): INTEGER local i: INTEGER
do
from
i := a.lower ; Result := a[i]
until
i > a.upper loop
if a [i] > Result then Result := a [i] end
i := i + 1 variant
loop_variant: a.upper – i + 1 end
ensure
end end
invariant
correct_result: — ∀j a.lower ≤ j ≤ a.upper ● Result ≥ a[j]
across a.lower |..| a.upper as j all Result >= a [j.item]
29 of 45
loop_invariant: — ∀j a.lower ≤ j ≤ i ● Result ≥ a[j]
across a.lower |..| i as j all Result >= a [j.item] end
Contracts for Loops: Example 2.1
find_max (a: ARRAY [INTEGER]): INTEGER local i: INTEGER
do
from
i := a.lower ; Result := a[i]
invariant
until
i > a.upper loop
if a [i] > Result then Result := a [i] end
i := i + 1 variant
loop_variant: a.upper – i end
ensure
end end
correct_result: — ∀j a.lower ≤ j ≤ a.upper ● Result ≥ a[j]
across a.lower |..| a.upper as j all Result >= a [j.item]
31 of 45
loop_invariant: — ∀j a.lower ≤ j < i ● Result ≥ a[j]
across a.lower |..| (i - 1) as j all Result >= a [j.item] end
Contracts for Loops: Example 1.2
Consider the feature call find max( 20, 10, 40, 30 ) , given: ● Loop Invariant: ∀j a.lower ≤ j ≤ i ● Result ≥ a[j]
● LoopVariant:a.upper−i+1
EXIT (i > a.upper)?
× × –
AFTER ITERATION
i
Result
✓ ✓ ×
Loop invariant violation at the end of the 2nd iteration:
∀j a.lower ≤ j ≤ ● ≥ a[j]
evaluates to false ∵ 20 ≥ a[3] = 40 30 of 45
LI
LV
Initialization
1
20
–
1st
2
20
3
2nd
3
20
–
3
20
Contracts for Loops: Example 2.2
Consider the feature call find max( 20, 10, 40, 30 ) , given: ● Loop Invariant: ∀j a.lower ≤ j < i ● Result ≥ a[j]
● LoopVariant:a.upper−i
Result EXIT (i > a.upper)?
AFTER ITERATION
Initialization
i
LI
✓× ✓× ✓× ✓× ✓✓
LV
1
20
–
1st
2nd
2
20
2
3
20
1
3rd
4
40
0
4th
5
40
-1
Loop variant violation at the end of the 2nd iteration
∵ a.upper − i = 4 − 5 evaluates to non-zero. 32 of 45
Contracts for Loops: Example 3.1
find_max (a: ARRAY [INTEGER]): INTEGER local i: INTEGER
do
from
i := a.lower ; Result := a[i]
invariant
until
i > a.upper loop
if a [i] > Result then Result := a [i] end
i := i + 1 variant
loop_variant: a.upper – i + 1 end
ensure
end end
correct_result: — ∀j a.lower ≤ j ≤ a.upper ● Result ≥ a[j]
across a.lower |..| a.upper as j all Result >= a [j.item]
33 of 45
loop_invariant: — ∀j a.lower ≤ j < i ● Result ≥ a[j]
across a.lower |..| (i - 1) as j all Result >= a [j.item] end
Contracts for Loops: Exercise
class DICTIONARY[V, K]
feature {NONE} — Implementations
values: ARRAY[K]
keys: ARRAY[K]
feature — Abstraction Function
model: FUN[K, V] feature — Queries
get_keys(v: V): ITERABLE[K]
local i: INTEGER; ks: LINKED_LIST[K] do
from i := keys.lower ; create ks.make_empty invariant ??
until i > keys.upper
do if values[i] ∼ v then ks.extend(keys[i]) end end
Result := ks.new_cursor
ensure
35 of 45
result valid: ∀k k ∈ Result ● model.item(k) ∼ v
no missing keys: ∀k k ∈ model.domain ● model.item(k) ∼ v ⇒ k ∈ Result end
Contracts for Loops: Example 3.2
Consider the feature call find max( 20, 10, 40, 30 ) , given:
● Loop Invariant: ∀j a.lower ≤ j < i ● Result ≥ a[j]
● LoopVariant:a.upper−i+1
● Postcondition : ∀j a.lower ≤ j ≤ a.upper ● Result ≥ a[j]
LV
–
3
2
1
0
AFTER ITERATION
Result
EXIT (i > a.upper)?
✓× ✓× ✓× ✓× ✓✓
i
LI
Initialization
1
20
1st
2
20
2nd
3
20
3rd
4
40
4th
5
40
34 of 45
Proving Correctness of Loops (1)
{Q} from
Sinit
invariant
I
until
B
loop
Sbody
variant
V
end {R}
○ A loop is partially correct if:
● Given precondition Q, the initialization step Sinit establishes LI I.
● AttheendofSbody,ifnotyettoexit,LIIismaintained.
● IfreadytoexitandLIImaintained,postconditionRisestablished.
○ A loop terminates if:
● Given LI I, and not yet to exit, Sbody maintains LV V as non-negative.
36 of 45 ● Given LI I, and not yet to exit, Sbody decrements LV V.
Proving Correctness of Loops (2)
{Q} from Sinit invariant I until B loop Sbody variant V end {R}
○ A loop is partially correct if:
● Given precondition Q, the initialization step Sinit establishes LI I.
{Q} Sinit {I}
● AttheendofSbody,ifnotyettoexit,LIIismaintained.
{I∧¬B}Sbody {I}
● IfreadytoexitandLIImaintained,postconditionRisestablished.
I∧B⇒R
○ A loop terminates if:
● Given LI I, and not yet to exit, Sbody maintains LV V as non-negative.
{I∧¬B}Sbody {V ≥0}
● Given LI I, and not yet to exit, Sbody decrements LV V.
37 of 45
{I∧¬B}Sbody {V
{ (∀j a.lower ≤j a.upper ⇒ ∀j a.lower ≤ j ≤ a.upper ● Result ≥ a[j]
Proving Correctness of Loops: Exercise (1.1)
Prove that the following program is correct:
find_max (a: ARRAY [INTEGER]): INTEGER local i: INTEGER
do
from
i := a.lower ; Result := a[i]
i > a.upper loop
if a [i] > Result then Result := a [i] end
i := i + 1 variant
loop_variant: a.upper – i + 1 end
ensure
end
invariant
loop_invariant: ∀j a.lower ≤ j < i ● Result ≥ a[j] until
correct_result: ∀j a.lower ≤ j ≤ a.upper ● Result ≥ a[j] end
38 of 45
Proving Correctness of Loops: Exercise (1.3)
Prove that each of the following Hoare Triples is TRUE. 4. Loop Variant Stays Non-Negative Before Exit:
{ (∀j a.lower ≤j a.upper) } if a [i] > Result then Result := a [i] end i := i + 1
{ a.upper−i+1≥0 }
5. Loop Variant Keeps Decrementing before Exit:
{ (∀j a.lower ≤j a.upper) } if a [i] > Result then Result := a [i] end i := i + 1
{ a.upper−i+1<(a.upper−i+1)0 }
where (a.upper − i + 1)0 ≡ a.upper0 − i0 + 1 40 of 45
Proof Tips (1)
{Q} S {R} ⇒ {Q ∧ P} S {R}
In order to prove {Q ∧ P} S {R}, it is sufficient to prove a version
with a weaker precondition: {Q} S {R}.
Proof:
○ Assume: {Q} S {R}
It’s equivalent to assuming: ⇒ wp(S, R) (A1) ○ Toprove:{Q∧P}S{R}
● It’sequivalenttoproving:Q∧P⇒wp(S,R) ● Assume: Q ∧ P, which implies Q
Q
● According to (A1), we have wp(S, R). 41 of 45
Index (1)
Weak vs. Strong Assertions Motivating Examples (1) Motivating Examples (2) Software Correctness Hoare Logic
Hoare Logic and Software Correctness Proof of Hoare Triple using wp
Hoare Logic: A Simple Example Denoting New and Old Values
wp Rule: Assignments (1)
wp Rule: Assignments (2)
wp Rule: Assignments (3) Exercise wp Rule: Assignments (4) Exercise
wp Rule: Alternations (1) 43 of 45
Proof Tips (2)
When calculating wp(S, R), if either program S or postcondition R involves array indexing, then R should be augmented accordingly.
e.g., Before calculating wp(S, a[i] > 0), augment it as wp(S, a.lower ≤ i ≤ a.upper ∧ a[i] > 0)
e.g., Before calculating wp(x := a[i], R), augment it as wp(x := a[i], a.lower ≤ i ≤ a.upper ∧ R)
42 of 45
Index (2)
wp Rule: Alternations (2)
wp Rule: Alternations (3) Exercise
wp Rule: Sequential Composition (1)
wp Rule: Sequential Composition (2)
wp Rule: Sequential Composition (3) Exercise Loops
Loops: Binary Search
Correctness of Loops
Contracts for Loops: Syntax
Contracts for Loops
Contracts for Loops: Runtime Checks (1) Contracts for Loops: Runtime Checks (2) Contracts for Loops: Visualization
Contracts for Loops: Example 1.1
44 of 45
Index (3)
Contracts for Loops: Example 1.2
Contracts for Loops: Example 2.1
Contracts for Loops: Example 2.2
Contracts for Loops: Example 3.1
Contracts for Loops: Example 3.2
Contracts for Loops: Exercise
Proving Correctness of Loops (1)
Proving Correctness of Loops (2)
Proving Correctness of Loops: Exercise (1.1) Proving Correctness of Loops: Exercise (1.2) Proving Correctness of Loops: Exercise (1.3) Proof Tips (1)
Proof Tips (2)
45 of 45