--- layout: fc_discuss_archives title: Message 52 from Frama-C-discuss on May 2009 ---
*Dear Virgile and David, Thanks for your helpful explanations. Regards e.* Virgile Prevosto a ?crit : > Hello ?ric, > > Le mar. 19 mai 2009 17:08:58 CEST, > JENN Eric <eric.jenn at fr.thalesgroup.com> a ?crit : > > >> EJN-1: "assigns" clauses >> >> How do you express an assign clause when the variable is a multi-dimensional array ? >> > > Your formulations are all correct. However, the normalization phase > performed by the jessie plugin is not compatible with multi-dimensional > arrays. This is a known bug (bts #32: > http://bts.frama-c.com/view.php?id=32) > *Ok, so I'll slightly adapt the application to use monodimensional arrays.* > >> 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. >> >> 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; @*/ >> } >> > > I assume that you mean \forall integer k; ? Otherwise, the assertion is > ill-formed. *Yes, I do. Unfortunately, I do my experiments on another machine, not connected to the network, so I have to copy things manually, hence the errors. Sorry about that.* > The post-condition is proved because you have the assertion > as hypothesis when trying to prove it (an assertion can be seen as a > logical cut: you have to prove it at the point of program where it > appears, but in exchange, it can be used as an hypothesis for each > subsequent point). If you remove the assertion altogether, the ensures > is not proved anymore. > *Ok. I understand. This also explains the next issue... I actually wrote "when I replace the last assertion", while I actually simply added the other assertions... which then took as granted (as far as I understand) the property expressed by the previous, not proved, assertion.* > Now why isn't that proved in the first place? We are just after a loop, > so the first idea should be 'Is the loop invariant strong enough?' In > fact, the invariant does not speak about my_var, so nothing is known > outside of the loop for my_var. We must add something in the invariant: > loop invariant \forall integer k; 0<=k<i ==> my_var[k] == 0; > seem appropriate. > *Ok.* >> If I replace the last assertion by an explicit verification of each entry of the array: >> >> /*@ assert (my_array[0] == 0) && (my_array[1] == 0) ... (my_array[4] == 0); @*/ >> >> then all corresponding proof obligations are discharged. >> >> If I replace the implies ("==>") by (what I suppose is) its logical equivalent : >> >> /*@ assert \forall integer z; ( z>=5) || (z < 0) || (my_var[z] == 0); @*/ >> >> then again the proof obligation is discharged. >> > > I'm not sure I'm following you. Even after changing my_array into my_var > (and filling the dots), I can't prove the assertions without the > loop invariant above. Did you use some other annotations? > > *Well, as I wrote above, I actually left the first (unproved) assertions... hence the result.* >> EJN-3: On runtime checks >> >> Have you (or anybody else) ever considered generating runtime checks of pre, post and invariants, in the same way it is done with JML? >> > > I haven't heard of anything in this area yet. For a carefully chosen > subset of ACSL this shouldn't be too hard, though. > > Best regards, > -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090519/1c0b0953/attachment-0001.htm -------------- next part -------------- A non-text attachment was scrubbed... Name: eric.jenn.vcf Type: text/x-vcard Size: 199 bytes Desc: not available Url : http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090519/1c0b0953/attachment-0001.vcf