Verified Design By Contract

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