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