Overspecification

One of the key concepts in software engineering is the need to avoid over specification. It is natural that at some point in the decomposition of the specification of a system to be created that the specifier resorts to a description of how to do it instead of a statement of what must be done. When you drill down into this the problem is the difference between denotational semantics versus axiomatic semantics. In the first, the problem to be decomposed is given in what is hopefully the most abstract algorithmic way possible by the specifier. The problem is that it assumes there is only one algorithm possible for the solution and it locks the implementor into that algorithm.

The alternative is the axiomatic semantics of stating the pre- and post-conditions as well as any invariants in the required solution. This at once gives the implementer the choice of algorithm and implementation choices possible in the solution set. But at the same time it gives the implementer no direction as to how it can be achieved. Traditionally in commercial work the axiomatic method of specification has not been used merely because of the difficulty of making these statements about the required implementation. They are seen in formal methods but the difficulty of implementing formal methods is well known.