Verified Design-by-Contract is
DesignByContract with mathematical verification that all the contracts are always honored. In other words, instead of
PreConditions and
PostConditions being checked at
RunTime, the program is analyzed and
ProofOfCorrectness are developed to show that the pre-conditions hold whenever a method is called and the post-conditions always hold when a method returns. The proofs can be developed by hand (tedious, but often unavoidable) or by an
AutomatedTheoremProving system. Additionally,
ProofAssistant's make it possible to develop proofs manually while filling in the most tedious steps using automated methods.
The proofs are also carried out in relation to preconditions of built-in operators. For example, in the expression A/B it is a precondition that B is not zero, and in the expression A[B] it is a precondition that B is within the bounds of A.
Using verified design-by-contract with standard
ProgrammingLanguages is difficult because these languages are not designed for precise
StaticAnalysis. Even
EiffelLanguage (which has pre- and post-conditions as part of the language) allows
NullValues by default, which is a problem (see
NullConsideredHarmful). However, the ESC/Java tool goes a long way to supporting VDBC using annotated Java.
Verified design-by-contract is much more practical using a language designed for precise static analysis (such as
PerfectDeveloper) or a subset of a standard programming language (such as
SparkAda, or the C subset supported by Escher C Verifier). -
DavidCrocker
See
StaticAssert,
DependentTyping,
ProofOptimizer
CategoryFormalMethods