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 }

score 6 · Accepted Answer · edited Jun 13 '17 at 01:21

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.

score 3 · Answer 2 · answered Jan 24 '11 at 15:36

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.

Very informal explanation for a formal thing:). Invariants do not hold at start and end, but they should hold after every statement of a program as long as input satisfies the preconditions. Hoare's Logic is based on a simple program schemas, the concrete implementation langauge does not really matter. — Gabriel Ščerbák, Jan 25 '11 at 00:41
Heh, thanks for the comment :) In my education the term 'invariant' was tossed around a lot, without a formal explanation of what it was--I apparently picked up some wrong ideas. — Mark McKenna, Jan 25 '11 at 12:28
I think when it comes to Hoare Logic, the invariant is kind of thrown around without any good explanation... — nunopolonia, Jan 26 '11 at 00:19

score 2 · Answer 3 · answered Jan 24 '11 at 15:35

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.

Hoare Logic Loop Invariant

3 Answers3