Existential quantified assertion fails

Question

I am trying to prove quantified assertions for arrays and encountered some problems. Consider the following small program:

int a[4] = {1,2,3,4};

/*@ requires p == a;
    assigns \nothing;
*/
void test(int *p)
{
  p++;
  //@ assert \forall int i; 0 <= i < 3 ==> p[i] < 10;
  //@ assert \exists int i; p[i] == 3;
}

I am using the 'Typed' memory model:

frama-c-gui -wp -wp-qed -wp-byreference -wp-model 'Typed' -main test Test.c

For some reason the "requires" does not hold and thus all assertions can be proved, even 1==2. In order to overcome this I directly assign the global variable in the function body:

int a[4] = {1,2,3,4};

/*@  assigns \nothing;
*/
void test(int *p)
{
  p = a;

  p++;
  //@ assert \forall int i; 0 <= i < 3 ==> p[i] < 10;
  //@ assert \exists int i; p[i] == 3;
}

Here the forall holds but the exists does not. The exists only holds when I add the assertion "p[1] == 3" before it. What is missing to prove such existential array properties? I need this to express a loop invariant for a search loop over array entries.

Thanks, Harald

François Bobot François Bobot · Accepted Answer · 2013-01-09T17:04:44

The "requires" is transformed into false by an incorrect simplification. It will be corrected in the next release. Thank you for spotting the error.

With the fix, the last assertion is still not proved by Alt-ergo because it is not able to find the witness for i using its usual heuristics. When you add the assertion "p[1] == 3" you give the witness, that's why it's easier to prove. Some other provers (Z3, CVC4) will be able to prove this particular assertion directly. Stay tuned for the next release.

Existential quantified assertion fails

1 Answers