Promoting Forward Simulation
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 ). 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.
Unable to display preview. Download preview PDF.
- J.M. Spivey, The Z notation: A Reference manual, Prentice-Hall International (1989).Google Scholar
- 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
- 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
- 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