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



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