Design by Contract

As I mentioned before, the state of the art in logics of programs isn't yet capable of verifying large-scale programs, even with the best theorem provers currently available.  As a result, the vast majority of programmers don't use any formal methods during software development, and the term "verification and validation" refers mainly to testing.  What many people don't realize is that there is a middle way in using formal methods; it is possible to improve software quality by using limited but effective parts of the theory.

Design by Contract is a method of using assertions in object-oriented programs to specify their behavior.  This importance of this specification is first and foremost methodological.  The mere fact of writing these specifications and having them available in libraries focuses programmer attention to the correct use of program interfaces.  Many errors stem from misunderstandings; a simple but common example is when the writer of a method assumes that a certain parameter may not be null, and omitting to check or handle the case of a null pointer, while the client of the method assumes that the method does something reasonable when given a null value.  The contract defines precisely the responsibilities of the client and supplier; in particular, if the method doesn't handle null pointers, it must declare that fact in its contract.  This contract is a formal part of the interface, and (unlike the source code) must be available to all programmers who use the method.  They, in turn, must look at the contract and behave according to their responsibilities in it.

This simple process of writing the contract for suppliers and consulting it when writing clients can prevent many errors before they are even made.  In order for this to work, the contract doesn't even need to be completely formal, as long as it is precise.  And it has to be simple enough to be easily understood, otherwise it is worthless and may even cause damage.  However, if developers take the trouble of writing formal contracts, they can be rewarded by more than methodological advantages.  Indeed, if contracts are written using a formal notation, it is possible to create tools that give additional benefits.

First, it is possible (though by no means trivial) to write tools that check the contract at runtime.  Many errors are time bombs waiting to happen.  For example, storing a null value in a field of an object may by itself cause no harm.  Only later, when the field is accessed under the assumption that it can't contain null, does the software present an error (in Java, it would be a NullPointerException, nicknamed NPE).  The process of finding where in the program the original null value was assigned can be difficult and time consuming.  A debugger is a useful tool, but it takes skill and time to use it to track such errors, because in many cases the method call that assigned the null value has already completed its execution and is no longer available on the stack to be examined by the debugger.  A tool that checks contracts at runtime would alert the developer to the problem much earlier, thus speeding both discovery and fix of the problem.

Contracts also enable some level of verification.  Instead of having to prove that the program as a whole has some desired properties, the method and class contracts provide "stepping stones" to a (partial) proof of correctness.  If we can prove that all calls in the program satisfy the method of the called method, we will have increased our confidence in the correctness of the program.  Because proving such properties is much easier than proving correctness of a whole program, tools such as theorem provers can be more effective there.  While there aren't yet any commercial tools that do that, there is a lot of research on this topic, and I expect the benefits of automated theorem provers to become practical first in this limited arena.

One of the important advantages of design by contract is that it provides incremental benefits.  Programmers can get immediate benefit from simple contracts, such as those having to do with null pointers.  By adding more details to the contract, they can get more benefit.  It isn't necessary (or even useful) to attempt a full specification in order to use this methodology.

Purists may scoff and say that this is not what logicians mean by verification, and is no better than testing.  I would agree with the first part of this statement, but not with the second.  Contracts are complementary to testing, and both are necessary.  (I will have more to say about this in the future.)  If you insist in full verification, meaning proofs of complete correctness, you will not bring practical value to software development for a very long time.  Design by contract is a practical and useful methodology that should be employed by every software developer.  I will discuss some of the reasons why this is not yet the case in a future post.