Minimisation in Formal Specification and Design

  • A. M. Gravell
Conference paper
Part of the Workshops in Computing book series (WORKSHOPS COMP.)


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.


Cost Function Multiprocessor System Proof Obligation Data Refinement Information Processing Letter 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [Bellman 57]
    R. Bellman. Dynamic Programming. Princeton University Press. 1957.Google Scholar
  2. [Bird 86]
    R. S. Bird. Transformational Programming and the Paragraph Problem. Science of Computer Programming no 6. Pages 159–189. 1986.MATHCrossRefGoogle Scholar
  3. [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
  4. [van Gasteren 88]
    A. J. M. van Gasteren. On the Shape of Mathematical Arguments. PhD Thesis. Eindhoven University. 1988.Google Scholar
  5. [Hayes 89]
    I. J. Hayes and C. B. Jones. Specifications are not (necessarily) executable. Private communication. 1989.Google Scholar
  6. [Hoare 87]
    C. A. R. Hoare, J. He, and J. Sanders. Prespecification in Data Refinement. Information Processing Letters vol 25 no 2 pages 71–76. 1987.MathSciNetMATHCrossRefGoogle Scholar
  7. [Josephs 88]
    M. B. Josephs. The Data Refinement Calculator for Z Specifications. Information Processing Letters vol 27 no 1 pages 29–33. Feb 1988.MathSciNetCrossRefGoogle Scholar
  8. [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
  9. [Knuth 81]
    D. E. Knuth. Breaking Paragraphs into Lines. Software Practice and Experience vol 11 pages 1119–1184. 1981.MATHCrossRefGoogle Scholar
  10. [Meyer 85]
    B. Meyer. On Formalism in Specifications. IEEE Software vol 2 no 1 pages 159–176. 1985.CrossRefGoogle Scholar
  11. [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
  12. [Morgan 86]
    C. Morgan. Telephone Network. In Specification Case Studies. Ed. I. J. Hayes. Pages 73–87. Prentice Hall. 1986.Google Scholar
  13. [Morgan 88]
    C. Morgan. On the Refinement Calculus. Programming Research Group Monograph 70. 1988.Google Scholar

Copyright information

© Springer-Verlag London 1990

Authors and Affiliations

  • A. M. Gravell
    • 1
  1. 1.Department of Electronics and Computer ScienceUniversity of SouthamptonUK

Personalised recommendations