Formal Specification: Saying Exactly What a System Must Do
Chapter Eleven
Syllabus topic Module 1, "formal specification"
Pages 32 to 34 of 378
In one line
A formal specification says what a system must do in a language with no room for reading it two ways.
In the wording you can write in an examination: a formal specification is a description of required behaviour written in a notation with a precisely defined syntax and semantics, so that whether an implementation satisfies it is a matter of proof or of mechanical checking rather than of interpretation. It states what must hold, not how to achieve it.
Why ordinary language will not do
Here is a requirement, written the way requirements are usually written: every student has a supervisor.
It has at least three readings.
- For each student there is some supervisor, possibly a different one for each.
- There is one supervisor who supervises all the students.
- Each student has exactly one supervisor, no more.
A sentence in logic has to pick one.
for all S: student(S) implies (exists T: supervises(T, S))
That is reading one, and only reading one. Reading two moves the quantifier to the front; reading three adds a uniqueness condition. The notation forces the choice at writing time rather than leaving it to be discovered in testing.
That is the entire argument for formality, and it is worth stating that plainly: formal notation does not make you right, it makes you specific.
The three things a specification fixes
What must hold. The properties any acceptable implementation has. Not the code, and not the algorithm: the conditions.
Under what assumptions. The preconditions the caller must satisfy. A specification with no preconditions is either trivial or dishonest.
What is left free. Everything not stated is permitted. This is the part beginners get wrong: a specification is also a licence, and anything it fails to forbid is allowed.
Worked example: sorting, specified three ways
Informally. "Sorts the list." Admits an implementation that returns a list of zeroes of the same length, which is sorted.
Better. "Returns a list whose elements are in non-decreasing order and which is a permutation of the input." This closes the hole, and it names both conditions.
Formally.
pre: the list is finite
post: for all i in 0 .. n-2: out[i] <= out[i+1]
post: out is a permutation of in
free: the order of equal elements, unless stability is required
The last line matters. Nothing above forbids swapping two equal elements, so an implementation may. If the caller needs stability it has to be specified, and a caller who assumed it without specifying it has made the classic mistake.
The sūtra as a specification
This is the comparison MU's label is reaching for, and it holds better than most comparisons in this paper.
| A specification has | A śāstra has |
|---|---|
| a notation with fixed syntax | the sūtra style, with its technical terms and markers |
| meanings fixed before use | Book I of the Nyāya Sūtra; Pāṇini's definitional sūtras |
| conditions stated, not procedures | most vidhi rules state what is substituted for what, not how to write it |
| a rule for what happens when two requirements conflict | the four precedence principles, and sūtra 1.4.2 |
| tests | the bhāṣya, which works an instance of every rule |
| errata | the vārttika |
Formal Specification: Saying Exactly What a System Must Do
The row that makes the comparison worth drawing is the fourth. Ordinary specifications are notoriously silent about conflicts between their own clauses, and a reader has to guess. Pāṇini wrote the conflict rule down. [Vipratiṣedha: When Two Rules Collide, the Later Wins] is that rule.
Worked example: a sūtra read as a specification
Pāṇini 7.3.84, in Vasu's translation: "when a sārvadhātuka or an ārdhadhātuka affix follows there is guṇa of the base."
As a specification.
pre: the affix is of kind sarvadhatuka or ardhadhatuka
pre: by 1.1.3, the vowel operated on is one of the ik vowels
post: that vowel is replaced by its guna
free: everything about the affix other than its kind
except: 1.1.5, an affix carrying an indicatory k or ng, blocks this
Three features of that are worth naming. The rule does not say how to perform the substitution, only what the result is. Its second precondition is supplied by another rule, which is what a meta-rule is for. And its exception is declared elsewhere and has priority, which is a stated conflict policy.
What a formal specification is NOT
It is not an implementation. It says what, not how. A specification that fixes the algorithm has over-specified and has forbidden better implementations.
It is not a guarantee of correctness. It can be wrong about what was wanted. Formality moves the argument from "does the code do this?" to "is this what we wanted?", which is progress and not a solution.
It is not necessarily mathematical notation. A precise subset of English with defined terms can be a specification. What matters is that the terms are fixed and the conditions are complete, which is exactly what a śāstra does.
Limits of the classical comparison
Two honest limits, both of which belong in a critical answer.
A sūtra's preconditions are not all written down. Some are carried over from earlier sūtras by anuvṛtti, and which ones are in force at a given rule is decided by the commentary. A modern specification that relied on an editor to say which preconditions applied would be rejected.
Nothing checks a sūtra mechanically. There is no machine that can confirm the rules are consistent, and in fact the tradition disputes the consistency of particular rules at length. A formal specification in the modern sense is one a tool can check; a sūtra is one only a trained reader can check.
Formal Specification: Saying Exactly What a System Must Do
Quick revision
- A formal specification states required behaviour in a notation whose syntax and semantics are fixed, so satisfaction is checkable rather than arguable.
- It fixes three things: what must hold, under what assumptions, and what is left free. Anything not forbidden is permitted.
- "Every student has a supervisor" has three readings; a formula has one.
- The śāstra parallel is strong on definitions, conditions, conflict policy, tests and errata.
- It is weak on two counts: preconditions carried over rather than written, and no mechanical checking.
Test yourself
1. Define a formal specification and name the three things it fixes.
A description of required behaviour in a notation with fixed syntax and semantics, so that satisfaction can be proved or checked mechanically. It fixes what must hold, the assumptions under which it must hold, and what is left free.
2. Give a requirement with more than one reading and show how a formal notation removes the ambiguity.
"Every student has a supervisor" may mean each has some supervisor, or there is one supervisor for all, or each has exactly one. Writing "for all S: student(S) implies (exists T: supervises(T, S))" commits to the first and to nothing else.
3. Why is it a mistake to think a specification only constrains?
Because it also licenses: whatever it does not forbid is permitted. A sort specification that does not require stability permits an unstable implementation, and a caller who assumed stability has misread the licence.
4. Name one respect in which a sūtra falls short of a modern formal specification.
Its preconditions are not all written at the rule; some are carried over from earlier rules and which are in force is settled by the commentary. Relatedly, no tool can check a sūtra set for consistency, so the checking is done by a trained reader.
The rest of this subject
These notes are cut from the University's printed syllabus. Open the syllabus itself for the same subject.