Metavariables and Conditional Refinements in the Refinement Calculus
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.
KeywordsSequential Composition Natural Deduction Proof Obligation Rule Application Applicability Condition
Unable to display preview. Download preview PDF.
- Carroll Morgan. Programming from Specifications. Prentice Hall, 1990.Google Scholar
- 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
- David Gries. The Science of Programming. Springer-Verlag, 1981.Google Scholar
- E. W. Dijkstra. A Discipline of Programming. Academic Press, 1976.Google Scholar
- 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
- 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
- L. Naish. Negation and quantifiers in NU-Prolog. In Proceedings of the Third International Conference on Logic Programming, 1986.Google Scholar
- 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
- C. B. Jones, K. D. Jones, P. A. Lindsay and R. Moore. mural: A Formal Development Support System. Springer-Verlag, 1991.Google Scholar