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

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 {Va.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]
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