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.
KeywordsGlobal State Specification Language Promotion Schema Forward Simulation Global Invariant
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