--- layout: fc_discuss_archives title: Message 26 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?



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                    |