Hoare Logic Loop Invariant

Question

I'm looking at Hoare Logic and I'm having problems understanding the method of finding the loop invariant.

Can someone explain the method used to calculate the loop invariant?

And what should a loop invariant should contain to be a "useful" one?

I'm only dealing with simple examples, finding invariants and proving partial and complete correction in examples like:

{ i ≥ 0 } while i > 0 do i := i−1 { i = 0 }

Answer 1

If we are talking about Hoare's Logic for proving (partial) correctness of programs, then you use the precondition and postcondition, decompose the program and use the rules of Hoare's Logic inference system to create and prove an inductive formula.

In your example, you want decompose the program using the rule

{p} while b do S {p^not(b)} <=> {p^b} S {p}

In your case

• p: i ≥ 0
• b: i > 0
• S: i := i−1.

So in next step we infer {i ≥ 0 ^ i > 0} i := i−1 {i ≥ 0}. This can be further inferred and proven quite easily. I hope this helps.

Answer 2

I'm not sure if this will answer your question, but just in case it does:

• A "loop invariant" informally is a statement of fact that remains true before and after an iteration of a loop. It essentially defines the consistency constraint of the program with respect to that loop.
• I don't know enough about Hoare Logic to tell you precisely how a loop invariant would be 'calculated', but I suspect such a thing would depend on the language of the code being analyzed moreso than on the formal proof language itself. Do you have a formal algorithmic description that you're working with? I might be able to go further with a bit more background.
• A useful loop invariant would describe something specific about the state of an application. For example if you were writing Insertion Sort, a useful loop invariant for the main element motion loop would essentially state that the (sub)list contains the same collection of objects before and after execution of the loop, and perhaps that the elements that were previously in sorted order remain in sorted order.

Answer 3

Being useful (for your reasoning) is the main point of the invariant. So, look at the post-condition you want to prove and try to make up an invariant that will help you arrive at the post-condition step-by-step and that is derivable from the code of the loop.