What is the best way of determining a loop invariant?

Question

When using formal aspects to create some code is there a generic method of determining a loop invariant or will it be completely different depending on the problem?

Shontashoo

Answer 1

It has already been pointed out that one same loop can have several invariants, and that Calculability is against you. It doesn't mean that you cannot try.

You are, in fact, looking for an inductive invariant: the word invariant may also be used for a property that is true at each iteration but for which is it not enough to know that it hold at one iteration to deduce that it holds at the next. If I is an inductive invariant, then any consequence of I is an invariant, but may not be an inductive invariant.

You are probably trying to get an inductive invariant to prove a certain property (post-condition) of the loop in some defined circumstances (pre-conditions).

There are two heuristics that work quite well:

• start with what you have (pre-conditions), and weaken until you have an inductive invariant. In order to get an intuition how to weaken, apply one or several forward loop iterations and see what ceases to be true in the formula you have.

• start with what you want (post-conditions) and strengthen until you have an inductive invariant. To get the intuition how to strengthen, apply one or several loop iterations backwards and see what needs to be added so that the post-condition can be deduced.

If you want the computer to help you in your practice, I can recommend the Jessie deductive verification plug-in for C programs of Frama-C. There are others, especially for Java and JML annotations, but I am less familiar with them. Trying out the invariants you think of is much faster than working out if they work on paper. I should point out that verifying that a property is an inductive invariant is also undecidable, but modern automatic provers do great on many simple examples. If you decide to go that route, get as many as you can from the list: Alt-ergo, Simplify, Z3.

With the optional (and slightly difficult to install) library Apron, Jessie can also infer some simple invariants automatically.

Hawley

Well, there it is. The perfect answer. +1 :) Though, have you ever seen Simplify resolve an obligation that Alt-ergo or Z3 failed on? :-) – Nupercaine

@Nupercaine In this article, Simplify is doing well, and in Fig.1 there is an obligation with the property you ask (both Alt-ergo and Z3 fail on it). It all depends on the target program of course :) www-lipn.univ-paris13.fr/~mayero/publis/Calculemus2010.pdf – Hawley

Aha, nice :-) first one I've seen :) – Nupercaine

That makes more sense than what we were taught. The problem I had though was determining if what I have is an invariant, but this takes me one step closer to discovering it – Shontashoo

Would you like to provide some example? or any online best example link that shows calculating loop invariants – Snatch

Answer 2

It's actually trivial to generate loop invariants. true is a good one for instance. It fulfills all three properties you want:

1. It holds before loop entry
2. It holds after each iteration
3. It holds after loop termination

But what you're after is probably the strongest loop invariant. Finding the strongest loop invariant however, is sometimes even an undecidable task. See article Inadequacy of Computable Loop Invariants.

Nupercaine

"True" is weak. I think you mean "you're after the strongest loop invariant". Your answer has raises a good point, but I would say usually one needs "any inductive invariant sufficiently strong to prove the property one has in mind". The strongest loop invariant may not exist (if there is an infinity of variables, adding "and x' = x" for a fresh x to an invariant builds a stronger invariant) and may be unwieldy. – Hawley

Regarding "weakest", you're right, of course. I got it mixed up! (I thought of it as "true is weak since it doesn't imply anything"). Answer updated. Your second point seem slightly artificial to me though. Are you saying it doesn't exist because it would take infinite space to write it down? – Nupercaine

Well, in most logics a formula is a finite assemblage of symbols, and I guess a few meta-theorems would not be true if you allowed infinite assemblages, even limiting yourself to regular assemblages that can be described finitely. So you have to be careful. Leaving this nitpick aside (in ACSL you can state the invariance of infinite variables in a finite clause for instance), my point was that the strongest invariant can be much more complex than necessary. – Hawley

That's a good point. The strongest loop invariant is sometimes more than one needs. Agreed. Technically though, neither the OP nor my answer talks about formulas. You're the one mentioning such representation. ;) – Nupercaine

Maybe an improvement would be to call it an "inductive loop invariant sufficiently strong for proving correctness" (wrt the desired pre- and post- conditions). – Beaton

Answer 3

I don't think it's easy to automate this. From wiki:

Because of the fundamental similarity of loops and recursive programs, proving partial correctness of loops with invariants is very similar to proving correctness of recursive programs via induction. In fact, the loop invariant is often the inductive property one has to prove of a recursive program that is equivalent to a given loop.

Olshausen

Thanks, I don't want to automate it though, its just for pen and paper exercises where I need to find loop invariants. I guess it just takes practice. – Shontashoo

Answer 4

There are a number of heuristics for finding loop invariants. One good book about this is "Programming in the 1990s" by Ed Cohen. It's about how to find a good invariant by manipulating the postcondition by hand. Examples are: replace a constant by a variable, strengthen invariant, ...

Vapor

Answer 5

I've written about writing loop invariants in my blog, see Verifying Loops Part 2. The invariants needed to prove a loop correct typically comprise 2 parts:

1. A generalisation of the state that is intended when the loop terminates.
2. Extra bits needed to ensure that the loop body is well-formed (e.g. array indices in bounds).

(2) is straightforward. To derive (1), start with a predicate expressing the desired state after termination. Chances are it contains a 'forall' or 'exists' over some range of data. Now change the bounds of the 'forall' or 'exists' so that (a) they depend on variables modified by the loop (e.g. loop counters), and (b) so that the invariant is trivially true when the loop is first entered (usually by making the range of the 'forall' or 'exists' empty).

Uranyl