--- layout: fc_discuss_archives title: Message 52 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



*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