Build

The quest of the full stack code craftsman


Mark Derman

DevOps | Full Stack Coder
Thursday 1 February

Design by contract: Towards continuous correctness

  

Reliability is correctness plus robustness

The pursuit of totally reliable software is the goal of 'Design by Contract'. By reliability we mean correctness and robustness. Robustness deals with a program's ability to deal with \ recover from situations outside of the specification. The art of designing in correctness up front is the subject of this post.

What is software correctness?

There is no such thing as a piece of code (by itself) that is correct. Code can only correct with respect to what the code is meant to be doing, in other words, the software specification.

Software correctness principle

Correctness is the exactness with which software implements its specification.

In other words, when we have a 1-to-1 mapping between concept and code, specification and class, we have correct software. The software does exactly what the specification says it must.

We can use assertions in code to express specification requirements. In writing and using assertions we will discover:

  • We can produce code that is designed to be correct from the outset
  • Developer understanding of the domain is greatly increased
  • Software documentation is aided
  • We hugely empower our test code

Defining correctness

We can define the correctness of a method\property F of a class B to be:

{Precondition} F {Postcondition}

In other words, all executions of F, commencing in a state with Precondition satisfied, will terminate in a state where Postcondition is satisfied. Both Precondition and Postcondition here are assertions.

Assertions

Now that we have a way of expressing the correctness of a class member, we can include the specfication (together with the actual member code), in the software itself. This may seem a bizarre idea to many, the fact that we are going to add to execution code with what amounts to specification checking statements. We do this by using assertions. A typical assertion statement might check that a particular class member or method argument is not NULL for example.

Typically we will activate all assertion checking in our debug, continuous integration and staging builds, but usually not in our release builds, although this depends on a variety of factors.

Preconditions and postconditions

The primary use of assertions is the specification of class methods\routines by using 2 assertions that are associated with the method: a precondition and a postcondition.

The precondition states that which that must hold before the method is called.

The postcondition states that which must hold when the method returns.

A code example...

tba...
tba...

 

B.F() Precondition and postcondition benefits and responsibilities

  Benefits Responsiblities
Client of B.F() From postcondition:

Satisfy precondition:

B.F() (Supplier)

From precondition:
Simpler coding and unit testing due to the agreement that all pre-conditions are met.

Satisfy postcondition:

Redundant checking and defensive programming

Question: Should the class developer of B.F() also check the preconditions in case that have not been met by the client?

Answer: No.

While a wide-spread practice in the developer community, defensive programming (or redundant checking) leads to to some unwanted side-effects, the main one being increased complexity. With an exact definition of responsibility between the client and supplier relationship, there is no ambiguity as to who should be checking each condition. Whether a requirement should be the client or supplier

Assertions express correctness conditions. They are a powerful means to prevent defects of correctness in software.   

Assertions are not...

A way of checking input. Each assertion contract is valid between a Caller and a Supplier. This is in the realm of software-to-software communication, not human-input-to-software, or software-to-outside-api communication.

A way of handling special cases. Assertions have nothing to do with handling, for example, if a == NULL ...do option 1... else  ...do option 2....

Assertions simply express correctness conditions.

Assertion violations

A precondition violation is the discovery of a defect in the Client.

A postcondition violation is the discovery of a defect in the Supplier.

Class invariants 

Preconditions and postconditions describe the contract governing individual class methods. There is also a need to express correctness of a class's properties, that must be adhered to be all methods in a class. This assertion is called the class invariant.

The class invariant is automatically evaluated prior to all preconditions and postconditions on public methods, as well as at the end of any creation methods of a class.

References

Object-Orientated Software Construction, by Bertrand Meyer

 

Build is...

Our full stack developers blog. Tips, comments and the odd expletive about crafting elegant web apps on planet Earth.