Natural Language and the Boundary of Ambiguity

So far we have descended from a VDM implicit specification into design, implementation, and tests (parts 1 and 2), and examined the premise of TDD without a specification (part 3). Finally, let us compare against the most common practice of all — a specification document in natural language. Here is the same sort specification, in plain words.

At first glance there is nothing wrong with it. But what exactly does "sorted" mean? Ascending or descending? Are duplicate elements preserved? Must the output even be a rearrangement of the input? Look closer and "size" is ambiguous too — the length of the sequence, or the magnitude of the numbers? Nothing in this document lets you trace the answers. Just as with TDD, the reader has no choice but to infer the author's intent through common sense.

In the VDM specification, "sorted" corresponds to the postcondition's IsPermutation(r, l) and IsOrdered(r). If either word feels ambiguous, you can follow its definition.

The forall, inds, and l(i) appearing inside IsOrdered are language constructs whose meaning is fixed by the VDM-SL language standard (ISO/IEC 13817-1). Every word in the specification, followed far enough, bottoms out in a rigorous definition. There is no dead-end word — no term used without ever being defined.

Sorting is nearly self-evident to everyone, so in this example the gap with natural language looks small. But once a concept's definition varies across cultures, the same ambiguity becomes a chasm. Consider a requirement like the following.

What exactly does "problematic by social convention" refer to? The interpretation differs by country, by industry, and by individual. A human team might proceed on "common sense will cover it" — the implicit premise of shared culture we saw on the previous page. But the moment interpretations diverge, this specification endorses several mutually contradictory implementations as "correct" at the same time.

Natural language can approach rigor by piling up footnotes and glossaries. But there is no way to objectively verify where ambiguity still remains. The ambiguity stays scattered across the text — unauditable.

Let us write the same requirement in VDM, replacing the diffuse phrase "problematic by social convention" with a referenceable definition.

The diffuse phrase has become the precise predicate not (name in set blocked), and what blocked refers to — the set of organization names published by organization A as classification list α — is recorded as an annotation in exactly one place. Within the formalization, blocked is treated as a given set. Of course, ambiguity has not dropped to zero. Whether list α is appropriate, and when updates propagate — those remain outside the formalization.

What matters is that the remaining ambiguity has been localized into a single name: blocked. Exactly how far the specification is rigorous, and where the external reference begins — anyone can point to that boundary objectively. The review question changes from the vague "is there ambiguity somewhere in this text?" to the concrete "are the definition and governance of list α sound?".