Smart Objects Put their Contracts in Writing

When you write a function or method that is going to be called from other people’s code, then you would want to let them know how to use it, right? If you are using Java, the typical way of doing that would be to document your method in a JavaDoc comment. As an example, consider the specification for the Arrays.binarySearch method in the Java API. It clearly states that the array that you pass into this method must be sorted in order for the method to work correctly. This is what the method expects from its caller. The documentation goes on to explain what values the method returns under which conditions. This is what the caller can expect from the method. You can think of these mutual expectations as forming a contract between the method (service provider) and the caller (client, service consumer). The service provider basically tells the client: As long as you ensure X before calling my method, I guarantee Y when my method returns. X is known as the precondition, Y as the postcondition.

Clearly specifying such contracts is essential, especially for published interfaces. It allows developers of client code to make sure they use the method correctly, and it tells them what assumptions they can make about the result and/or side effect of the method. When something goes wrong, the contract helps find the cause of the problem. If the precondition was not satisfied, then there must be a bug in the calling code. If the precondition was satisfied, but the postcondition was not, then there must be a bug within the method.

So I guess what I’m saying is that documenting your contracts is important. That’s pretty much common practice, and many people would say it’s a no-brainer. So let’s go a step further. In fact, relying only on documentation to specify contracts has some limitations. First of all, contracts specified in a natural language (such as English) can be ambiguous, and different people may interpret them differently. It’s also easy to forget to update the documentation when changing the code. And a lot of methods do not even get documented in the first place, especially if they are not part of a published interface. But I think that being clear about contracts is also important among internal classes and non-published interfaces. Finally, the biggest limitation seems to be that adherence to these contracts can only be checked manually. In order to use the contracts for locating a bug, you first need to know that the bug exists. Only after learning about a bug and knowing how to reproduce it, you can step through the code and look for a contract violation.

To overcome these limitations, you need a formal, unambiguous way of specifying contracts, and an automated way of checking them. That’s exactly what the design by contract methodology promises. Bertrand Meyer introduced this concept with his programming language Eiffel back in 1986. Eiffel has built-in support for specifying formal contracts as part of the program code. But what if you can’t use Eiffel? Interestingly, in over 20 years design by contract still hasn’t made its way into most mainstream languages.

For lack of language support, I haven’t used “real” design by contract in a serious project. Instead, I have used regular assertions (using the assert keyword in Java or the corresponding macro in C/C++) to verify my contracts. I have found assertions very helpful in debugging and catching bugs early. But since these assertions are just statements within the method implementation, they cannot really be used to specify contracts, but only to verify them. So I still have to specify the contracts separately in the documentation in order to make them explicit and visible. But this means that the contract is represented twice, violating the DRY principle.

I think that design by contract done right can really help achieve software sustainability. So I’ve been experimenting with some external tools that add support for design by contract to languages like Java, and I will be writing about my experiences with these tools. In evaluating these tools, I’m particularly interested in their support for:

  • Generating documentation from contracts
  • Run-time verification of contracts
  • Static analysis of contracts to generate unit tests or even prove correctness

Stay tuned for some hands-on code examples using design by contract.

Advertisements

One Response to Smart Objects Put their Contracts in Writing

  1. […] Javadoc tags @pre and @post to specify a method’s preconditions and postconditions (see my earlier post for an introduction to these terms). There is also an @invariant tag that can be used on the class […]

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: