--- layout: fc_discuss_archives title: Message 29 from Frama-C-discuss on February 2014 ---
Hi, Thanks, but I'm getting syntax error on the line with the //@ ghost declaration. Best regards, Dharma -----Original Message----- From: frama-c-discuss-bounces at lists.gforge.inria.fr [mailto:frama-c-discuss-bounces at lists.gforge.inria.fr] On Behalf Of Claude March? Sent: Thursday, February 13, 2014 5:30 AM To: frama-c-discuss at lists.gforge.inria.fr Subject: Re: [Frama-c-discuss] State-based contracts in ACSL? 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://cp.mcafee.com/d/k-Kr6x0edEICzBddUsOYOrKrjKYyYMM-yCrjKYyYMM-UOrj > KYyYMM-yMrjKYCVtxdVcSwhS7QS0atInlgVJl3LgrdKSbGEsSGxTEdCTPhPVEVIWC_R-sj > 7cczKLsKDuZ-ud7babXDbnhIyyHuWfaxVZicHs3jq9JATvAm4TDNOb2pEVdTdw0PVkDjyb > E07-B2cJVSe08n8ixwCHIcfBisEeRNSeGWnIngBiPta6ToWHFuNt2lbdQEn8lrxrW0E-l9 > QUyW01_FgzbutyrohuudwLQzh0qmNueGWnIngBiPta6BQQg34ZDVsxJfgd45GMD7rjEq89 > gd40w930l96TQPtB2kMkwRYgW -- Claude March? | tel: +33 1 72 92 59 69 INRIA Saclay - ?le-de-France | Universit? Paris-sud, Bat. 650 | http://cp.mcafee.com/d/avndxMA72hJ5AQsFFL3CnCjtPqtTAnC67QkPqtTAnC67T6jqtTAnC67Qm3qtTATbI9L9CQ2eM-CM1jJyWG7dGEtW3pJSNtl3CRkeZ1IS-qevd7dDkT-LPyoVxAtRXBQXTLPNEVphvsVqWdAklrThVkffGhBrwqrjdICXYyMCY-ehojd79KVI04v6neNMQ_aX6NfYdKNRniZyW4GmrFgKgGT2TQ1hYGjFN5Q03_ix6mYX4SMyYYr1vF6y0QJyYtlQLoKxaBCWkdbFEw69XfOV3quwq8blxeeSDgQgiwq810i60GidLFCShdV F-91405 ORSAY Cedex | _______________________________________________ Frama-c-discuss mailing list Frama-c-discuss at lists.gforge.inria.fr http://cp.mcafee.com/d/2DRPoQrhpd7aqrMVBVATsSDtV5VxxZ5cSDtV5VxxZNASDtV5VxxZ5wSDtVdOX2rOpJ0zIfFI0kXoKGxPqG7uwSrtInlgVJl3LgrdLCzDPhPpRd_HYUCeop7tuVteZXYYqemknTemKzp55mZQul3PWApmU6CSjr9K_8I9LfzAm4PhOrKr01DOFeD4ng0fZa4prPIs0gKgB31dnoovaAVgtHzItlQLoKxaBCWkdKNRniZyW4GmrFgKgGT2TQ1hYGjFN5Q03_ix6mYX4SMyYYr1vF6y0QJyYtlQLoKxaBCWkdbFEw69XfOV3quwq8blxeeSDgQgiwq810i60GidLFCQ0w2C8mh