Computer Programming/Design by Contract

This page about DbC focuses on Design by Contract more closely than its cousin. The reason is that Eiffel's DbC (and that of very few other languages) provide close integration of complete DbC with all aspects of the respective language, and the respective language's definitions.

Designing by Contract

»Not without my abstract data types.«

First, Design by Contract applies to modules, to the routines in the modules, to loops in subroutines, and between statements. Exceptions are involved, too. That is to say, you cannot have partial contracts. Contracts involve the whole module at every level of refinement.

If you set up a module(!) contract, the contract's clauses apply to an entire module throughout its entire life time. If you use a module that has a contract, you are obliged to obey its visible rules.

There are two views of a module, the client's view, and the supplier's view. When you write a subroutine, and the subroutine calls other subroutines contained in some module, then your subroutine becomes a client of the module. The client sees two parts of the module's contract:

the module's invariants and
the preconditions and the postconditions of the module's subroutines.

The module itself is considered a supplier from the clients point of view, it supplies subroutines. The supplier sees more of the module and adds some internal contract clauses, so to speak. The supplier will have to provide, that is, write

the module's invariants,
the preconditions and the postconditions of the module's subroutines,
loop invariants and loop variants,
check instructions
consistent exception handling

All of these are assertions, or, in the case of exceptions, consistent with assertions.

Check the presence of supporting facilities per language here: w:Design by contract.

Assertions

The purpose of an assertion is twofold: First, it states expected values of (computed) variables and their relations. Second, it facilitates testing that the variables do have the values stated and that the relations are indeed true. Being part of a program, assertions can be used as run-time checks of variables and their relations. But at the same time, assertions allow reasoning about the program before it is run. You use assertions for showing that a module, subroutine, loop, etc. is correct.

Each assertion is a Boolean expression, and is either True or False. Example:

 $s=0$  or else  $g(s)=2*t$

There are two relations in the example involving two variables, some values are computed. The two equality tests are either True or False, and are connected by or else, a Boolean operator.

Taken to the module level, assertions can express requirements that a client must satisfy when calling the module's subroutine. The requirements are stated as preconditions of a subroutine, that is, assertions involving the subroutine's formal arguments and possibly other features of the module. In return, a subroutine's postcondition describes what the subroutine will have to offer as a result. Again, the postcondition is expressed using an assertion involving the subroutine's results and possibly other features of the module. A typical subroutine description, part of the module's contract might look like this:

  pop
        --  remove the topmost item
     require
        has_items: not is_empty
     ensure
        one_less: count = old count - 1

The subroutine pop takes no argument, and it doesn't return anything. However, it modifies the module, a stack. Therefore the pre- and postconditions are assertions that refer to other features of the module, is_empty and count. Useful names are attached to the assertions for reference.

To complete the contract, another assertion is added at the module level, the module invariant. The relations of the module invariant inform the client about the state of the module by saying what is guaranteed between each call of a subroutine of the module. Example:

 invariant
    sensible_count: count >= 0

Contract violations are assertions that evaluate to False. Typically, when the program does not live up to its assertions, an exception is raised, because the program is obviously wrong. The situation is then handled using the exception mechanisms of the language, bridled by the rules that Design by Contract requires.

Extensive program analysis based on assertions can in some cases be performed at compile time. This amounts in a mechanical proof that certain checks are not necessary. The checks can then be omitted from the compiled program. See w:SPARK programming language.

If an assertion is false, there is a bug in the program!

The reason is that the program does not produce the results that it must produce according to the assertions. Here is a list of the possible assertions in Design by Contract (C means visible to clients (outside the module), S means visible to supplier (inside the module)):

Module Invariants (C, S): Module invariants assert what is true after initialisation of the module. They also assert the same truths before and after any execution of one of its subprograms.
Preconditions (C, S): A precondition of a subprogram states what must be true before calling the subprogram. Usually, it expresses relations of (computed) module variables and subprogram parameters. Only if the precondition is true can the subprogram execute in order to fulfil its postcondition.
Postconditions (C, S): Postconditions state what will be true about (computed) variables and relations when the subprogram has finished successfully.
(Loop variants) (S): A loop variant is an expression (of type Natural) whose value decreases towards zero on each iteration of the loop. Typically one of the variables of the loop is used to express this property. The loop variant guarantees termination.
Loop invariants (S): A loop invariant expresses a relation that is true when the loop is entered, or entered once more. The relation will name variables of interest to the loop.
Checks (S): When a statement has executed, it will likely have changed the value of one or more variables by assignment. A check expresses the programmer's expectation of the relation between these variables after the assignment.

Preconditions P and postconditions Q of a subprogram S frame the subprogram in the sense of a Hoare triple:

{at least P} S {guarantees Q},

provided the module invariant is True before and after the call! Notice this last requirement. The module must be in a known good state, because the preconditions and the postconditions may refer to the module's state.

Design by contract is not input checking

By implication, the rule from above about false assertions means that assertions are not to be used as replacements for input validation. When you can't trust your input, use means provided by your language in a conditional, like the 'Valid attribute in Ada. For example, calling Sqrt(x) where x = -1.23 is a bug in using Sqrt, a violation of the contract. The caller has failed to test x before sending it to the math routine.

Assertions can't replace conditionals

Can you pass all kinds of numbers to Sqrt and just prepare to handle the exception raised when the precondition of Sqrt evaluates to false? In other words, can you deliberately ignore the contract? The answer is no, for at least two reasons.

If a module has been shown to be correct, assertion checking might have been turned off for this module, expecting that clients will fulfil their part of the contract. A contract violation by the caller could then go unnoticed and might produce a vastly erroneous computation.
If the called subprogram is not Sqrt but controls the speed of a train, you can't just pass invalid input until it doesn't happen to make the speed-control subprogram fail with an exception. Worse, see 1.

Example: A Stack

(This example is given in very minimal Ada notation, knowing that language support for DbC is pretty good, in particular in Ada 2005, but limited. Imagining require, ensure, and invariant in place of the comments marked pre, post, and inv will render the following closer to the Eiffel original. Use the facilities that your language provides for expressing assertions and exception handling.)

The exclamation points (`!') below are only a notational device. They stand for the facilities available with the respective languages. Their meaning is only informative of the contract.

generic
   type Item is private;
   --  any definite type that permits assignment

package Stack is

   --  last in first out storage, initially empty

   function is_empty return Boolean;
   --  is there an element on the stack?
   --  ! post: result = (count = 0)

   function count return Natural;
   --  number of items currently on the stack

   function top return Item;
   --  the topmost item
   --  ! pre: not is_empty

   procedure push(x: Item);
   --  add `x` on top of the stack
   --  ! post: count = old count + 1
   --  ! post: not is_empty
   --  ! post: top = x

   procedure pop;
   --  remove the topmost item
   --  ! pre: not is_empty
   --  ! post: count = old count - 1


   --  ! inv: count >= 0
   --  ! inv: (count = 0) = is_empty

end Stack;

Notice that up to this point, there is no executable statement in the module. It's just a package specification with contractual pre- and postconditions, and a module invariant. Yet the module's contract is complete as far as clients of this module are concerned.

The function top states as precondition that there must be an element on the stack, otherwise it cannot succeed. To express this, it refers to another function of the same module, is_empty. Note that the module invariant does allow an empty stack. The function count has neither precondition nor postcondition, but is mentioned in a module invariant. This means that clients can still expect that count returns a value >= 0

Now if is_empty = False then by count >= 0, count > 0 must be true because not is_empty if and only if count /= 0.

A software component is correct in the sense of these contracts if you finally prove it, using the assertions and rules from the language definition.

The internal view of the module, in this case a package body, shows how assertions can be placed in an program. It is important to understand that pragma assert in Ada, require in Eiffel, etc. are tightly integrated with the languages' exception handling mechanisms. This is unlike what you might be guessing if you know C's assert. (The implementation of the example stack is actually based on Ada.Containers, similar to how Eiffel's STACK classes are usually implemented. It could also be based on D's arrays, or whatever language you choose.)

pragma Assertion_Policy(Check);
  ...
   s: Vector;
  ...
   function top return Item is
   begin
      pragma assert(not is_empty, "stack is empty");
      return s.Last_Element;
   end top;

Think about the effects of turning assertion checking on or off. Assertions express a contract, they do not handle invalid input.

Exceptions and Contracts

What if a precondition is true, but some statement from the executing subprogram raises an exception? Chances are that the postcondition can no longer be established by the subprogram. It will fail. However, what about the state of the module?

The first answer to the question about the state of the module is given by this rule:

When an exception is allowed to propagate from the subprogram, the module invariant must first be established.

The second answer can be different, depending on the language. The Eiffel way, for reference, is to retry the routine in case of an exception: If the exception is handled, and the subprogram should retry to fulfil its postcondition, then both its precondition, and the module invariant must first be established. (Otherwise the system cannot act like invoking the routine again without violating the contract.)

Ada, like some other languages, has nested blocks, so exception handling could start from a block's preconditions. Hence if you manage to restore the block's preconditions, you can retry the block. A block may be nested inside a loop, for example. Then your handler will have to assign values to variables satisfying the necessary preconditions of a loop execution.

Inheritance

TBD

In brief, the preconditions of overridden methods are or-ed, the post-conditions are and-ed.

For modules built around derived types, it must be possible to substitute an object of a derived type for an object of the parent type such that a dispatching call can still rely on the parent's contract. Likewise, the postconditions of the feature that gets actually called must imply the postconditions of the parents' features.

A Flaw

Given an OO parent type T, together with one of its methods,

 type T is tagged private;

 function foo(x: T; n: Count) return Natural;
 -- ! pre: n >= 42

and a type derived from T, called D, with the method overridden,

 type D is new T with private;
 
 overriding
 function foo(x: D; n: Count) return Natural;
 -- ! pre: n >= 66

imagine a reference to an OO variable of some type in the T hierarchy. Then

 declare
     x: access T'Class := new D;
 begin
     x.foo(42);
 end;

Who is to blame?

Concurrency

TBD

One new (to the discussion so far) problem introduced by concurrent execution is this: Suppose

a module's routines should do their work on behalf of more than one caller at a time,
an “instance” of some routine may be interrupted by another “instance”

Then for example what was true about the module state when the first call was initiated might no longer be true after executing the second call has changed the state of the module. This extends to pre/postcondition checks: Since the assertions of the routines will likely refer to their module's state (and to anything visible in general), they can become inconsistent.

A first attempt at a solution is to make the precondition check, the execution of a routine, and the postcondition check sequential and exclusive. That is, as long as a caller is served by the routine, other calls to the routine are made pending until the routine has finished.

But in addition, since the routine's assertions are about module state, any service of the module called by any other caller should be put on hold.

See also guards, SCOOP, Ada (tasking and protected types, synchronized interfaces).