On formalism in specifications Bertrand Meyer, IEEE Software 1985

Following yesterday’s paper that used formal specification methods to resolve ambiguities and uncover potential vulnerabilities in OAuth 2.0, today’s choice is a 1980’s classic from Bertrand Meyer on the merits of formal specification and what it adds beyond natural language descriptions. With thanks once more to Glyn Normington for the recommendation.

Although natural language is the ideal notation for most aspects of human communication, from love letters to introductory programming language manuals, there are cases where it is not appropriate. Software specifications, for example, require more rigorous formalism.

Such formalism doesn’t replace the need for a good natural language description that can be understood by a wide range of stakeholders (and that a reader can use to quickly gain a high-level understanding). What it can do though, is help in the production of a better natural language description than might have existed otherwise.

In fact, mathematical specification of a problem usually leads to a better natural-language description. This is because formal notations naturally lead the specifier to raise some question that might have remained unasked, and thus unanswered, in an informal approach.

Having a natural language description backed by a formal specification also means that instead of having to try and eliminate all ambiguities in prose – which would make for a clumsy document -the reader can be referred to the formal treatment should such questions arise.

As you read the paper, keep in mind that ‘specification’ is used to refer to the document describing what a program should do, as opposed to ‘formal specification’ which is a specification that also uses formal methods. We don’t talk much about specifications these days (we usually use the phrase ‘requirements’ instead) and there’s a tendency to put an implicit ‘formal’ in front of the word specification when read.

‘On formalism in specifications’ is structured around three natural language (and one formal) specifications of the same toy problem. There’s a really interesting back-story and explanation for why Meyer chose this particular problem.

The problem was first described in a 1969 paper by Peter Naur as follows:

Naur’s paper was on program construction and proving, and accompanied this description with a program and a proof that the program had satisfied the requirements.

Goodenough and Gerhart wrote a subsequent paper (two in fact), on the value of program testing. A prevailing view in some circles at the time was that testing was not a good method for validating software (it can only show the presence of bugs, not their absence, as the famous Dijkstra saying goes), and that formal proofs were the only way to go. Goodenough and Gerhart dealt with this objection by showing that many programs which had been proved to be correct in fact contained significant errors. One of their examples was Naur’s program, in which they found seven errors from minor to serious.

The Naur-Goodenough/Gerhart problem is interesting, however, because it exhibits in a particularly clear fashion some of the difficulties associated with natural language specifications. Goodenough and Gerhart mention that the trouble with Naur’s paper was partly due to inadequate specification; since their paper proposed a replacement for Naur’s program, they gave a corrected specification. This specification was prepared with particular care…

As Goodenough and Gerhart noted, “Making these specifications precise is difficult and is an excellent example of the specification task.” Their version is a carefully thought-out description of the problem. As Meyer notes:

If a natural language specification of a programming problem has ever been written with care, this is it. Yet, as we shall see, it is not without its own shadows.

It is for this reason that Meyer chooses this problem to explain the benefits of formal specification – to show what it can add above and beyond a very carefully written natural language specification.

Here’s the Goodenough and Gerhart version of the specification, with some annotations by Meyer I’ll explain next. It’s longer, and clarifies some aspects while introducing some new ambiguities of its own. It’s good, but is it good enough? (Sorry, I couldn’t resist).

Meyer identifies seven sins of (informal) specifications, six of which are exhibited in this revised text.

The seven sins

1. Noise. Noise elements introduce no new information, and can actually obscure the text. One particular variation Meyer calls out is referring to the same concept in different ways – good in literary writing, but bad in specifications. The phrases ‘non-empty sequence’ on line 8, followed by ‘one or more characters’ on line 9 is a simple example.
2. Remorse. Remorse describes the situation where additional conditions or constraints on an element are made not in the place where it is defined (e.g the notion of ‘output’ on lines 12 and 17), but later on where it is used (line 20, introducing the possibility of no output). “It is as if the specifier suddenly regretted his initial definition.”
3. Silence. Despite best efforts, a specifier often leaves a number of features undefined (while over-documenting / specifying others). An example of silence in the revised text is the concept of a line, which is only described in a piece of remorse around line 24.
4. Contradiction. Is the input a stream of characters (line 1), or a sequence of words (line 10)? seq<char> and seq<seq<char>> are not the same thing!
5. Overspecification. “Over-specification in requirements can be annoyingly close to silence. The reader is told too much about the solution while he or she is desperately trying to grasp the problem and figure out – by themselves – features not covered by the text. An example of over-specification in the the Goodenough/Gerhart text is the treatment of end-of-text characters which are an implementation detail of end-of-file detection that only applied on certain systems of the day.
6. Ambiguity. For example, the text says that up to (and including?) the point of an error, the output should correspond to the input, but it doesn’t define what the ‘point of the error’ is. The last acceptable letter? The end of the last acceptable word??
7. Forward references. Not all forward references are bad, but implicit forward references that use a concept before its proper definition, without particular warning to the reader, can present much more of a problem.
8. Wishful thinking. “The presence in the text of an element that defines a feature of the problem in such a way that a candidate solution cannot realistically be validated with respect to this feature.

Yes, you may have noticed that’s eight sins in Meyer’s list of seven sins! Meyer describes remorse as a sub-category of noise, but by his own definitions I think he is wrong to do so. Noise is defined as “the presence in the text of an element that does not carry information relevant to any feature of the problem,” whereas remorse introduces information relevant to a feature of the problem, but at the wrong moment. (Rather delicious to have this error [imho!] in a piece on the importance of precision 😉 ).

Combining formal and informal specifications

The last part of the paper provides a formal specification of the problem based on sets and relations, which I won’t attempt to repeat here. It’s worth saying though that you certainly wouldn’t want only the formal specification – that would be a very information dense way of getting at the intention of the specifier. It’s the balance of a formal specification with a natural language description building on top of it that we really need. Here’s Meyer’s informal specification that was constructed from knowledge gained doing the formal modelling:

The main advantage of natural language texts is their understandability. One should concentrate on this asset rather than trying to use natural language for precision and rigor, qualities for which it is hopelessly inadequate. Understandability is seriously hindered when natural language requirements become ridiculously long in a vain attempt to chase away silence, ambiguity, contradiction etc. Such attempts, as shown by the text studied here, only make matters worse…. Natural language descriptions should remain reasonably short; the exact description of fine points, special cases, precise details etc., should be left to a formal specification.