Post on 22-Aug-2020
Formale Entwicklung objektorientierter SoftwarePraktikum im Wintersemester 2008/2009
Prof. P. H. SchmittChristian Engel, Benjamin Weiß
Institut fur Theoretische InformatikUniversitat Karlsruhe
07. Januar 2009
Loop Invariants
Formale Entwicklung objektorientierter Software 07. Januar 2009 2 / 15
Unwinding Loops
loopUnwind
Γ ==> U〈π if(e){p; while(e) p} ω〉ψ, ∆
Γ ==> U〈π while(e) p ω〉φ, ∆
How to handle a loop with. . .
0 iterations? Unwind 1×10 iterations? Unwind 11×10000 iterations? Unwind 10001×(and don’t make any plans for the rest of the day)
an unknown number of iterations?
We need an invariant rule (or some other form of induction)
Formale Entwicklung objektorientierter Software 07. Januar 2009 3 / 15
Unwinding Loops
loopUnwindΓ ==> U〈π if(e){p; while(e) p} ω〉ψ, ∆
Γ ==> U〈π while(e) p ω〉φ, ∆
How to handle a loop with. . .
0 iterations? Unwind 1×10 iterations? Unwind 11×10000 iterations? Unwind 10001×(and don’t make any plans for the rest of the day)
an unknown number of iterations?
We need an invariant rule (or some other form of induction)
Formale Entwicklung objektorientierter Software 07. Januar 2009 3 / 15
Unwinding Loops
loopUnwindΓ ==> U〈π if(e){p; while(e) p} ω〉ψ, ∆
Γ ==> U〈π while(e) p ω〉φ, ∆
How to handle a loop with. . .
0 iterations?
Unwind 1×10 iterations? Unwind 11×10000 iterations? Unwind 10001×(and don’t make any plans for the rest of the day)
an unknown number of iterations?
We need an invariant rule (or some other form of induction)
Formale Entwicklung objektorientierter Software 07. Januar 2009 3 / 15
Unwinding Loops
loopUnwindΓ ==> U〈π if(e){p; while(e) p} ω〉ψ, ∆
Γ ==> U〈π while(e) p ω〉φ, ∆
How to handle a loop with. . .
0 iterations? Unwind 1×
10 iterations? Unwind 11×10000 iterations? Unwind 10001×(and don’t make any plans for the rest of the day)
an unknown number of iterations?
We need an invariant rule (or some other form of induction)
Formale Entwicklung objektorientierter Software 07. Januar 2009 3 / 15
Unwinding Loops
loopUnwindΓ ==> U〈π if(e){p; while(e) p} ω〉ψ, ∆
Γ ==> U〈π while(e) p ω〉φ, ∆
How to handle a loop with. . .
0 iterations? Unwind 1×10 iterations?
Unwind 11×10000 iterations? Unwind 10001×(and don’t make any plans for the rest of the day)
an unknown number of iterations?
We need an invariant rule (or some other form of induction)
Formale Entwicklung objektorientierter Software 07. Januar 2009 3 / 15
Unwinding Loops
loopUnwindΓ ==> U〈π if(e){p; while(e) p} ω〉ψ, ∆
Γ ==> U〈π while(e) p ω〉φ, ∆
How to handle a loop with. . .
0 iterations? Unwind 1×10 iterations? Unwind 11×
10000 iterations? Unwind 10001×(and don’t make any plans for the rest of the day)
an unknown number of iterations?
We need an invariant rule (or some other form of induction)
Formale Entwicklung objektorientierter Software 07. Januar 2009 3 / 15
Unwinding Loops
loopUnwindΓ ==> U〈π if(e){p; while(e) p} ω〉ψ, ∆
Γ ==> U〈π while(e) p ω〉φ, ∆
How to handle a loop with. . .
0 iterations? Unwind 1×10 iterations? Unwind 11×10000 iterations?
Unwind 10001×(and don’t make any plans for the rest of the day)
an unknown number of iterations?
We need an invariant rule (or some other form of induction)
Formale Entwicklung objektorientierter Software 07. Januar 2009 3 / 15
Unwinding Loops
loopUnwindΓ ==> U〈π if(e){p; while(e) p} ω〉ψ, ∆
Γ ==> U〈π while(e) p ω〉φ, ∆
How to handle a loop with. . .
0 iterations? Unwind 1×10 iterations? Unwind 11×10000 iterations? Unwind 10001×(and don’t make any plans for the rest of the day)
an unknown number of iterations?
We need an invariant rule (or some other form of induction)
Formale Entwicklung objektorientierter Software 07. Januar 2009 3 / 15
Unwinding Loops
loopUnwindΓ ==> U〈π if(e){p; while(e) p} ω〉ψ, ∆
Γ ==> U〈π while(e) p ω〉φ, ∆
How to handle a loop with. . .
0 iterations? Unwind 1×10 iterations? Unwind 11×10000 iterations? Unwind 10001×(and don’t make any plans for the rest of the day)
an unknown number of iterations?
We need an invariant rule (or some other form of induction)
Formale Entwicklung objektorientierter Software 07. Januar 2009 3 / 15
Unwinding Loops
loopUnwindΓ ==> U〈π if(e){p; while(e) p} ω〉ψ, ∆
Γ ==> U〈π while(e) p ω〉φ, ∆
How to handle a loop with. . .
0 iterations? Unwind 1×10 iterations? Unwind 11×10000 iterations? Unwind 10001×(and don’t make any plans for the rest of the day)
an unknown number of iterations?
We need an invariant rule (or some other form of induction)
Formale Entwicklung objektorientierter Software 07. Januar 2009 3 / 15
An Invariant Rule
Idea behind loop invariants
Find a formula Inv which. . .
holds at the beginning of the loop
is preserved by the loop body
Consequence:
Inv still holds after arbitrarily many loop iterationsIf the loop terminates at all, then Inv holds afterwards
Encode the desired postcondition after the loop into Inv
Basic invariant rule
loopInvariant
Γ ==> UInv , ∆ (initially valid)Inv , e ==> [p]Inv (preserved)Inv ,¬e ==> [π ω]φ (use case)
Γ ==> U [π while(e) p; ω]φ, ∆
Formale Entwicklung objektorientierter Software 07. Januar 2009 4 / 15
An Invariant Rule
Idea behind loop invariants
Find a formula Inv which. . .
holds at the beginning of the loopis preserved by the loop body
Consequence:
Inv still holds after arbitrarily many loop iterationsIf the loop terminates at all, then Inv holds afterwards
Encode the desired postcondition after the loop into Inv
Basic invariant rule
loopInvariant
Γ ==> UInv , ∆ (initially valid)Inv , e ==> [p]Inv (preserved)Inv ,¬e ==> [π ω]φ (use case)
Γ ==> U [π while(e) p; ω]φ, ∆
Formale Entwicklung objektorientierter Software 07. Januar 2009 4 / 15
An Invariant Rule
Idea behind loop invariants
Find a formula Inv which. . .
holds at the beginning of the loopis preserved by the loop body
Consequence:
Inv still holds after arbitrarily many loop iterations
If the loop terminates at all, then Inv holds afterwards
Encode the desired postcondition after the loop into Inv
Basic invariant rule
loopInvariant
Γ ==> UInv , ∆ (initially valid)Inv , e ==> [p]Inv (preserved)Inv ,¬e ==> [π ω]φ (use case)
Γ ==> U [π while(e) p; ω]φ, ∆
Formale Entwicklung objektorientierter Software 07. Januar 2009 4 / 15
An Invariant Rule
Idea behind loop invariants
Find a formula Inv which. . .
holds at the beginning of the loopis preserved by the loop body
Consequence:
Inv still holds after arbitrarily many loop iterationsIf the loop terminates at all, then Inv holds afterwards
Encode the desired postcondition after the loop into Inv
Basic invariant rule
loopInvariant
Γ ==> UInv , ∆ (initially valid)Inv , e ==> [p]Inv (preserved)Inv ,¬e ==> [π ω]φ (use case)
Γ ==> U [π while(e) p; ω]φ, ∆
Formale Entwicklung objektorientierter Software 07. Januar 2009 4 / 15
An Invariant Rule
Idea behind loop invariants
Find a formula Inv which. . .
holds at the beginning of the loopis preserved by the loop body
Consequence:
Inv still holds after arbitrarily many loop iterationsIf the loop terminates at all, then Inv holds afterwards
Encode the desired postcondition after the loop into Inv
Basic invariant rule
loopInvariant
Γ ==> UInv , ∆ (initially valid)Inv , e ==> [p]Inv (preserved)Inv ,¬e ==> [π ω]φ (use case)
Γ ==> U [π while(e) p; ω]φ, ∆
Formale Entwicklung objektorientierter Software 07. Januar 2009 4 / 15
An Invariant Rule
Idea behind loop invariants
Find a formula Inv which. . .
holds at the beginning of the loopis preserved by the loop body
Consequence:
Inv still holds after arbitrarily many loop iterationsIf the loop terminates at all, then Inv holds afterwards
Encode the desired postcondition after the loop into Inv
Basic invariant rule
loopInvariant
Γ ==> UInv , ∆ (initially valid)Inv , e ==> [p]Inv (preserved)Inv ,¬e ==> [π ω]φ (use case)
Γ ==> U [π while(e) p; ω]φ, ∆
Formale Entwicklung objektorientierter Software 07. Januar 2009 4 / 15
An Invariant Rule
Idea behind loop invariants
Find a formula Inv which. . .
holds at the beginning of the loopis preserved by the loop body
Consequence:
Inv still holds after arbitrarily many loop iterationsIf the loop terminates at all, then Inv holds afterwards
Encode the desired postcondition after the loop into Inv
Basic invariant rule
loopInvariant
Γ ==> UInv , ∆ (initially valid)
Inv , e ==> [p]Inv (preserved)Inv ,¬e ==> [π ω]φ (use case)
Γ ==> U [π while(e) p; ω]φ, ∆
Formale Entwicklung objektorientierter Software 07. Januar 2009 4 / 15
An Invariant Rule
Idea behind loop invariants
Find a formula Inv which. . .
holds at the beginning of the loopis preserved by the loop body
Consequence:
Inv still holds after arbitrarily many loop iterationsIf the loop terminates at all, then Inv holds afterwards
Encode the desired postcondition after the loop into Inv
Basic invariant rule
loopInvariant
Γ ==> UInv , ∆ (initially valid)Inv , e ==> [p]Inv (preserved)
Inv ,¬e ==> [π ω]φ (use case)
Γ ==> U [π while(e) p; ω]φ, ∆
Formale Entwicklung objektorientierter Software 07. Januar 2009 4 / 15
An Invariant Rule
Idea behind loop invariants
Find a formula Inv which. . .
holds at the beginning of the loopis preserved by the loop body
Consequence:
Inv still holds after arbitrarily many loop iterationsIf the loop terminates at all, then Inv holds afterwards
Encode the desired postcondition after the loop into Inv
Basic invariant rule
loopInvariant
Γ ==> UInv , ∆ (initially valid)Inv , e ==> [p]Inv (preserved)Inv ,¬e ==> [π ω]φ (use case)
Γ ==> U [π while(e) p; ω]φ, ∆
Formale Entwicklung objektorientierter Software 07. Januar 2009 4 / 15
Example
Precondition: a 6 .= null
& ClassInv
int i = 0;while(i < a.length) {
a[i] = 0;i++;
}
Postcondition: ∀x.(0 ≤ x < a.length→ a[x].= 0)
Loop invariant: 0 ≤ i & i ≤ a.length
& ∀x.(0 ≤ x < i→ a[x].= 0)
& a 6 .= null& ClassInv ′
Formale Entwicklung objektorientierter Software 07. Januar 2009 5 / 15
Example
Precondition: a 6 .= null
& ClassInv
int i = 0;while(i < a.length) {
a[i] = 0;i++;
}
Postcondition: ∀x.(0 ≤ x < a.length→ a[x].= 0)
Loop invariant: 0 ≤ i & i ≤ a.length
& ∀x.(0 ≤ x < i→ a[x].= 0)
& a 6 .= null& ClassInv ′
Formale Entwicklung objektorientierter Software 07. Januar 2009 5 / 15
Example
Precondition: a 6 .= null
& ClassInv
int i = 0;while(i < a.length) {
a[i] = 0;i++;
}
Postcondition: ∀x.(0 ≤ x < a.length→ a[x].= 0)
Loop invariant: 0 ≤ i & i ≤ a.length
& ∀x.(0 ≤ x < i→ a[x].= 0)
& a 6 .= null& ClassInv ′
Formale Entwicklung objektorientierter Software 07. Januar 2009 5 / 15
Example
Precondition: a 6 .= null
& ClassInv
int i = 0;while(i < a.length) {
a[i] = 0;i++;
}
Postcondition: ∀x.(0 ≤ x < a.length→ a[x].= 0)
Loop invariant: 0 ≤ i & i ≤ a.length
& ∀x.(0 ≤ x < i→ a[x].= 0)
& a 6 .= null& ClassInv ′
Formale Entwicklung objektorientierter Software 07. Januar 2009 5 / 15
Example
Precondition: a 6 .= null
& ClassInv
int i = 0;while(i < a.length) {
a[i] = 0;i++;
}
Postcondition: ∀x.(0 ≤ x < a.length→ a[x].= 0)
Loop invariant: 0 ≤ i & i ≤ a.length& ∀x.(0 ≤ x < i→ a[x]
.= 0)
& a 6 .= null& ClassInv ′
Formale Entwicklung objektorientierter Software 07. Januar 2009 5 / 15
Example
Precondition: a 6 .= null
& ClassInv
int i = 0;while(i < a.length) {
a[i] = 0;i++;
}
Postcondition: ∀x.(0 ≤ x < a.length→ a[x].= 0)
Loop invariant: 0 ≤ i & i ≤ a.length& ∀x.(0 ≤ x < i→ a[x]
.= 0)& a 6 .= null
& ClassInv ′
Formale Entwicklung objektorientierter Software 07. Januar 2009 5 / 15
Example
Precondition: a 6 .= null & ClassInv
int i = 0;while(i < a.length) {
a[i] = 0;i++;
}
Postcondition: ∀x.(0 ≤ x < a.length→ a[x].= 0)
Loop invariant: 0 ≤ i & i ≤ a.length& ∀x.(0 ≤ x < i→ a[x]
.= 0)& a 6 .= null& ClassInv ′
Formale Entwicklung objektorientierter Software 07. Januar 2009 5 / 15
Basic Invariant Rule: Problem
Basic invariant rule
loopInvariant
Γ ==> UInv , ∆ (initially valid)Inv , e ==> [p]Inv (preserved)Inv ,¬e ==> [π ω]φ (use case)
Γ ==> U [π while(e) p; ω]φ, ∆
Context Γ, ∆, U must be omitted in 2nd and 3rd premiss
Context contains (parts of) precondition and class invariants
Required context information must be added to loop invariant Inv
Formale Entwicklung objektorientierter Software 07. Januar 2009 6 / 15
Basic Invariant Rule: Problem
Basic invariant rule
loopInvariant
Γ ==> UInv , ∆ (initially valid)Inv , e ==> [p]Inv (preserved)Inv ,¬e ==> [π ω]φ (use case)
Γ ==> U [π while(e) p; ω]φ, ∆
Context Γ, ∆, U must be omitted in 2nd and 3rd premiss
Context contains (parts of) precondition and class invariants
Required context information must be added to loop invariant Inv
Formale Entwicklung objektorientierter Software 07. Januar 2009 6 / 15
Basic Invariant Rule: Problem
Basic invariant rule
loopInvariant
Γ ==> UInv , ∆ (initially valid)Inv , e ==> [p]Inv (preserved)Inv ,¬e ==> [π ω]φ (use case)
Γ ==> U [π while(e) p; ω]φ, ∆
Context Γ, ∆, U must be omitted in 2nd and 3rd premiss
Context contains (parts of) precondition and class invariants
Required context information must be added to loop invariant Inv
Formale Entwicklung objektorientierter Software 07. Januar 2009 6 / 15
Basic Invariant Rule: Problem
Basic invariant rule
loopInvariant
Γ ==> UInv , ∆ (initially valid)Inv , e ==> [p]Inv (preserved)Inv ,¬e ==> [π ω]φ (use case)
Γ ==> U [π while(e) p; ω]φ, ∆
Context Γ, ∆, U must be omitted in 2nd and 3rd premiss
Context contains (parts of) precondition and class invariants
Required context information must be added to loop invariant Inv
Formale Entwicklung objektorientierter Software 07. Januar 2009 6 / 15
Keeping the Context
We would like to keep unmodified parts of the context
assignable clauses for loops can tell what may be modified
//@ assignable i, a[*];
But: determining unaffected formulas syntactically is impossiblebecause of aliasing
Solution: anonymising updates V delete information about modifiedlocations
V = {i := i0 | for x; a[x] := arr0(a, x)}
Formale Entwicklung objektorientierter Software 07. Januar 2009 7 / 15
Keeping the Context
We would like to keep unmodified parts of the context
assignable clauses for loops can tell what may be modified
//@ assignable i, a[*];
But: determining unaffected formulas syntactically is impossiblebecause of aliasing
Solution: anonymising updates V delete information about modifiedlocations
V = {i := i0 | for x; a[x] := arr0(a, x)}
Formale Entwicklung objektorientierter Software 07. Januar 2009 7 / 15
Keeping the Context
We would like to keep unmodified parts of the context
assignable clauses for loops can tell what may be modified
//@ assignable i, a[*];
But: determining unaffected formulas syntactically is impossiblebecause of aliasing
Solution: anonymising updates V delete information about modifiedlocations
V = {i := i0 | for x; a[x] := arr0(a, x)}
Formale Entwicklung objektorientierter Software 07. Januar 2009 7 / 15
Keeping the Context
We would like to keep unmodified parts of the context
assignable clauses for loops can tell what may be modified
//@ assignable i, a[*];
But: determining unaffected formulas syntactically is impossiblebecause of aliasing
Solution: anonymising updates V delete information about modifiedlocations
V = {i := i0 | for x; a[x] := arr0(a, x)}
Formale Entwicklung objektorientierter Software 07. Januar 2009 7 / 15
Improved Invariant Rule
loopInvariant
Γ ==> UInv , ∆ (initially valid)Γ ==> UV(Inv & e→ [p]Inv), ∆ (preserved)Γ ==> UV(Inv & !e→ [π ω]φ), ∆ (use case)
Γ ==> U [π while(e) p; ω]φ, ∆
Context is kept as far as possible
Invariant does not need to talk about unmodified locations
For assignable \everything (the default):
V = {∗ := ∗} wipes out all informationEquivalent to basic invariant ruleAvoid this! Always give a more narrow assignable clause.
Formale Entwicklung objektorientierter Software 07. Januar 2009 8 / 15
Improved Invariant Rule
loopInvariant
Γ ==> UInv , ∆ (initially valid)
Γ ==> UV(Inv & e→ [p]Inv), ∆ (preserved)Γ ==> UV(Inv & !e→ [π ω]φ), ∆ (use case)
Γ ==> U [π while(e) p; ω]φ, ∆
Context is kept as far as possible
Invariant does not need to talk about unmodified locations
For assignable \everything (the default):
V = {∗ := ∗} wipes out all informationEquivalent to basic invariant ruleAvoid this! Always give a more narrow assignable clause.
Formale Entwicklung objektorientierter Software 07. Januar 2009 8 / 15
Improved Invariant Rule
loopInvariant
Γ ==> UInv , ∆ (initially valid)Γ ==> UV(Inv & e→ [p]Inv), ∆ (preserved)
Γ ==> UV(Inv & !e→ [π ω]φ), ∆ (use case)
Γ ==> U [π while(e) p; ω]φ, ∆
Context is kept as far as possible
Invariant does not need to talk about unmodified locations
For assignable \everything (the default):
V = {∗ := ∗} wipes out all informationEquivalent to basic invariant ruleAvoid this! Always give a more narrow assignable clause.
Formale Entwicklung objektorientierter Software 07. Januar 2009 8 / 15
Improved Invariant Rule
loopInvariant
Γ ==> UInv , ∆ (initially valid)Γ ==> UV(Inv & e→ [p]Inv), ∆ (preserved)Γ ==> UV(Inv & !e→ [π ω]φ), ∆ (use case)
Γ ==> U [π while(e) p; ω]φ, ∆
Context is kept as far as possible
Invariant does not need to talk about unmodified locations
For assignable \everything (the default):
V = {∗ := ∗} wipes out all informationEquivalent to basic invariant ruleAvoid this! Always give a more narrow assignable clause.
Formale Entwicklung objektorientierter Software 07. Januar 2009 8 / 15
Improved Invariant Rule
loopInvariant
Γ ==> UInv , ∆ (initially valid)Γ ==> UV(Inv & e→ [p]Inv), ∆ (preserved)Γ ==> UV(Inv & !e→ [π ω]φ), ∆ (use case)
Γ ==> U [π while(e) p; ω]φ, ∆
Context is kept as far as possible
Invariant does not need to talk about unmodified locations
For assignable \everything (the default):
V = {∗ := ∗} wipes out all informationEquivalent to basic invariant ruleAvoid this! Always give a more narrow assignable clause.
Formale Entwicklung objektorientierter Software 07. Januar 2009 8 / 15
Improved Invariant Rule
loopInvariant
Γ ==> UInv , ∆ (initially valid)Γ ==> UV(Inv & e→ [p]Inv), ∆ (preserved)Γ ==> UV(Inv & !e→ [π ω]φ), ∆ (use case)
Γ ==> U [π while(e) p; ω]φ, ∆
Context is kept as far as possible
Invariant does not need to talk about unmodified locations
For assignable \everything (the default):
V = {∗ := ∗} wipes out all informationEquivalent to basic invariant ruleAvoid this! Always give a more narrow assignable clause.
Formale Entwicklung objektorientierter Software 07. Januar 2009 8 / 15
Improved Invariant Rule
loopInvariant
Γ ==> UInv , ∆ (initially valid)Γ ==> UV(Inv & e→ [p]Inv), ∆ (preserved)Γ ==> UV(Inv & !e→ [π ω]φ), ∆ (use case)
Γ ==> U [π while(e) p; ω]φ, ∆
Context is kept as far as possible
Invariant does not need to talk about unmodified locations
For assignable \everything (the default):
V = {∗ := ∗} wipes out all information
Equivalent to basic invariant ruleAvoid this! Always give a more narrow assignable clause.
Formale Entwicklung objektorientierter Software 07. Januar 2009 8 / 15
Improved Invariant Rule
loopInvariant
Γ ==> UInv , ∆ (initially valid)Γ ==> UV(Inv & e→ [p]Inv), ∆ (preserved)Γ ==> UV(Inv & !e→ [π ω]φ), ∆ (use case)
Γ ==> U [π while(e) p; ω]φ, ∆
Context is kept as far as possible
Invariant does not need to talk about unmodified locations
For assignable \everything (the default):
V = {∗ := ∗} wipes out all informationEquivalent to basic invariant rule
Avoid this! Always give a more narrow assignable clause.
Formale Entwicklung objektorientierter Software 07. Januar 2009 8 / 15
Improved Invariant Rule
loopInvariant
Γ ==> UInv , ∆ (initially valid)Γ ==> UV(Inv & e→ [p]Inv), ∆ (preserved)Γ ==> UV(Inv & !e→ [π ω]φ), ∆ (use case)
Γ ==> U [π while(e) p; ω]φ, ∆
Context is kept as far as possible
Invariant does not need to talk about unmodified locations
For assignable \everything (the default):
V = {∗ := ∗} wipes out all informationEquivalent to basic invariant ruleAvoid this! Always give a more narrow assignable clause.
Formale Entwicklung objektorientierter Software 07. Januar 2009 8 / 15
Proving Termination
The invariant rule only proves partial correctness
Solution: Find a decreasing integer term v (called variant)
v ≥ 0 is initially validv ≥ 0 is preserved by the loop bodyv is strictly decreased by the loop body
int i = 0;while(i < a.length) {
a[i] = 0;i++;
}
v = a.length-i
- Add v ≥ 0 to Inv- Add v < vold to right of “preserved” case
- Replace box with diamond
Formale Entwicklung objektorientierter Software 07. Januar 2009 9 / 15
Proving Termination
The invariant rule only proves partial correctness
Solution: Find a decreasing integer term v (called variant)
v ≥ 0 is initially validv ≥ 0 is preserved by the loop bodyv is strictly decreased by the loop body
int i = 0;while(i < a.length) {
a[i] = 0;i++;
}
v = a.length-i
- Add v ≥ 0 to Inv- Add v < vold to right of “preserved” case
- Replace box with diamond
Formale Entwicklung objektorientierter Software 07. Januar 2009 9 / 15
Proving Termination
The invariant rule only proves partial correctness
Solution: Find a decreasing integer term v (called variant)
v ≥ 0 is initially valid
v ≥ 0 is preserved by the loop bodyv is strictly decreased by the loop body
int i = 0;while(i < a.length) {
a[i] = 0;i++;
}
v = a.length-i
- Add v ≥ 0 to Inv- Add v < vold to right of “preserved” case
- Replace box with diamond
Formale Entwicklung objektorientierter Software 07. Januar 2009 9 / 15
Proving Termination
The invariant rule only proves partial correctness
Solution: Find a decreasing integer term v (called variant)
v ≥ 0 is initially validv ≥ 0 is preserved by the loop body
v is strictly decreased by the loop body
int i = 0;while(i < a.length) {
a[i] = 0;i++;
}
v = a.length-i
- Add v ≥ 0 to Inv- Add v < vold to right of “preserved” case
- Replace box with diamond
Formale Entwicklung objektorientierter Software 07. Januar 2009 9 / 15
Proving Termination
The invariant rule only proves partial correctness
Solution: Find a decreasing integer term v (called variant)
v ≥ 0 is initially validv ≥ 0 is preserved by the loop bodyv is strictly decreased by the loop body
int i = 0;while(i < a.length) {
a[i] = 0;i++;
}
v = a.length-i
- Add v ≥ 0 to Inv- Add v < vold to right of “preserved” case
- Replace box with diamond
Formale Entwicklung objektorientierter Software 07. Januar 2009 9 / 15
Proving Termination
The invariant rule only proves partial correctness
Solution: Find a decreasing integer term v (called variant)
v ≥ 0 is initially validv ≥ 0 is preserved by the loop bodyv is strictly decreased by the loop body
int i = 0;while(i < a.length) {
a[i] = 0;i++;
}
v = a.length-i
- Add v ≥ 0 to Inv- Add v < vold to right of “preserved” case
- Replace box with diamond
Formale Entwicklung objektorientierter Software 07. Januar 2009 9 / 15
Proving Termination
The invariant rule only proves partial correctness
Solution: Find a decreasing integer term v (called variant)
v ≥ 0 is initially validv ≥ 0 is preserved by the loop bodyv is strictly decreased by the loop body
int i = 0;while(i < a.length) {
a[i] = 0;i++;
}
v = a.length-i
- Add v ≥ 0 to Inv- Add v < vold to right of “preserved” case
- Replace box with diamond
Formale Entwicklung objektorientierter Software 07. Januar 2009 9 / 15
Proving Termination
The invariant rule only proves partial correctness
Solution: Find a decreasing integer term v (called variant)
v ≥ 0 is initially validv ≥ 0 is preserved by the loop bodyv is strictly decreased by the loop body
int i = 0;while(i < a.length) {
a[i] = 0;i++;
}
v = a.length-i
- Add v ≥ 0 to Inv
- Add v < vold to right of “preserved” case
- Replace box with diamond
Formale Entwicklung objektorientierter Software 07. Januar 2009 9 / 15
Proving Termination
The invariant rule only proves partial correctness
Solution: Find a decreasing integer term v (called variant)
v ≥ 0 is initially validv ≥ 0 is preserved by the loop bodyv is strictly decreased by the loop body
int i = 0;while(i < a.length) {
a[i] = 0;i++;
}
v = a.length-i
- Add v ≥ 0 to Inv- Add v < vold to right of “preserved” case
- Replace box with diamond
Formale Entwicklung objektorientierter Software 07. Januar 2009 9 / 15
Proving Termination
The invariant rule only proves partial correctness
Solution: Find a decreasing integer term v (called variant)
v ≥ 0 is initially validv ≥ 0 is preserved by the loop bodyv is strictly decreased by the loop body
int i = 0;while(i < a.length) {
a[i] = 0;i++;
}
v = a.length-i
- Add v ≥ 0 to Inv- Add v < vold to right of “preserved” case
- Replace box with diamond
Formale Entwicklung objektorientierter Software 07. Januar 2009 9 / 15
Further Complications
Since Java is a real language. . .
the loop guard expression e may have side effects
both e and the loop body may throw an exception
the loop body may use break or continue
The invariant rule in KeY takes all this into account.
Formale Entwicklung objektorientierter Software 07. Januar 2009 10 / 15
Further Complications
Since Java is a real language. . .
the loop guard expression e may have side effects
both e and the loop body may throw an exception
the loop body may use break or continue
The invariant rule in KeY takes all this into account.
Formale Entwicklung objektorientierter Software 07. Januar 2009 10 / 15
Further Complications
Since Java is a real language. . .
the loop guard expression e may have side effects
both e and the loop body may throw an exception
the loop body may use break or continue
The invariant rule in KeY takes all this into account.
Formale Entwicklung objektorientierter Software 07. Januar 2009 10 / 15
Further Complications
Since Java is a real language. . .
the loop guard expression e may have side effects
both e and the loop body may throw an exception
the loop body may use break or continue
The invariant rule in KeY takes all this into account.
Formale Entwicklung objektorientierter Software 07. Januar 2009 10 / 15
Loop Specifications in JML
int i = 0;/*@@@@@@*/
while(i < a.length) {a[i] = 0;i++;
}
Formale Entwicklung objektorientierter Software 07. Januar 2009 11 / 15
Loop Specifications in JML
int i = 0;/*@ loop_invariant
@ 0<= i && i<=a.length@ && (\forall int x; 0<=x && x<a.length; a[x]==0);@@@*/
while(i < a.length) {a[i] = 0;i++;
}
Formale Entwicklung objektorientierter Software 07. Januar 2009 11 / 15
Loop Specifications in JML
int i = 0;/*@ loop_invariant
@ 0<= i && i<=a.length@ && (\forall int x; 0<=x && x<a.length; a[x]==0);@ assignable i, a[*];@@*/
while(i < a.length) {a[i] = 0;i++;
}
Formale Entwicklung objektorientierter Software 07. Januar 2009 11 / 15
Loop Specifications in JML
int i = 0;/*@ loop_invariant
@ 0<= i && i<=a.length@ && (\forall int x; 0<=x && x<a.length; a[x]==0);@ assignable i, a[*];@ decreases a.length-i;@*/
while(i < a.length) {a[i] = 0;i++;
}
Formale Entwicklung objektorientierter Software 07. Januar 2009 11 / 15
Using Method Contracts
Formale Entwicklung objektorientierter Software 07. Januar 2009 12 / 15
Expanding Method Bodies
methodBodyExpand
Γ ==> U〈π method-frame(C,o){b} ω〉φ, ∆
Γ ==> U〈π o.m(p1, ..., pn)@C; ω〉φ, ∆
Disadvantages:
Non-modular
Duplication of effort
Can lead to huge proofs
Sometimes the method body is not available (e.g. native methods)
Formale Entwicklung objektorientierter Software 07. Januar 2009 13 / 15
Expanding Method Bodies
methodBodyExpandΓ ==> U〈π method-frame(C,o){b} ω〉φ, ∆Γ ==> U〈π o.m(p1, ..., pn)@C; ω〉φ, ∆
Disadvantages:
Non-modular
Duplication of effort
Can lead to huge proofs
Sometimes the method body is not available (e.g. native methods)
Formale Entwicklung objektorientierter Software 07. Januar 2009 13 / 15
Expanding Method Bodies
methodBodyExpandΓ ==> U〈π method-frame(C,o){b} ω〉φ, ∆Γ ==> U〈π o.m(p1, ..., pn)@C; ω〉φ, ∆
Disadvantages:
Non-modular
Duplication of effort
Can lead to huge proofs
Sometimes the method body is not available (e.g. native methods)
Formale Entwicklung objektorientierter Software 07. Januar 2009 13 / 15
Expanding Method Bodies
methodBodyExpandΓ ==> U〈π method-frame(C,o){b} ω〉φ, ∆Γ ==> U〈π o.m(p1, ..., pn)@C; ω〉φ, ∆
Disadvantages:
Non-modular
Duplication of effort
Can lead to huge proofs
Sometimes the method body is not available (e.g. native methods)
Formale Entwicklung objektorientierter Software 07. Januar 2009 13 / 15
Expanding Method Bodies
methodBodyExpandΓ ==> U〈π method-frame(C,o){b} ω〉φ, ∆Γ ==> U〈π o.m(p1, ..., pn)@C; ω〉φ, ∆
Disadvantages:
Non-modular
Duplication of effort
Can lead to huge proofs
Sometimes the method body is not available (e.g. native methods)
Formale Entwicklung objektorientierter Software 07. Januar 2009 13 / 15
Expanding Method Bodies
methodBodyExpandΓ ==> U〈π method-frame(C,o){b} ω〉φ, ∆Γ ==> U〈π o.m(p1, ..., pn)@C; ω〉φ, ∆
Disadvantages:
Non-modular
Duplication of effort
Can lead to huge proofs
Sometimes the method body is not available (e.g. native methods)
Formale Entwicklung objektorientierter Software 07. Januar 2009 13 / 15
Use Method Contract Rule
Given a contract (Pre, Post , V):
Γ ==> UPre, ∆ (Pre)Γ ==> UV(exc .= null ∧ Post → 〈π ω〉φ), ∆ (Post)Γ ==> UV(exc 6 .= null ∧ Post → 〈π throw exc; ω〉φ), ∆ (Exc.)
Γ ==> U〈π o.m(p1, ..., pn)@C; ω〉φ, ∆
Formale Entwicklung objektorientierter Software 07. Januar 2009 14 / 15
Use Method Contract Rule
Given a contract (Pre, Post , V):
Γ ==> UPre, ∆ (Pre)Γ ==> UV(exc .= null ∧ Post → 〈π ω〉φ), ∆ (Post)Γ ==> UV(exc 6 .= null ∧ Post → 〈π throw exc; ω〉φ), ∆ (Exc.)
Γ ==> U〈π o.m(p1, ..., pn)@C; ω〉φ, ∆
Formale Entwicklung objektorientierter Software 07. Januar 2009 14 / 15
Use Method Contract Rule
Given a contract (Pre, Post , V):
Γ ==> UPre, ∆ (Pre)
Γ ==> UV(exc .= null ∧ Post → 〈π ω〉φ), ∆ (Post)Γ ==> UV(exc 6 .= null ∧ Post → 〈π throw exc; ω〉φ), ∆ (Exc.)
Γ ==> U〈π o.m(p1, ..., pn)@C; ω〉φ, ∆
Formale Entwicklung objektorientierter Software 07. Januar 2009 14 / 15
Use Method Contract Rule
Given a contract (Pre, Post , V):
Γ ==> UPre, ∆ (Pre)Γ ==> UV(exc .= null ∧ Post → 〈π ω〉φ), ∆ (Post)
Γ ==> UV(exc 6 .= null ∧ Post → 〈π throw exc; ω〉φ), ∆ (Exc.)
Γ ==> U〈π o.m(p1, ..., pn)@C; ω〉φ, ∆
Formale Entwicklung objektorientierter Software 07. Januar 2009 14 / 15
Use Method Contract Rule
Given a contract (Pre, Post , V):
Γ ==> UPre, ∆ (Pre)Γ ==> UV(exc .= null ∧ Post → 〈π ω〉φ), ∆ (Post)Γ ==> UV(exc 6 .= null ∧ Post → 〈π throw exc; ω〉φ), ∆ (Exc.)
Γ ==> U〈π o.m(p1, ..., pn)@C; ω〉φ, ∆
Formale Entwicklung objektorientierter Software 07. Januar 2009 14 / 15
THE
END
Formale Entwicklung objektorientierter Software 07. Januar 2009 15 / 15
THEEND
Formale Entwicklung objektorientierter Software 07. Januar 2009 15 / 15