Another bit of software engineering knowledge from my archive relates to two well-known formal quality methods used in software development. This is from a presentation made at ETH Zurich in 2010.

The background to this is my use of the Eiffel language for 25 years, in which Design by Contract (DbC) figures strongly. Its creator, Bertrand Meyer (currently provost Chair of Software Engineering at Schaffhausen Institute of Technology, Switzerland) coined the term, and developed DbC from earlier formulations such as in the Z language, Djikstra etc.

For those not familiar with ‘contracts’, the full form consists of routine pre- and post-conditions and class invariants. An example of a contract is shown below:

fill is
		-- Fill tank with liquid
	require
		in_valve.open
		out_valve.closed
	deferred
		-- i.e., no implementation
	ensure
		in_valve.closed
		out_valve.closed
		is_full
	end

The contract consists of the require and ensure predicates. The Eiffel website has a full explanation.

DbC was built into Eiffel (since 1988), and has some native supported in some languages like Ada 2012, Clojure, and Kotlin. Many other languages have had additional frameworks or tools created to add contracts, e.g. Java, C#, Groovy and so on.

However, it has to be said that the culture of contract-oriented has not become mainstream, which those of us who use them routinely find strange – they catch so many errors in testing that it is clear they greatly add to the quality of software.

Some experts think that Test-Driven Design (TDD) is a better alternative, since can be used to force developers to prove that each function they write passes an appropriate test, before they write more code. Personally, although I think routine use of unit testing via built-in frameworks is useful, TDD doesn’t replace DbC, and indeed, it can lead some developers to think their software, if passing all its tests, is ‘done’.

Understanding the difference between DbC and TDD is instructive to understanding why TDD, although very useful, doesn’t tell you if your software is correct.

Here’s the basic difference:

• A DbC contract is a mathematical specification of the valid domain (input state space) and/or result (output state space) of a routine within a class;
• TDD is development using ‘tests’ that constitute specific points in a routine’s input value space, which test a routine on an instance.

Mathematically, contracts are intensional (i.e. formally stated) definitions of valid state spaces. Tests are a kind of extensional definition in that they form a list of particular input or output values. From tests on their own, it is hard to a) determine what the total valid value space is and b) hard to see the design intent of the routine.

Since you still do testing if you are using DbC, DbC = contracts + tests. If you are using TDD only, you are just using tests – you have no formal statement of the intended valid state space of input values or results. It is therefore a somewhat haphazard exercise to know what tests to write, especially against someone else’s code. How do you know if you have sufficient coverage? Answer: you don’t.

Indeed, the presence of contracts is an important indicator for writing new tests, since the contract is telling you which kinds of values or states will make the software execute correctly or not.

I remain mystified as to why they are not built into more languages.