Promoting Forward Simulation

  • P. J. Lupton
Conference paper
Part of the Workshops in Computing book series (WORKSHOPS COMP.)


This paper is about systems that are composed of a super-structure that links together components. When such systems are designed and implemented, it seems very natural to assume that the super-structure can be designed and implemented independently of the design and implementation of the components. So long as the specifications of super-structure and the components match, the resulting assembly should be an implementation of the specification of the original system.

We work in the context of Z (see [1]). In Z, a super-structure corresponds to a promotion schema. What this paper does is to give conditions under which a promotion schema may be a promoter of forward simulation. That is, a promotion schema that when supplied with a valid forward simulation at the component level always produces a valid forward simulation of the composite system. With these results, there is a way not only of dividing the problem of data refinement but also of dividing it into two independent pieces.


Global State Specification Language Promotion Schema Forward Simulation Global Invariant 
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]
    J.M. Spivey, The Z notation: A Reference manual, Prentice-Hall International (1989).Google Scholar
  2. [2]
    J. He, C.A.R. Hoare, J.W. Sanders, Data Refinement Refined — Resume, in Procs. ESOP 86, LNCS 213, pp 187–196, Springer-Verlag.Google Scholar
  3. [3]
    S. King, Ib H. Sorensen, From Specification, through Design, to Code: A Case Study in Refinement, in The Theory and Practice of Refinement (Ed. J. McDermid ), pp 90–121, Butterworths (1989).Google Scholar
  4. [4]
    J.C.P. Woodcock, Mathematics as a Management Tool: Proof Rules for Promotion, in Procs. CSR Sixth Annual Conference on Large Software Systems, Bristol, Elsevier (1989).Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1991

Authors and Affiliations

  • P. J. Lupton
    • 1
  1. 1.Programming Research GroupOxford University Computing LaboratoryOxfordUK

Personalised recommendations