dbc

One of the most useful metaphors for organising software is the one of Design by Contract.

This technique, which was formalised by Bertrand Meyer in 1986 has its roots in previous ideas from Tony Hoare and Barbara Liskov. In a nutshell, DBC equates the relationship of two pieces of software (i.e. two methods) to that of a Client and a Supplier in the business world, both interacting with each other with clear rights and obligations, specified in a Contract.

In DBC, a Supplier can serve a request from a Client only if the latter satisfy the prerequisites or preconditions required by the Supplier. The Supplier has an obligation to return a property as expected by the Client, the post-condition, once the request is served.

Additionally, a contract must specify certain properties that must remain true before and after the nteraction between Client and Supplier. This obligation is known as a class invariant.

Example:

A classic example to show DBC in practice is by building a data structure class, such as a Stack class. The rules of adding items to this structure are very clear:

  • Pre conditions

    • An item must be provided to be added to the stack

    • There must be room in the stack to store the item

  • Post conditions

    • The number of items in the Stack increased by one

    • The item on top of the Stack is the one we just added

  • Class Invariants

    • The  number of items in the Stack  are greater or equal than zero

    • The number of items in the Stack are less or equal to the maximum size allowed

Who checks the contract?

Typically, a method checks the pre-conditions of the contract only. If any of the pre conditions were not enforced by the Client of the method, the Supplier will not continue with the execution of the method since its result (and even its execution) can be unexpected. This is usually done by assertions at the beginning of a method: we assert that a precondition is true prior to executing the method, if the assertion is wrong, then the execution is suspended (an exception is thrown).

Post conditions and Class Invariant could, in theory, be checked in code too. However, this would lead to very long, unreadable and inefficient code. Also, in many cases testing the post-conditions is simply not viable. Remember the DBC metaphor and it will be clear that the party who is responsible for an obligation (the Supplier in this case) cannot be in charge of verifying that the obligation has been fulfilled (i.e. that the post condition is true).

Now, the Client could verify Post-Conditions and Class invariants, but we don’t know (and shouldn’t care) who will be the client of the method we are currently building. And if we are creating a Client of a method, our code requires the Supplier to do what is expected when we invoke its method. So where do we test Post conditions and Class invariants? You know the answer, in the Unit Tests.

Each of the six rules defined above can be converted into a unit test. This is what we’ll do next.

A structure for your tests

But before writing the tests, let me suggest a naming convention for them. I like naming the tests using the following pattern: %MethodName%%ruleType%%Description%

Where rule type is any of the three types of DBC rule: pre condition, post condition or class invariant Here is the list of test we will write for this User Story, based on the previous pattern

[Test]
public void Add_PreCond_ItemIsRequired()
    { throw new NotImplementedException(); }

[Test]
public void Add_PreCond_StackCantBeFull()
    { throw new NotImplementedException(); }

[Test]
public void Add_PreCond_HappyCase()
    { throw new NotImplementedException(); }

[Test]
public void Add_PostCond_CountHasIncreasedByOne()
    { throw new NotImplementedException(); }

[Test]
public void Add_PostCond_ItemIsOnTopOfTheStack()
    { throw new NotImplementedException(); }

[Test]
public void Add_PostCond_InvariantsWereEnforced()
    { throw new NotImplementedException(); }

[Test]
public void CheckInvariants_PostCond_CountIsNonNegative()
    { throw new NotImplementedException(); }

[Test]
public void CheckInvariants_PostCond_CountIsLessThanMaximumAllowed()
    { throw new NotImplementedException(); }

The Happy Case test was not in the list, and there are two tests for a method called Check Invariants. We will look into these tests in detail later. Typically you would put these methods in a class called StackTests. However, if you have a method that requires a large number of tests, you can have one test class per method instead. Your test class would be named Stack_AddTests and the test names would be, for example, PreCond_ItemIsRequired.

Generating Documentation from your Tests

By following this structure for tests and fixtures, we can enrich the documentation generated from our code. This requires customisation of tools like NDoc or Sandcastle. The exact implementation is outside of the scope of this article, but I will post it at some point. The idea is to parse the name of Fixtures and Tests to append pre and post conditions to their relative methods, in a readable way.

One caveat I have with this idea is that you have to remember that you are not using the “true” code for generating the docs, but the names of the apis. This means that your documentation will be as accurate as the name of your tests.