Minimisation in Formal Specification and Design
Minimisation is a useful technique both in specification and in design. In specification it can lead to shorter and more elegant definitions. These will communicate more clearly the intent of the specifier. In design, minimisation can be used to eliminate non-determinism, for instance after a data refinement step. Minimisation is a general technique for removing non-determinism, and can be applied during a constructive refinement. It records the quantity the designer is optimising, which will help later developers to understand the decisions which were taken during design. These points are supported by some simple examples. The Z notation is used in the examples, and it is suggested that the notation would be improved if minimisation could be expressed more concisely. Following the principle of separation of concerns, a suitable notation for minimisation is one which encourages separate definitions of the set of possible solutions and the function (or relation) which will be used to select the minimal solution or solutions.
Unable to display preview. Download preview PDF.
- [Bellman 57]R. Bellman. Dynamic Programming. Princeton University Press. 1957.Google Scholar
- [Bird 86]
- [Dijkstra 89]E. W. Dijkstra. A Computing Scientist’s Approach to a OnceDeep Theorem of Sylvester’s. In Constructive Methods in Computing Science. Ed. Manfred Broy. Springer Verlag Series F vol 55. 1989.Google Scholar
- [van Gasteren 88]A. J. M. van Gasteren. On the Shape of Mathematical Arguments. PhD Thesis. Eindhoven University. 1988.Google Scholar
- [Hayes 89]I. J. Hayes and C. B. Jones. Specifications are not (necessarily) executable. Private communication. 1989.Google Scholar
- [Hoare 87]
- [Josephs 88]
- [Kleene 36]S. C. Kleene. General Recursive Functions of Natural Numbers. Mathematische Annalen Band 112, Heft 5. 1936 pp 727–742. Reprinted in The Undecidable. Ed. Martin Davis. Pages 236–253. Raven Press. 1965.Google Scholar
- [Knuth 81]
- [Meyer 85]
- [Móller 89]B. Móller. Illustrations in Constructive Methods in Computing Science. Ed. Manfred Broy. Springer Verlag Series F vol 55. 1989.Google Scholar
- [Morgan 86]C. Morgan. Telephone Network. In Specification Case Studies. Ed. I. J. Hayes. Pages 73–87. Prentice Hall. 1986.Google Scholar
- [Morgan 88]C. Morgan. On the Refinement Calculus. Programming Research Group Monograph 70. 1988.Google Scholar