Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] meaning of disjoint and complete behaviors
  • From: siegel at udel.edu (Stephen Siegel)
  • Date: Tue, 9 Apr 2013 23:22:04 -0600
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".