Design By Contract

In our last article we referenced the Cadence language. You may have noticed that it supports preconditions and postconditions. Those are major supporting elements for the concept of Design By Contract. In this article we will look at why Design By Contract is useful for creating correct and secure software.

Design By Contract was first put forward by Bertrand Meyer in 1986 and was baked into his Eiffel programming language. The term was trademarked in 2004 by Dr. Meyer's company (Eiffel Software) and so that is why the term is not generally used by languages that use these concepts.

Let's start with preconditions which are boolean statements at the very beginning of function code. When the function is invoked the preconditions must be true or else an error is triggered and the function is not called. Similarly there are postconditions that are checked immediately before the function returns. (An additional idea is that of an invariant which is a boolean statement that serves as both a precondition and a postcondition.)

Since basically all languages have both functions and assert statements, preconditions and postconditions can easily be added to your code even without explicit support for them. Seen in this way, Design By Contract does not seem like an especially big deal. However it is a much bigger deal in object oriented software since preconditions and postconditions can be added to the definition of abstract types and then, at least in Eiffel, are inherited by all implementations of that type. (Additionally "class invariants" are applied for all functions in an entire class.) But even without inheritance these special types of assertions add a lot of value. Let's look at why this is.

As experienced developers know, fixing bugs is often quite easy. What is often harder is finding the bug in the first place. Design By Contract helps out a lot. If a precondition fails it is always the fault of the calling function. If a postcondition fails, it is the called functions fault. Put enough of these checks in your functions and the problem of locating bugs in your code is drastically reduced.

The next advantage is that you can omit a lot of defensive coding. Specifically you don't have to write error detection and handling code for bad inputs or states that are already trapped by your preconditions.

Another plus is that stateful code can be managed more clearly. While stateless code is usually the best plan, on some occasions you may need functions to be called in specific patterns and managed state is a way to enforce that. If you can relegate your state checking to your preconditions and postconditions then the management of this state should be clearer to your users.

Another great thing happens if you have a documentation tool that knows about preconditions and postconditions. They can be extracted and presented as part of the API presentation for your public functions. This is a great way to help make your code more usable assuming that you keep the precondition logic understandable and use good labels for your preconditions (assuming that your system allows labeled preconditions.)

There are some caveats to Design By Contract. If the logic within the preconditions or postconditions is difficult to understand then most of the value is lost, If you manage to insert a bug directly within your precondition, for example, then finding that bug can be a real headache as the system error messages will point you elsewhere. Also you need to be decide on whether or not the preconditions and postconditions are just for use during development or are actually required in production. Either approach can make sense depending on how you use Design By Contract and how well your language tools support them. In Eiffel the default setting was to always check preconditions but suppress postcondition and invariant checking in production, but you could override this when necessary.

Other than Cadence I am not aware of any smart contract languages that fully or partially support Design By Contract. Will Radix support it? That is unclear at this time but given the statements that finite state machine support is part of the plan, it seems like it might. If not, then equivalently powerful means for managing state and improving code reliability and system correctness should be present. We shall see.

Photo by Alexander Suhorucov from Pexels