--- layout: fc_discuss_archives title: Message 22 from Frama-C-discuss on April 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] meaning of disjoint and complete behaviors



I'm confused about the meaning of "complete behaviors" and "disjoint behaviors" in function contracts.  Suppose the contract pre-condition is P and it has two behaviors, b1 and b2, with assumptions A1 and A2 (resp.)  As I understand it, "complete behaviors" means "P ==> A1 || A2".  But the validity of that formula does not depend on the implementation of the function; it depends only on the contract (only on P, A1, and A2).  So what difference does it make to add this clause to the contract?  If it is not valid, is the contract considered erroneous (and is this what Frama-C+Jessie+... checks?).   Is it possible for an implementation to satisfy a contract with this clause, but then fail to satisfy the contract with the clause removed (or vice-versa, satisfy the contract without the clause, but fail to satisfy the contract with the clause)?
Similar questions for "disjoint".