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:
fillis
-- Fill tank with liquid
requirein_valve.open
out_valve.closeddeferred
-- i.e., no implementation
ensurein_valve.closed
out_valve.closed
is_fullend
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.
This website uses cookies to improve your experience. We'll assume you're ok with this, but you can opt-out if you wish.AcceptRead More
Privacy & Cookies Policy
Privacy Overview
This website uses cookies to improve your experience while you navigate through the website. Out of these, the cookies that are categorized as necessary are stored on your browser as they are essential for the working of basic functionalities of the website. We also use third-party cookies that help us analyze and understand how you use this website. These cookies will be stored in your browser only with your consent. You also have the option to opt-out of these cookies. But opting out of some of these cookies may affect your browsing experience.
Necessary cookies are absolutely essential for the website to function properly. This category only includes cookies that ensures basic functionalities and security features of the website. These cookies do not store any personal information.
Any cookies that may not be particularly necessary for the website to function and is used specifically to collect user personal data via analytics, ads, other embedded contents are termed as non-necessary cookies. It is mandatory to procure user consent prior to running these cookies on your website.