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.