--- layout: fc_discuss_archives title: Message 29 from Frama-C-discuss on April 2013 ---
Hello, 2013/4/10 Virgile Prevosto <virgile.prevosto at m4x.org>: >> 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. I would add that nothing prevent you to add those kind of disjoint or completness formula to the contract, but behaviour approach brings improved readability. This is very useful to express real-world specifications (e.g. the various expected functional behaviours and erroneous behaviours of a function). Best regards, david