Taxonomy/2. Methodology/Monotonic Refinement

Classical software engineering recommends monotonic refinement and developed theories, languages, and tools to support this method.

Applicability

Monotonic refinement works under the following preconditions:

The specification...

• Is given and cannot be changed, at least not considerably,
• is complete (specifies all relevant properties),
• is consistent (contradiction-free),
• is realisable in the solution domain.

Examples are mathematical functions to be impemented as programs for a universal machine. Monotonic refinement is efficient, theoretically sound, and works very well. But only if a definitive, implementable specification is given in the beginning. This is the case when the artefact to be designed is to be part of a surrounding artefact, for which a correctness theorem exists.

The method

You start from a given formal specification that is not doubted. You know that an artefact can be constructed in a well-understood, formally specified solution domain, usually the constructs of a programming language. From the given specification you derive an intermediate result that introduces some structure (refinement!), but you ensure that the properties of that intermediate result imply the original specification (monotonic!). From that intermediate result you derive another one, and so on, until you end up in the solution domain. The result is "correct by construction" and does not require an extra correctness proof. You thus start from the given right hand side of the correctness theorem, develop the left hand side by correct refinement steps, and you know the resulting theorem is proven.

Criticism

The method would also work for any other realisable specification, once it has been found. It could be argued that the authors of classical SE-textbooks first find their specifications and blueprints by informal Non-Monotonic Refinement and then present their correctness theorem as if it had been derived by monotonic refinement.

In practise, the definitive realisation, a machine program for a real computer, often is not quite an implementation of the specification, due to the precision of computer arithmetic, bounds for numbers, and the like. This resembles Non-Monotonic Refinement, only the deviation from the original specification is considered negligible.