--- layout: fc_discuss_archives title: Message 9 from Frama-C-discuss on August 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] question about hybrid logic functions



>>  /*@ requires 0 < count_of{Here}(st);
>>   @ assigns st.my_abstraction;
>>   @ ensures  count_of{Here}(st) == count_of{Old}(\old(st)) - 1;
>>   @*/ 
>>
>> in fact, the labels {Here} and {Old} given to count_of are insignificant
>>   
>>     
> Wrong again. It is the \old(st) which is useless: st is not modified by 
> the function so \old(st)==st.
> In the other hand, count_of{Old}(st) is a priori different from 
> count_of{Here}(st) since count_of
>  reads st.my_abstraction and this is said to be assigned.
>   
I can't see is how you can 

 @ assigns st.my_abstraction
and

 @ ensures \old(st)==st

in a same specification ?

Patrick.

-------------- section suivante --------------
Une pi?ce jointe HTML a ?t? enlev?e...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090825/a0466ec5/attachment.htm