--- layout: fc_discuss_archives title: Message 23 from Frama-C-discuss on April 2013 ---
Hello Stephen, 2013/4/10 Stephen Siegel <siegel at udel.edu>: > 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". This is correct (for disjoint behaviors, the corresponding formula would be 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? Indeed, complete and disjoint clauses do not really say anything about the implementation. Rather, you can see them as a check on the contract itself. > 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)? As said above, verification of complete and disjoint clauses are independent from any implementation, so you can't have a contract that is proved with the clause, and isn't without it. What could happen (although I don't think that it is the case currently) is that a plug-in could try to take advantage of these clauses to prove other parts of the specification (e.g. value analysis with a suitable slevel could split the analysis with respect to the behaviors of a complete clause), but if it doesn't succeed in proving the clause itself , the contract as a whole won't be considered valid. Best regards, -- E tutto per oggi, a la prossima volta Virgile