Exploring historical formal systems research to steal ideas for modern testing approaches
You probably know I’m a bit of a computer history buff; probably because this field is so dynamic and young that its history seems short enough to get a handle on. (Turns out that’s wrong, but who cares, I’m hooked.)
I’ve started watching the 1982 BBC TV series The Computer Program (watch it in its entirety at archive.org (…and consider giving this wonderful organisation a donation!)). At the end of the first episode (starting at 21:39), author and technology commentator Rex Malik forecasts how the ubiquity of computers in society will transform our lives over the coming decades - in fact up to our present time. He’s astonishingly prescient!
At the start of the clip, the camera pans in close-up over a stack of books on Rex’s desk, to the sound of him mashing keys on a manual typewriter. The title of one of those books caught my attention, and after I’d heard Rex’s accurate prognosis, I reckoned his books were worth taking another look at.
One of them is entitled Every Object is a System, by Dr Patrick Doyle. The book is out of print, and some casual Googling doesn’t turn up any second-hand copies, but I did find a summary of the book, in Bernie Cohen’s sharp, witty, short and (as far as I can tell) accurate A Brief History of Formal Methods (PDF). (…he’s a little too liberal in his use of scare quotes, but we’ll forgive him that.)
Here’s what Cohen has to say about Patrick Doyle and his book Every Object is a System:
In the early 70s, Dr. Patrick Doyle, a mathematician with the Irish Life Insurance Company in Dublin, was commissioned to develop a sales commission tracking system. Not being a ‘systems analyst’, he tackled the problem in an unconventional way: by constructing a model of the required system in set theory. Although he believed that the model he had constructed captured all the requirements of the potential users of the system, he felt that it should be signed off as an acceptable specification before he proceeded to implement it. So he offered the appropriate authority, the Board itself, an interesting alternative: either to receive a long, rather boring and probably ambiguous English-language document, which he could derive from his model, or to follow a short course in elementary set theory which would enable the Board members to read and understand his specification in its original form. The Board took the course, read and understood the formal specification, made some suggestions for change and signed it off. Doyle turned the model into a collection of precise software module specifications which he passed to a small team of (non-mathematical) programmers, who coded and ‘integrated’ the modules. The system worked first time! Paddy Doyle was so far ahead of his time that he had to publish his own book, Every Object is a System (still available from its author), in which he presents his unique view of the rôle of mathematics in information system design, concluding that, ultimately, it is an exercise in topological manifolds.
That article was published in the journal Formal Aspects of Computing in January 1995.
I’m still not sold on formal methods, but the field is nonetheless worth paying attention to. Perhaps the most revealing passage about translating formal methods into a language comprehensible to end users comes in the very next paragraph in Cohen’s paper:
At about the same time, Jean-Raymond Abrial and Steve Schuman, in the IRIA laboratory in France, were also investigating the use of set theory as a medium for system specification. They called their notation Z (after Zermelo and Fränkel, who had defined the well-founded set theory on which they relied). Z was taken up by the Programming Research Group at Oxford University, by then under the leadership of Strachey’s successor, Tony Hoare, where it was enriched, supported by tools and applied to several real problems in industry and commerce. One of these was the CAVIAR system for administering visitors to STL Harlow, ITT’s main laboratory. Abrial himself interviewed the client, Gladys, who manually maintained the records and bookings for the 12000 visitors who passed through STL each year, and constructed the (very elegant) Z specification.
However, unlike Doyle, he made no attempt to instruct Gladys in the mysteries of set theory. Instead, he ‘validated’ his model by deriving from it ten theorems (’emergent’ properties of the model), each of which could be cast in the form of a simple, English-language statement about the system, such as: ‘No two visitors shall share the same hotel room’, and asked Gladys to confirm, or deny, them. Gladys gladly did so and the system was duly implemented.
The model’s ‘emergent properties’ sound to me a lot like the tests that emerge from a specification when using Acceptance Test Driven Development (ATDD). To find out how to do that well, take a look at How to transform bad acceptance tests into awesome ones, by Augusto Evangelisti. Augusto and I used to work together, and it looks like he’s taken ATDD to a very clean level indeed. In my opinion, this approach is the future of automated testing.