What is the best way of determining a loop invariant?

loops invariants formal-methods loop-invariant
filinep picture filinep · May 29, 2010 · Viewed 26.2k times · Source

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?

Answer

Pascal Cuoq picture Pascal Cuoq · Aug 5, 2010

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.

Related questions

Using Loop invariant to prove correctness of merge sort (Initialization , Maintenance , Termination)

How would you go about proving the correctness of merge sort with reasoning over the states of loop invariants?.The only thing that i can visualize is that during the merge step the subarrays(invariants) when combined maintain their states …

Read More
For-each over an array in JavaScript

How can I loop through all the entries in an array using JavaScript? I thought it was something like this: forEach(instance in theArray) Where theArray is my array, but this seems to be incorrect.

Read More
Loop through an array in JavaScript

In Java you can use a for loop to traverse objects in an array as follows: String[] myStringArray = {"Hello", "World"}; for (String s : myStringArray) { // Do something } Can you do the same in JavaScript?

Read More