Using libristra's Design by Contract system

What is Design-by-contract

Design-by-contract (DBC) is a way of managing interfaces so that programmers know what the expectations are on each side of an interface. There are (at least!) two possible issues:

1. Declaring the preconditions of a function (or method, it really doesn't matter). A precondition is something that must be true for an arbitrary input value.
2. Declaring the postconditions: the things that must be true at the end of a function.
3. Enforcing the pre- and postconditions. When a contract cannot be honored because a precondition or postcondition fails, what should be done? One could throw an exception, set an error number, write to a log, or maybe just do nothing.

libristra's DBC helps by allowing a library programmer to implement assertions that specify requirements on inputs, and to check invariants on outputs. When a DBC assertion fails, different actions can be chosen: an exception can be thrown, a notice can be sent to a log/stream, or nothing at all.

There are severeal basic assertions:

• Require: a precondition that must be true for the function to operate correctly
• Ensure: check that a postcondition is true
• Check: specify an invariant.
• Insist: some super-important invariant that must always be true.

Require and Check can be turned on and off at compile time; if turned off, there is no penalty--they compile to null-ops. Insist assertions are always on.

There are a number of more specific Require assertions that capture common uses. These include GreaterThan, Equal, OneOf, etc. These offer more precise reporting to the programmer.

More about preconditions and postconditions.

For example, suppose you have a function double divide_two_by(double x) { return 2.0 / x; }. What if the caller passes 0 to this function? DBC would say, make a precondition that the user not divide by 0:

double divide_two_by(double x) {
  Require( x != 0.0, "x must not equal 0!");
  return 2.0 / x;
}

or, more succinctly:

double divide_two_by(double x) {
  NotEqual( x, 0.0);
  return 2.0 / x;
}

Similarly, a postcondition is declared, and possibly enforced, via Ensure:

unique_ptr<widget_t> make_widget(interfact_t &iface){
  ... widgety goodness
  auto w = make_unique<widget_t>(args);
  Ensure(w,"Pithy error message");
  return w;
} 

Historical Note

Design by contract is a coherent philosophy promulgated by Bertrand Meyer in his book, Object Oriented Software Construction. There is an entire language, Eiffel, devoted to it. We're a little more flexible and likely less coherent about the matter.