Issue #38: Design By Contract

Assertions

Colin Powell passed away during the preparation of this article. In one of the most memorable and abhorrent chapters of his career he gave a speech in the United Nations trying to justify the unjustifiable. In that occasion, he said:

My colleagues, every statement I make today is backed up by sources, solid sources. These are not assertions.

Of course, neither the sources were solid, nor the statements were true. But that is another problem.

As a practitioner in the computer field, this author cannot but to feel baffled by this (mis)use of the word “assertion”. Are not assertions, precisely, strong and definite statements? At least dictionaries say so, and in your code, they very much seem so too, to the extent that they will crash your whole program irrevocably should they ever fail. The world of software coopts words (such as exception, static, public) and sometimes gives them a completely different meaning; but in this case I think it was Mr. Powell who chose a more fitting meaning for his case.

The Word

What are assertions to computer programmers, then? According to Bertrand Meyer,

An assertion is an expression involving some entities of the software, and stating a property that these entities may satisfy at certain stages of software execution.

(“Object Oriented Software Construction, Second Edition”, 1997, page 337)

As explained in chapter 11 of Meyer’s book, assertions are meant to check the correctness of a piece of software; that is, its ability to perform the tasks defined in their specification.

Because, you do have a specification, right? Right?

On the other hand, exceptions (a closely related concept to assertions, but not quite the same) are meant check its robustness, that is, its ability to withstand abnormal conditions.

In section B6 of the “K&R” book, Brian Kernighan and Dennis Ritchie explain that

The `assert` macro is used to add diagnostics to programs.

(“The C Programming Language, Second Edition”, 1988, page 253)

Bjarne Stroustrup describes assertions while discussing exception handling in his magnum opus:

A variety of techniques are used to express checks of desired conditions and invariants. When we want to be neutral about the logical reason for the check, we typically use the word assertion, often abbreviated to an assert. An assertion is simply a logical expression that is assumed to be true.

(“The C++ Programming Language, Fourth Edition”, 2013, page 360)

Stroustrup sets a very interesting point about the distinction between compile-time and runtime assertions, to which we will come back shortly before the end of this article.

Steve McConnell gives a similar definition of assertion to Meyer’s in “Code Complete”:

An assertion is code that’s used during development–usually a routine or macro–that allows a program to check itself as it runs.

(“Code Complete, Second Edition”, 2004, page 191-192)

Among the various guidelines McConnell provides for assertions, the following two stand out:

  • Use error-handling code for conditions you expect to occur; use assertions for conditions that should never occur.
  • Use assertions to document and verify preconditions and postconditions. Preconditions and postconditions are part of an approach to program design and development known as “design by contract” (Meyer 1997)

Here we find the connection between assertions and the subject of this month’s issue: assertions can be used to implement “Design by Contract” in software.

The phrase “Design by Contract” means many different things. First of all, it is a trademark, and this author hopes that our use of the phrase in this edition of the magazine will fall under the “Fair Use” clause of copyright law. Henceforth we will refer to it throughout this text using the proper casing defined by said trademark.

Second of all, Design by Contract is actually more than just asserting. But, alas, in many programming languages asserting is a poor man’s approach (sometimes the only one available) to implement a Design by Contract strategy. Some unlucky folks might even have to create their own assertion macro or function from scratch, but hopefully not anymore these days.

The Implementation

Some programming languages provide full Design by Contract features, usually provided through some library or framework: let us mention Python’s deal and PHP’s deal libraries; Rust’s contracts crate; and C++’s Boost.Contract and a proposal from 2017 to integrate it into the language.

Furthermore, Android developers will be happy to learn that Kotlin has Design by Contract baked in since version 1.3 introduced in 2018. The syntax is quite straightforward:

fun String?.isNullOrEmpty(): Boolean {
  contract {
    returns(false) implies (this@isNullOrEmpty != null)
  }
  return this == null || isEmpty()
}

Similarly, the defer keyword in Swift could be used to provide some sort of postcondition contract checking.

The .NET Framework used to have code contracts until recently, but they unfortunately never made it into .NET Core. But Microsoft has bigger problems with open source, anyway.

Finally, in Java one could use AspectJ to “inject” pre- and postcondition checks through join points and annotations.

The Language

The quintessential programming language that brought Design by Contract to the spotlight was Eiffel, created by the aforementioned Bertrand Meyer.

In Eiffel, the implementation of Design by Contract explicitly specifies keywords and placeholders in methods, where the contract verification code must be placed. As an example, this quote from the book (page 349) should suffice:

class STACK2 [G] creation
  make
feature -- Initialization
  make (n: INTEGER} is
    -- Allocate stack for a maximum of n elements
  require
    positive_capacity: n >= 0
  do
    capacity := n
    !! representation.make(I, capacity)
  ensure
    capacity_set: capacity = n
    array_allocated: representation /= Void
    stack_empty: empty
  end

The code above, describing the well-known stack data structure, is quite self-explanatory, even if you have never seen a line of Eiffel before. The require block checks for the preconditions of the code, before the main body of the function (do) runs: we need this check, because even though the STACK2 class constructor takes an INTEGER value, we cannot accept (for obvious reasons) a negative value. Should that ever happen, the runtime would announce a breach of the positive_capacity contract, and loudly so.

Inversely, the ensure block checks for the state of the newly created instance before returning control to the caller. Should the library code fail to create the underlying backing array, in a memory-constrained environment for example, the array_allocated contract would be broken, and the program would halt.

Design by Contract, as implemented in Eiffel and in some of the libraries enumerated above, goes a bit further away: not only are pre- and postconditions checked in methods, but also invariants can be set at class level. These contracts make it evident, at every single moment of the execution of the software, what the state of the component should be. Needless to say, this provides a higher level of correctness verification to software; even if a method fails to check correctly for parameters or state, the class itself is aware of it at any single time.

The Value

The writer of these lines assumes, not without a certain sadness, that most of our readers are not using Eiffel to build their microservice, full-stack, or mobile apps. Whatever the environment or runtime your code runs into, it is impossible to stress enough the importance of (ab)using the provided assertion mechanism by your language in your code.

Doing so will definitely make you more productive; furthermore, many languages allow you to disable those assertions from production builds should you wish to, allowing your code to run faster, but still providing help during writing, debugging, and testing.

Because, after all, those unit tests you cherish so much, they are simply assertions that you run from the outside, usually with a separate executable. Now, imagine sprinkling your code with those same assertions, but inline, all over the place, and having them executed at every step of their way. Such is the underused power of Design by Contract, through a simple mechanism that is freakishly accessible to most of us.

Bertrand Meyer summarized the benefits of Design by Contract in an interview:

How does Design by Contract help a team of developers?

Bertrand: It makes it possible for the various parts of the team to know what their partners are doing without having to know how they are doing it. (…) It is also very good for managers.

(“Masterminds of Programming”, 2009, page 422)

The Future

But is Design by Contract still relevant in the age of pervasive type inference and rewriting in Rust? Should not compilers provide all of these checks? Could not the STACK2 Eiffel class above just use an unsigned int as a parameter for the constructor instead of using a contract?

As powerful as type systems are these days, to answer that question this author yields to Joel Spolsky, who told 20 years ago the story about a seemingly impossible condition in C++ code: a NULL reference and its related crash. Hopefully the debugging of such situation did not take long, but an assert() would have certainly helped. Even though, to be honest, it might have seemed bafflingly useless to most reviewers; after all, the C++ specification explicitely excludes such condition.

Somewhat in this direction, it is worth mentioning Go’s type assertions, or C++’s static_assert mechanism introduced in C++11.

The need for reliable “mass produced software components”, as proposed by Douglas McIlroy in 1968, requires, in the opinion of this author, both static typing and runtime checks. Statically compiled code cannot withstand the ever-changing conditions of all the machines where it might run, simply because, by design, the future cannot be completely foreseen. Design by Contract and assertions were, are, and will continue to be one of our strongest allies in this quest for reuse, composability, and quality.

After all, Mr. McIlroy invented Unix pipes, and his idea of software components was hailed as a potential “silver bullet” by Fred Brooks himself. McIlroy foresaw a thing or two about what the future of software components should be, and our world of ever changing, never API stable, npm install style of components is not it.

Cover photo by Denys Nevozhai on Unsplash.

Donate using Liberapay

Adrian Kosmaczewski is a published writer, a trainer, and a conference speaker, with more than 25 years of experience in the software industry. He holds a Master's degree in Information Technology from the University of Liverpool.