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] Assigns clause on multidimensional arrays, assertion before return vs ensure clause

Hello,

On Tue, May 19, 2009 at 17:08, JENN Eric <eric.jenn at fr.thalesgroup.com> wrote:
> EJN-2: Ensure clause vs assertion
> In the following example, the post condition PO is discharged automatically
> whereas the assertion fails. I don't really undestand why.

Because once you have made an assertion, Jessie assumes the assertion
is true and built remaining proofs with this hypothesis.

> int my_var[5];
>
> /*@
> ? requires \valid(my_var);
> ? ensures? \forall integer i; (0 <= i <5) ==> my_var[i] == 0;
> ?@*/
> void main()
> {
> ?int i;
> ?/*@ loop invariant 0 <= i <= 5; @*/
> ?for ( i = 0; i<5; i++) { my_var[i] = 0; }
> ?// The following assertion fails...
> ?/*@ assert \forall integer i; (0 <= k < 5) ==> my_var[k] == 0; @*/

Beware!! You made a typo: k is undefined here (see Frama-C warnings).
You assertion is:
  /*@ assert \forall integer k; (0 <= k < 5) ==> my_var[k] == 0; @*/

> }


[...]
> I guess I am missing some fundamental point here.

Jessie is "opaque to loops". If you want to prove something after a
loop, you need to add necessary proof invariant to build the proof at
each loop step.

Here is your code slightly modified. Beyond the typo in last
assertion, I just added a loop invariant:

int my_var[5];

/*@
  requires \valid(my_var);
  ensures  \forall integer i; (0 <= i <5) ==> my_var[i] == 0;
 @*/
void main()
{
 int i;
 /*@ loop invariant 0 <= i <= 5;
     loop invariant \forall integer k; (0 <= k < i) ==> my_var[k] == 0; @*/
 for ( i = 0; i<5; i++) { my_var[i] = 0; }
 // The following assertion fails...
 /*@ assert \forall integer k; (0 <= k < 5) ==> my_var[k] == 0; @*/
}

All proof obligations are discharged.

Yours,
d.