a thought about loop variants

[jensgerlach]

Here is a simple function that is verified with Frama-C without problems

/*@
  requires 0 < n;
  assigns  \nothing;
*/
int loop(int n)
{
   int a = 0;
   /*@
     loop invariant 0 <= i <= n;
     loop invariant a == i;
     loop assigns i, a;

     // note these two lines
     loop variant n-i;
     //loop invariant n-i;
   */
   for(int i = 0; i < n; ++i) {
      a += 1;
   }

  return a;
}

If, however, the user accidentally types invariant instead of variant,
then Frama-C does not warn about it.
I don't hink this is a bug, although I think the "loop invariant" n-i looks a bit odd (as an aside the loop "invariant" is not verified (at least with alt-ergo)).

My point is, that it might be nice, if there were a way to warn a user that he did not specify a loop variant. Something along the lines -wp-check-termination.

[vprevosto]

Indeed, the loop invariant is accepted as a short-hand for loop invariant n-i !=0;, which is not true at the end of the last iteration.

My proposal would be to refuse to mix invariant and assigns. This won't help you if don't provide a loop assigns clause;, but this is already a problem in itself.

[jensgerlach]

Yes, that would help although it would be rather indirect. I think an option as mentioned above would be clearer.