--- layout: fc_discuss_archives title: Message 50 from Frama-C-discuss on May 2009 ---
[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.