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



Small correction: please replace "f" by "open".

-----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 Dharmalingam Ganesan
Sent: Sunday, February 09, 2014 12:19 AM
To: Frama-C public discussion
Subject: [Frama-c-discuss] State-based contracts in ACSL?

Hi,

I have a function 

Bool open(int id);

Informally, f should return true for every new id otherwise returns false.

For example,

open(1) = true; 
open(1) = false;

I read the documentation of ACSL but could not locate anything similar to the above scenario. It seems ghost variables may contribute here(?), but assume we are not allowed to modify the existing definition of f nor we do not have access to any interface to check whether id is already in use .

Any comments?
Dharma

_______________________________________________
Frama-c-discuss mailing list
Frama-c-discuss at lists.gforge.inria.fr
http://cp.mcafee.com/d/avndy0A83hJ5AQsECzBdB4syrKrjKYyYMM-yCrjKYyYMM-UOrjKYyYMM-yMrjKYCVtxdVcSwhS7QS0atInlgVJl3LgrdKSbGEsSGxTEdCQvtKetjvW_8Kcfcf6zDHTbFFzxT9I9LCzBxfBHEShhlLtzBgY-F6lK1FJ4SyrLOb2rPUV5xcQsCXCM0pYGjFN5Q03_ix6mYX704bA9gMjlS67OFek7qUX7ltbSbEiFpKB3rItlQLoKxaBCWkbAaJMJZ0kvaAWsht00_QEhBLeNdIcec6PiSbNRniZyW4GmrFgQKCy0oDI_bAdFW1EwJm4UXqt3h1a1Ew418o2F8SMYr75XFvb1Qw1U