--- layout: fc_discuss_archives title: Message 7 from Frama-C-discuss on August 2009 ---
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