Understanding how to use post- condition and loop-invariant correctly with Frama-c

Question

I am trying to prove on this example that the return value will be either 0(if 8 is not in array) or 1(if 8 in array).

---

int fi8(int *array, int size) {
  int fi8 = 0;
  int i = 0;
  for(i = 0; i < length; ++i)
  {
     if(array[i] == 8)
     fi8 = 1;
  }
  return fi8;
}

And I created pre- and post conditions:

/*@ requires 0 <= size <= 100;
@  requires  \valid(array+(0..size-1));
@  assigns \nothing;
@  ensures (\forall integer i; 0<= i < size && array[i] != 8)  ==> (\result == 0);
@  ensures (\exists integer i; (0<= i < size && array[i] == 8)) && (\result == 1);
@*/

and loop invariants, because Frama-C is based on Hoare Logic:

/*@ loop invariant 0 <= i <= length;
  @  loop invariant  fi8 == 0 || fi8 == 1;
  @  loop invariant (\forall integer i; 0<= i < size && array[i] != 8)
      ==> (fi8 == 0);
  @  loop invariant (\exists integer i; (0<= i < size && array[i] == 8)) 
      && (fi8 == 1);
  @  loop assigns i, fi8;
  @*/

I'm pretty sure that I'm missing something on the lines, where I'm trying to use forall and exists. I spend hours trying to understand, how can I check correctly, if any value is assigned on array or not, but I feel like I'm stuck here. I really appreciate your help :)

Answer 1

There are a few issues with your code. First, you seem to have mixed size and length. I've taken the liberty to use size everywhere, otherwise this code won't even be accepted by a C compiler, let alone by Frama-C. Second, \forall integer i; 0<= i < size && array[i] != 8 (and the corresponding loop invariant) is incorrect. Literally, it means that any integer i verifies both that i is between 0 and size and array[i] is not 8. Taking 101 for i gives a trivial counter-example to this proposition. What you want to express is that for any integer i, if i is between 0 and size, then array[i] is not 8, which is expressed as \forall integer i; 0<= i < size ==> array[i] != 8. On the other hand, the && connector is correct when used under the \exists: this time we indeed want to find an i such that i is within the bounds of the array and for which array[i]==8. However, the second && in your last ensures is not correct: what you want to say is that if there is such an i, then \result == 1, hence you must have an implication here: (\exists integer i; 0<= i < size && array[i] == 8) ==> (fi8 == 1)

The last issue is with your loop invariants. You are re-using as a quantified variable while it is already a C variable, which is often not a good idea. In fact, it is a real problem, since the property you want to express is that as long as we have not seen an 8 between 0 and i, fi8==0 (and dually that if if have seen an 8, fi8==1), i being the C variable. If you use j in your quantification, as in

 loop invariant (\forall integer j; 0<= j < i ==> array[j] != 8) ==> (fi8 == 0);
 loop invariant (\exists integer j; 0<= j < i && array[j] == 8) ==> (fi8 == 1);

all proof obligations are discharged.