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



Oops!   I should have seen that.  I believe I could also write it

   a[i]==\at(a,Pre)[i]

Thanks again, Virgile,

Steve

> On May 18, 2018, at 11:44 AM, Virgile Prevosto <virgile.prevosto at m4x.org> wrote:
> 
> 
> 
> 2018-05-18 16:46 GMT+02:00 Stephen Siegel <siegel at udel.edu <mailto: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
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr <mailto:Frama-c-discuss at lists.gforge.inria.fr>
> https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss <https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20180518/23f7beb9/attachment-0001.html>