Metavariables and Conditional Refinements in the Refinement Calculus

  • Raymond G. Nickson
  • Lindsay J. Groves
Part of the Workshops in Computing book series (WORKSHOPS COMP.)


We describe two techniques for the refinement calculus that facilitate goal-directed development. The techniques achieve this by allowing the deferring of decisions about the precise form of refinement steps, so high-level choices can be expressed as soon as those choices are appropriate. Metavariables are place-holders for components of partly developed programs that will be instantiated when they are suitably constrained by later refinements. The conditional refinements technique allows the development of alternative refinements of a specification, and the collection of those alternative refinements into a guarded command set.

We think that programmers developing programs using the refinement calculus make use of both of these techniques informally, but the written derivation does not usually reflect their use. We describe and illustrate a rigorous way to apply these techniques and record their use.


Sequential Composition Natural Deduction Proof Obligation Rule Application Applicability Condition 
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. [1]
    Carroll C. Morgan and Ken Robinson. Specification statements and refinement. IBM Journal of Research and Development, 31 (5): 546–555, September 1987.CrossRefMathSciNetMATHGoogle Scholar
  2. [2]
    R. J. R. Back. A calculus of refinements for program derivations. Acta Inform atica, 25: 593–624, 1988.CrossRefMathSciNetMATHGoogle Scholar
  3. [3]
    Carroll Morgan. Programming from Specifications. Prentice Hall, 1990.Google Scholar
  4. [4]
    Lindsay Groves, Raymond Nickson and Mark Utting. A tactic driven refinement tool. In Cliff B. Jones, Roger C. Shaw and Tim Denvir, editors, Fifth Refinement Workshop, Workshops in Computing, pages 272–297. BCS FAGS, Springer-Verlag, 1992.Google Scholar
  5. [5]
    David Gries. The Science of Programming. Springer-Verlag, 1981.Google Scholar
  6. [6]
    E. W. Dijkstra. A Discipline of Programming. Academic Press, 1976.Google Scholar
  7. [7]
    Lindsay J. Groves and Raymond G. Nickson. An intelligent editor for constructing correct programs. In Proceedings of the Third New Zealand Conference on Expert Systems. New Zealand Expert Systems Special Interest Group, 1988.Google Scholar
  8. [8]
    Carroll Morgan. The specification statement. ACM Transactions on Programming Languages and Systems, 10 (3): 403–419, July 1988.CrossRefMATHGoogle Scholar
  9. [9]
    Greg Nelson. A generalization of Dijkstra’s calculus. ACM Transactions on Programming Languages and Systems, 11 (4): 517–561, October 1989.CrossRefGoogle Scholar
  10. [10]
    Lindsay Groves. Deriving language recognition algorithms: A case study in combining program specialisation and data refinement. In David Till and Roger C. F. Shaw, editors, Sixth Refinement Workshop, Workshops in Computing. BCS FACS, Springer-Verlag, 1994.Google Scholar
  11. [11]
    L. Naish. Negation and quantifiers in NU-Prolog. In Proceedings of the Third International Conference on Logic Programming, 1986.Google Scholar
  12. [12]
    Tim Clement. Using metavariables in natural deduction proofs. In Cliff B. Jones, Roger C. Shaw and Tim Denvir, editors, Fifth Refinement Workshop, Workshops in Computing. BCS FACS, Springer-Verlag, 1992.Google Scholar
  13. [13]
    C. B. Jones, K. D. Jones, P. A. Lindsay and R. Moore. mural: A Formal Development Support System. Springer-Verlag, 1991.Google Scholar
  14. [14]
    Joseph M. Morris. A theoretical basis for stepwise refinement and the programming calculus. Science of Computer Programming, 9: 287–306, 1987.CrossRefMathSciNetMATHGoogle Scholar

Copyright information

© British Computer Society 1994

Authors and Affiliations

  • Raymond G. Nickson
    • 1
  • Lindsay J. Groves
    • 2
  1. 1.Software Verification Research CentreUniversity of QueenslandBrisbaneAustralia
  2. 2.Department of Computer ScienceVictoria University of WellingtonWellingtonNew Zealand

Personalised recommendations