程序代写代做代考 Java Program Correctness OOSC2 Chapter 11

Program Correctness OOSC2 Chapter 11
EECS3311 A: Software Design Fall 2019
CHEN-WEI WANG

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
● What’s the weakest assertion?
● What’s the strongest assertion?
[ TRUE ] [ FALSE ]
● In
:
○ A weaker has more acceptable object states
e.g., balance > 0 vs. balance > 100 as an invariant for ACCOUNT
○ A weaker has more acceptable input values
○ A weaker has more acceptable output values 2 of 43
if
Design by Contract
invariant
precondition
postcondition

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 43

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 43

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 :
○ e.g.,{i>3}i := i + 9{i>13}
○ e.g.,{i>5}i := i + 9{i>13}
○ If can be proved TRUE, then the S is correct. e.g.,{i>5}i := i + 9{i>13}canbeprovedTRUE.
○ If cannot be proved TRUE, then the S is incorrect. e.g.,{i>3}i := i + 9{i>13}cannotbeprovedTRUE.
specification
Boolean predicate
{Q} S {R}
{Q} S {R}
{Q} S {R}
5 of 43

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 43
termination
partial correctness
total correctness

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.
○ {true} S {R}
All input values are valid
○ {false} S {R}
All input values are invalid
○ {Q} S {true}
:
7 of 43
All inputs/outputs are valid (No contracts) [ Least informative ]
contract view
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}
[ Most-user friendly ]
[ Most useless for clients ]

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)
○ 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.
8 of 43

Hoare Logic A Simple Example
Given {??}n ∶= n + 9{n > 13}:
●
●
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.
n>4
●
9 of 43

Denoting New and Old Values
In the
to denote its pre-state (old) value.
to denote its post-state (new) value.
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
○ We write
○ We write
postcondition
, for a program variable x:
x0
x
10 of 43

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 43

wp Rule: Assignments (2)
Recall:
{Q}S{R} ≡ Q⇒wp(S,R) Howdoweprove{Q}x := e{R}?
{Q}x := e{R} ⇐⇒ Q⇒ R[x∶=e]
􏰀􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰂􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰁
wp(x := e,R)
12 of 43

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}
x >x0[x ∶=x0 +1]
= {Replacing x x0 + 1 > x0
True
Any precondition is OK.
False is valid but not useful.
13 of 43
by x0 + 1} = {1 > 0 always true}

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).
wp(x := x + 1,x=23)
= {Rule of wp: Assignments}
x =23[x ∶=x0 +1]
= {Replacing x by x0 + 1}
x0 + 1 = 23
= {arithmetic}
x0 = 22
Any precondition weaker than x = 22 is not OK. 14 of 43

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 43

wp Rule: Alternations (2) Recall: {Q} S {R} ≡ Q ⇒ wp(S, R)
How do we prove that {Q} if 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 43
B

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}
17 of 43
⎛ ⎜ ⎝
∧
⎛ ⎜ ⎝
{(x>0∧y>0)∧(x>y)} ⎞ bigger := x ; smaller := y⎟ {bigger ≥ smaller} ⎠
{(x>0∧y>0)∧¬(x>y)} ⎞ bigger := y ; smaller := x⎟ {bigger ≥ smaller} ⎠

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 43
first phase
second phase

wp Rule: Sequential Composition (2)
Recall:
{Q}S{R} ≡ Q⇒wp(S,R) Howdoweprove{Q}S1 ;S2{R}?
{Q}S1 ;S2{R}⇐⇒Q⇒wp(S1,wp(S2,R))
􏰀􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰂􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰃􏰁
wp(S1 ; S2,R)
19 of 43

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 43
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 ● Loops are needed and powerful
● But loops very hard to get right:
21 of 43
○ Infinite loops
○ “off-by-one” error
○ Improper handling of borderline cases ○ Not establishing the desired condition
[ termination ] [ partial correctness ] [ partial correctness ] [ partial correctness ]

Loops: Binary Search
22 of 43
4 implementations for binary search: published, but wrong!
See page 381 in Object Oriented Software Construction

Correctness of Loops
How do we prove that the following loops are correct?
{Q} from
Sinit
until
B
loop
Sbody
end
{R}
{Q} Sinit
while(¬ B) { Sbody
} {R}
● In case of C/Java, denotes the stay condition.
● In case of Eiffel, denotes the exit condition.
There is native, syntactic support for checking/proving the
total correctness of loops. 23 of 43
¬B
B

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 43

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
● Denotes the number of iterations remaining
● Decreasedattheendofeachsubsequentiteration
”:
”.
Result is maximum of the array
Result is maximum of the part of array scanned so far
Integer
● Maintainednon-negativeattheendofeachiteration.
● AssoonasvalueofLVreacheszero,meaningthatnomoreiterations
remaining, the loop must exit. ● Remember:
total correctness = partial correctness + termination
25 of 43

Contracts for Loops: Runtime Checks (1)
26 of 43
V à à
not B
Sinit
not I
I
B
Loop Invariant Violation
Sbody
V < à Loop Variant Violation 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 Contracts for Loops: Runtime Checks (2) 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 43

Contracts for Loops: Visualization
Digram Source: page 5 in Loop Invariants: Analysis, Classification, and Examples 28 of 43

Contracts for Loops: Example 1.1
find_max (a: ARRAY [INTEGER]): INTEGER local i: INTEGER
do
from
i := a.lower ; Result := a[i]
invariant
loop_invariant: — ∀j ∣ a.lower ≤ j ≤ i ● Result ≥ a[j]
across a.lower |..| i as j all Result >= a [j.item] end
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
correct_result: — ∀j ∣ a.lower ≤ j ≤ a.upper ● Result ≥ a[j]
across a.lower |..| a.upper as j all Result >= a [j.item]
end end
29 of 43

Contracts for Loops: Example 1.2
Consider the feature call , given: ● Loop Invariant: ∀j ∣ a.lower ≤ j ≤ i ● Result ≥ a[j]
● LoopVariant:a.upper−i+1
find max( ⟨⟨20, 10, 40, 30⟩⟩ )
AFTER ITERATION
i
Result
LI
EXIT (i > a.upper)?
LV
Initialization
1
20
✓
×
–
1st
2
20
✓
×
3
2nd
3
20
×
–
–
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 43
3
20

Contracts for Loops: Example 2.1
find_max (a: ARRAY [INTEGER]): INTEGER local i: INTEGER
do
from
i := a.lower ; Result := a[i]
invariant
loop_invariant: — ∀j ∣ a.lower ≤ j < i ● Result ≥ a[j] across a.lower |..| (i - 1) as j all Result >= a [j.item] end
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
correct_result: — ∀j ∣ a.lower ≤ j ≤ a.upper ● Result ≥ a[j]
across a.lower |..| a.upper as j all Result >= a [j.item]
end end
31 of 43

Contracts for Loops: Example 2.2
Consider the feature call , given: ● Loop Invariant: ∀j ∣ a.lower ≤ j < i ● Result ≥ a[j] ● Loop Variant: a.upper − i find max( ⟨⟨20, 10, 40, 30⟩⟩ ) AFTER ITERATION i Result LI EXIT (i > a.upper)?
LV
Initialization
1
20
✓
×
–
1st
2
20
✓
×
2
2nd
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 43

Contracts for Loops: Example 3.1
find_max (a: ARRAY [INTEGER]): INTEGER local i: INTEGER
do
from
i := a.lower ; Result := a[i]
invariant
loop_invariant: — ∀j ∣ a.lower ≤ j < i ● Result ≥ a[j] across a.lower |..| (i - 1) as j all Result >= a [j.item] end
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
correct_result: — ∀j ∣ a.lower ≤ j ≤ a.upper ● Result ≥ a[j]
across a.lower |..| a.upper as j all Result >= a [j.item]
end end
33 of 43

Contracts for Loops: Example 3.2
Consider the feature call , 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] find max( ⟨⟨20, 10, 40, 30⟩⟩ ) AFTER ITERATION i Result LI EXIT (i > a.upper)?
LV
Initialization
1
20
✓
×
–
1st
2
20
✓
×
3
2nd
3
20
✓
×
2
3rd
4
40
✓
×
1
4th
5
40
✓
✓
0
34 of 43

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
result valid: ∀k ∣ k ∈ Result ● model.item(k)  v
no missing keys: ∀k ∣ k ∈ model.domain ● model.item(k)  v ⇒ k ∈ Result end
35 of 43

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.
● Given LI I, and not yet to exit, Sbody decrements LV V. 36 of 43

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.
● AttheendofSbody,ifnotyettoexit,LIIismaintained.
● IfreadytoexitandLIImaintained,postconditionRisestablished.
○ A loop terminates if:
● Given LI I, and not yet to exit, Sbody maintains LV V as non-negative.
● Given LI I, and not yet to exit, Sbody decrements LV V.
{Q} Sinit {I}
{I∧¬B}Sbody {I}
I∧B⇒R
37 of 43
{I∧¬B}Sbody {V ≥0}
{I∧¬B}Sbody {V a.upper loop
if a [i] > Result then Result := a [i] end
i := i + 1 variant
loop_variant: a.upper – i + 1 end
ensure
correct_result: ∀j ∣ a.lower ≤ j ≤ a.upper ● Result ≥ a[j] end
end
38 of 43

Proving Correctness of Loops: Exercise (1.2)
Prove that each of the following Hoare Triples is TRUE. 1. Establishment of Loop Invariant:
{ True }
i := a.lower Result := a[i]
{ ∀j ∣a.lower ≤j a.upper) } if a [i] > Result then Result := a [i] end i := i + 1
{ (∀j ∣a.lower ≤j a.upper ⇒ ∀j ∣ a.lower ≤ j ≤ a.upper ● Result ≥ a[j]
39 of 43