Loop assigns, part 3: On the importance of loop invariants

Context

Last week's post mentioned that it is not possible to prove the following loop assigns with Jessie:

void fill(char* a, char x) {
//@ loop assigns a, \at(a,Pre)[0..(a-\at(a,Pre)-1)];
  for(;*a;a++)
    *a = x;
   return;
}

and in fact this annotation is not provable. An hint to where the issue lies is given by the title of this post: we don't provide enough context on what the loop steps are doing.

Loop invariants

One (perhaps the most) important thing to remember when doing deductive verification is that one has to provide sufficiently strong loop invariant for each loop of the program. Formally, loop invariant is a property which must hold before entering the loop and is preserved by a loop step (i.e. if it holds before a step, it must also hold after the step has been executed). Another way to look at this is to say that the invariant abstracts away what has been done by the first k steps (for an arbitrary k). In this view, the loop invariant is the only thing which is known about the state of the program after an arbitrary number of loop steps, and thus we must provide the right amount of information to be able to prove

1. our property of interest (here loop assigns, which is a special case of invariant)
2. the loop invariant itself (otherwise we just exchange an unprovable goal against another, which is not that useful regarding the correctness of the whole function).

In our case, the missing invariant is simply that a is increasing: if we don't mention that, then for all what Jessie knows a-\at(a,Pre)-1 could well be negative (since a itself has been modified, but we don't say anything about its new value), and thus our assigned interval be empty, whereas it should at least include a-1. Thus a sufficient loop invariant would be:

loop invariant \at(a,Pre) - a <= 0;

and this time, the loop assigns can be discharged on the whole program:

void fill(char* a, char x) {
/*@ loop assigns a, a[(\at(a,Pre)-a)..(-1)];
       loop invariant \at(a,Pre) - a <= 0;
*/
  for(;*a;a++)
    *a = x;
   return;
}

As said in the previous, we are not interested for the moment in safety issues (\i.e." we assume that all pointer accesses are valid for now). We thus instruct Jessie not to generate the proof obligations corresponding to potential run-time errors with a particular -jessie-behavior option:

frama-c -jessie -jessie-behavior default -jessie-atp alt-ergo

Unfortunately alt-ergo is still not able to discharge the proof and neither can Simplify nor z3. It seems like the proof obligation generated by jessie is too complicated for automated theorem provers. However the specification is correct as the attached coq file that discharge all proof obligations generated by

frama-c -jessie -jessie-behavior default -jessie-atp coq

shows.