Verified Design-by-Contract is DesignByContract
with mathematical verification that all the contracts are always honored. In other words, instead of PreCondition
s and PostCondition
s 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 ProgrammingLanguage
s 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