Design by Contract: Part One

Despite the usefulness of Design by Contract (DbC), support for it is sorely lacking in nearly all mainstream programming languages. It appears as if Ruby and JavaScript are the only mainstream languages for which a reliable and easy-to-use DbC library is available.

However, rolling your own code for preconditions and postconditions is straightforward in any language. Support for invariants is another story, but it’s possible your application can get along without it. Often the intent of an invariant can be enforced through precondition and postcondition checks.

This is a series of three posts on the subject of DbC. Part 1 contains:

• An explanation of Design by Contract
• Clarification of the purpose of DbC — specifically, it’s not a testing tool
• Random opinionated comments

Part 2:

• A quick survey of available DbC libraries for some mainstream programming languages (Java, C#, Ruby, JavaScript, Python, Go)
• A small demonstration of the contracts gem for Ruby
• A small demonstration of the contractual package for JavaScript
• Random opinionated comments

Part 3:

• Step-by-step walkthrough of test-driving hand-rolled support for DbC in Java
• Random opinionated comments

What is Design by Contract?

Created by Bertrand Meyer in the 1980s, Design by Contract (DbC) is an approach to software design that focuses on specifying contracts that define the interactions among components. DbC is one more tool in our toolkit for gaining confidence that our code is correct, alongside other tools such as type systems, executable test cases, static code analysis, and mutation testing.

An underlying assumption is that components interact with one another in a client-server model. A server makes certain promises (also called obligations) to provide benefits to clients, and client components may assume these promises will be kept. The contract also specifies postconditions and invariants, which participating components must honor.

DbC is based on logical building blocks that existed previously. A key underlying concept is the idea of Hoare triples. In 1969, British computer scientist Tony Hoare proposed that we could reason about the correctness of software by considering how the execution of a section of code changes the state of the computation. The basic formulation is:

{P} C {Q}

where P denotes a precondition, C represents the computation, and Q denotes a postcondition. Preconditions and postconditions are expressed as assertions, in the sense of predicate logic (also known as first-order logic). Those are the basic logical building blocks of DbC.

In DbC, the obligations are preconditions, expressed as assertions; the benefits are postconditions, expressed as assertions; and the invariants are aspects of the system state that are guaranteed not to be affected by the computation.

Eiffel Language

It would have been interesting and useful to define a way of specifying contracts as documentation that programmers could use as a guide for building software based on DbC, but Meyer did not stop there. He also developed a programming language that has DbC constructs built in and enforced at compile time. The Eiffel language implements DbC directly.

To see how DbC can help us, let’s take a look at Eiffel first, as it was the original implementation. Here’s a sample Eiffel class from the DbC intro on the Eiffel site:

class DICTIONARY [ELEMENT]
feature
	put (x: ELEMENT; key: STRING) is
			-- Insert x so that it will be retrievable
			-- through key.
		require
			count <= capacity
			not key.empty 
		ensure
			has (x)
			item (key) = x
			count = old count + 1
		end

	... Interface specifications of other features ...

invariant
	0 <= count
	count <= capacity
end	

The require keyword specifies the preconditions for the put routine in a Dictionary. One or more assertions can follow require. In this example, the preconditions are that the number of dictionary entries (count) doesn’t exceed the capacity of the dictionary, and that the client is not attempting to add an entry that has no key.

The ensure keyword specifies the postconditions for the put routine. It promises that after the put operation, the dictionary will contain the element x, that a lookup based on key will retrieve element x, and that the new count will be one greater than the previous count.

The invariant keyword specifies aspects of the system state that must remain unchanged. The scope of invariant is larger than that of require and ensure, because the invariants must hold true no matter what operations are performed. In the example, the invariants are that the number of items in the dictionary (count) must be positive, and the count cannot exceed the dictionary’s capacity.

Not a Testing Technique

In the course of looking for implementations of DbC for languages other than Eiffel, I noticed a common misconception: Many people think of DbC as a testing technique. The difference between testing and checking is usually clearcut, but the situations in which each can occur may be open to interpretation.

DbC is a form of checking, and it is based on assertions. As Michael Bolton and James Bach put it, “An assertion, in the Computer Science sense, is a kind of check. But not all checks are assertions, and even in the case of assertions, there may be code before the assertion which is part of the check, but not part of the assertion.” DbC is consistent with this observation.

There is also confusion about context; some people assume any sort of check, especially those performed via a software tool, must occur during a “testing phase” of product development or delivery. Issues that I’m seeing with the implementations of DbC libraries may stem from this very misconception. Many DbC solutions are designed to be used during development and testing. They involve “extra” and “optional” libraries that can be enabled and disabled at build time or at runtime. At least one that I looked at requires the code to be compiled with debug options turned on so that the object code is instrumented, and the DbC tool can use debugging information. This would not be done when preparing code for production deployment.

But the intent is that preconditions, postconditions, and invariants are asserted in production with the application running live. That’s the whole point. It’s a hedge against invalid arguments or incorrect data structures being passed into application components; against components inadvertently generating unusable or damaging outputs; against applications changing the system state as an unintended side-effect of their operations. The canonical reference implementation, Eiffel, does not separate DbC checks from the rest of the code. That is not the intent.

Why Not Just Write an “If” Statement?

When you look at various DbC libraries, you discover they tend to be complicated wrappers around relatively basic conditional code. One reason DbC hasn’t caught on in a big way may be that people are intimidated by the apparent complexity of the tools. When investigating the value of DbC, developers often ask, Why not just write an “if” statement for that?

They’re right. The issue isn’t that you couldn’t just write an “if” statement. The problem is that most people don’t bother to write “if” statements. Calling it out as a distinct “thing” with its own name might subtly influence developers to pay more attention to it.

The same Michael Bolton mentioned above tells a story of a time when a developer challenged him to break a web application he had written. The developer was very confident that the code was rock-solid. Bolton not only broke the application, but crashed the server, in a matter of seconds. He pasted the full text of a book from Project Gutenberg into the application’s login form.

So, why didn’t that developer just write an “if” statement? It would have saved him considerable trouble and embarrassment. It’s also arguably a fundamental software engineering competency to guard against well-known security risks. Limiting the size of an input value on a form is pretty basic stuff, after all.

A Thing Becomes Real When It has a Name

Now, maybe if there were a “thing” that software developers could name and discuss (like “Design by Contract,” perhaps), then it would be easier for them to remember to take care of this.

With the growing popularity of microservices, a given application may comprise many small services that are developed independently by people who do not work together and who never meet. Sometimes clients look up services from a registry, and they don’t even know which implementation of a service interface they are calling. These applications live in an inherently insecure environment known as the “Internet.” You may have heard of it.

Some of these clients may even be hostile. Indeed, we know some of them are.

DbC offers a way to ensure code contracts are honored in the wild, when software components may be invoked by client code the service developers know nothing about and do not control. It doesn’t automatically protect against all errors or against determined hackers, but it’s a useful defensive tool.

We cannot manage this situation entirely by checking our code before deployment. We have to manage it actively in production. DbC is meant to enforce the contract for interacting with a component, not merely to check it.

Next

In the next instalment, I’ll share my experiences looking for DbC support for Java, C#, Ruby, JavaScript, Python, and Go. In the third and final instalment, we’ll walk through the process of developing DbC support in a couple of mainstream languages.