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



BAUDIN Patrick wrote:
> Just a minor correction
>   
>> //@ logic type abstract_stack;
>>
>> struct stack {
>>   //@ ghost abstract_stack my_abstraction;
>> } st;
>>
>> /*@ axiomatic A {
>>   @    logic integer count_of{L} (Stack s) reads s.my_abstraction;
>>   @*/
>>   
>>     
> The label {L} isn't used into the reads definition of count_of (it's a 
> meaning of a good abstraction).
>
>   
Wrong. To make things clearer, I should have written

  reads \at(s.my_abstraction,L)

but as said in ACSL manual, when there is only one label in the context, 
the \at can omitted.

>> /*@ requires 0 < count_of{Here}(st);
>>   @ assigns st.my_abstraction;
>>   @ ensures  count_of{Here}(st) == count_of{Old}(st) - 1;
>>   @*/
>>   
>>     
> so, the specification shoud be corrected as follow:
>
>  /*@ 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.
> Patrick.
>
>   


-- 
Claude March?                          | tel: +33 1 72 92 59 69           
INRIA Saclay - ?le-de-France           | mobile: +33 6 33 14 57 93 
Parc Orsay Universit?                  | fax: +33 1 74 85 42 29   
4, rue Jacques Monod - B?timent N      | http://www.lri.fr/~marche/
F-91893 ORSAY Cedex                    |