Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] proving assigns

2018-05-18 16:46 GMT+02:00 Stephen Siegel <siegel at udel.edu>:

> Thanks, Virgile, for the explanation and fix — it verifies immediately
> with frama-c -wp.
>
> I actually tried something like that but with an extra assertion (see
> below, assertion a7).
> I was never able to prove this assertion, so gave up.
> Just out of curiosity, do you know how to prove it or why it cannot be
> proved?  It clearly follows from the loop invariant; I just want to tell
> some prover “please instantiate that \forall expression with k=i.”
>
> -Steve
>
>
>
> /*@ requires n>=0;
>     requires \valid(a+(0..n-1));
>     assigns a[0 .. n-1];
>     ensures \forall integer k; 0<= k < n ==> a[k] == \at(a[k],Pre);
> */
> void f(int *a, int n) {
>   /*@ loop invariant i1: 0<=i<=n;
>       loop assigns i, a[0 .. n-1];
>       loop invariant \forall integer k; 0<= k < n ==> a[k] ==
> \at(a[k],Pre);
>   */
>   for (int i=0; i<n; i++) {
>     //@ assert a7: a[i]==\at(a[i],Pre);
>     if (a[i]==2) {
>       a[i]=1;
>       a[i]=2;
>     }
>   }
> }
>
>
Well, I have to admit that it was very surprising for me too, but WP is
right: your assertion as it is written is false. You can see where the very
subtle issue lies if you open the formula in the TIP interactive prover
built in WP (see section 2.3 of WP manual): on the GUI, in the 'WP Goals'
tab, double click on the line of the assertion a7 to open a view of the
pending goal. There's a dropdown menu allowing you to select various views
of the goal, but the 'autofocus' one is sufficient: the goal looks like:

>>> Prove: « a at L1[i] »@L4 = « a[0] »@L1.

Where does this 0 comes from? Well, \at(a[i], Pre) evaluates the whole
expression in the pre-state of the function, including i. In all fairness,
WP should have chosen an indeterminate value since i is not even alive in
Pre, instead of giving it its initial value. You can observe this behavior
if you declare i before assigning it 0 in the initialization part of the
for loop. In any case, the assert should in fact be written

   /*@ assert a7: a[i] == \at(a[\at(i,Here)]); */

or, which might be clearer,

    /*@ assert a7: \let i_curr = i; a[i_curr] == \at(a[i_curr],Pre); */

Here, i_curr is a logic (hence immutable) variable, whose value is the
value of i at the moment it is evaluated, regardless of whether it is under
an at or not. This is also what happens in the quantified formulas: k has
the same values regardless of whether it is evaluated at Here or at Pre.

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile
-------------- section suivante --------------
Une pièce jointe HTML a été nettoyée...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20180518/553d27f1/attachment.html>