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



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).

> /*@ 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

Patrick.

-- 
Patrick Baudin,
CEA, LIST, SOL, 91191 Gif-surYvette cedex, France.
tel: +33 (0)1 6908 2072