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

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