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