--- layout: fc_discuss_archives title: Message 26 from Frama-C-discuss on February 2014 ---
David, your answer is quite surprising, from someone who is familiar with abstraction/refinement approaches ;-) Obviously, the solution is to introduce a ghost state, something like //@ ghost set<int> already_seen; /*@ assigns already_seen; @ ensures already_seen = union(\old(already_seen),singleton(id)); @ ensures \result <==> mem(id,\old(already_seen)); @*/ bool open(int id); details left as an exercise. - Claude Le 13/02/2014 11:18, David MENTRE a ?crit : > Hello, > > Le 09/02/2014 06:19, Dharmalingam Ganesan a ?crit : >> Bool open(int id); >> >> Informally, f should return true for every new id otherwise returns >> false. > > open(), not f(). > > How open() is implemented? I assume it looks at some global variables > recording the current state. I would refer to this global state in > open()'s contract. > > Best regards, > david > > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss -- Claude March? | tel: +33 1 72 92 59 69 INRIA Saclay - ?le-de-France | Universit? Paris-sud, Bat. 650 | http://www.lri.fr/~marche/ F-91405 ORSAY Cedex |