An Introduction to Programming by Contract

An Example

Programming by Contract is known under the name of Design by Contract™ first implemented by Eiffel, a programming language introduced by Bertrand Meyer¹.

The main principle of programming by contract is to actually add a program’s specification as expressions in the form of meta-data to certain elements in the source code. Let us take a look at the Rocket class below:

import org.gcontracts.annotations.*

@Invariant({ (started == true && speed > 0) || (started == false && speed == 0) })
class Rocket {
    boolean started = false
    int speed = 0

    @Requires({ !started })
    @Ensures({ started && speed > 0 })
    def start()  {
        speed += 10
        started = true
    }

    @Requires({ started })
    @Ensures({ old -> speed - old.speed > 0 })
    def accelerate()  {
        speed += 10
    }
}

Note that the code above is valid Groovy code. As you might notice, it makes use of the following Java annotations: @Invariant, @Requires and @Ensures. These annotations are currently provided by GContracts in package org.gcontracts.annotations.* to specify class invariants, preconditions and postconditions. To explicitly activate contract injection during compilation, @EnableAssertions has to be applied either at the current package or type.

All annotations have in common that they make use of so-called closure annotations – special annotations which allow Groovy closures as attributes.

The @Invariant annotation in this case states that a Rocket instance is either started and flies with some speed, or is not started and stands still.

The @Requires annotation of method start makes an otherwise implicit assumption explicit: whenever the rocket is started, a call to start will not make any sense. If we call start twice, with GContracts the second method execution would fail with an AssertionError:

def rocket = new Rocket()
rocket.start()
rocket.start()

Assertion failed: 

org.gcontracts.PreconditionViolation: <org.gcontracts.annotations.Requires> Rocket.java.lang.Object start() 

!started
||
|true
false

Notice that the exception message makes use of Groovy’s power assertion messages which provide a human-readable interpretation of the expressions found in the annotation closure.

The @Ensures annotation of method accelerate states, that the new value of property speed must be at least greater than its old value. The old variable is a special variable that can be specified as optional parameter to the @Ensures annotations closure. It resembles a map of instance variables of the current object, before the method has been executed. Another special variable the can be used as parameter is result. Whenever specifying a postcondition on a non-void returning method, result contains the method’s result.

Contracts, contracts, everywhere…

So far we have seen class invariants, preconditions and postconditions and how they can be applied on class or method declarations. But where do all those contracting takes place? As you might have already supposed, a contract in terms of Design by Contract™ is an agreement between the supplier (the programmer, the creator) and the client (the one who makes use of it) of a class.

Let’s take class Rocket and its start method as an example. The class supplier clearly states with the given precondition that a Rocket instance must not be started twice. Without an explicitly defined contract in source code, this assumption is either made implicitly by the class programmer or is explicitly stated in the documentation – barely hold in sync with the actual source code.

As a consequence, using contracts is the opposite of applying the principle of defensive programming². Let’s imagine how method start would look like without contracts but with the same checks (implicitly injected by GContracts during compilation) in the previous example:

 def start()  {
    if (started)  {
        throw new AssertionError("Rocket already started!")
    }
    def oldSpeed = speed 
    speed += 10
    started = true
    if (!(started && speed - oldSpeed > 0)) throw new AssertionError("Rocket not started properly!")
}

compared to

@Requires({ !started })
@Ensures({ started && speed > 0 })
def start()  {
    speed += 10
    started = true
}

Contracts are not a mechanism for input validation – they are a concept for tracking bugs in software artifacts. But if we compare the two code samples above, another benefit of DbC becomes immediately visible: the conditions under which a method will be executed successfully are specified in source code, separated in a distinct meta-data element: the annotations. Therefore, the source of the class does not get polluted with if-else statements, supporting maintainability and readability. In most projects, at least the ones that i’ve participated in, there is no clear programming guideline where to place specification of class invariants, pre- and postconditions. I assume this is due to the lack of knowledge on this topic.

Using the three annotations provided by GContracts, to specify

• class invariants
• preconditions
• postconditions

simply solve this problem by inventing the convention of externalizing assumptions or specifications as program code.

When to use it?

Good question. First of all, let us separate between an application’s domain model and the application framework of choice. We will simply ignore the latter for this discussion.

Whenever you find yourself dealing with more complex business rules in the domain model, GContracts can be used to explicitly specify assumptions about various method calls, or class usage. To be clear: specifying contracts in a data-driven application (give data – store data – read/search data with nearly no business logic) will be overhead. But whenever business logic creeps in and complexity raises there is a good chance that thinking about contracts in at least parts which can be identified as reusable is worth for future extensions and maintainability.

Programming by Contract is a technique which adds significant value to an application’s domain model.

Especially in common project libraries it makes sense to specify contracts to ensure valid usage of API classes throughout the project team and to ensure these contracts are satisfied in future versions. Since class invariants, preconditions and postconditions are inherited like class method, properties etc. it is guaranteed that contracts will be strengthened in sub-classes.

Cool. Where to get this stuff?

You are at the right place. If you want to have a play with GContracts, open the groovyConsole and follow these three steps.

To use GContracts in your Groovy/Java project you might download the binary directly in the download section or by defining a Maven dependency.

In order to enable programming by contract with GContracts for your project, you’ll simply have to put the gcontracts*.jar file into the classpath. Groovy’s compiler will automatically look it up and do the rest during the compilation process.

¹ Object-Oriented Software Construction, 2nd Edition, Bertrand Meyer
² Defensive Programming, Wikipedia (En)