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