--- layout: fc_discuss_archives title: Message 29 from Frama-C-discuss on February 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] State-based contracts in ACSL?



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