Abstract
We discuss the interpretation of read and write frames in model-oriented specification taking the B’s generalised substitutions as the vehicle for the presentation. In particular, we focus on the interpretation of read frames, the semantics of which have not been considered by previous authors. We gives several examples of the relevance of read frames and show that a substitution admits a read respecting implementation if and only if a certain bisimulation condition is satisfied. We use this to motivate a richer semantic model for substitutions which interprets read and write constraints directly in the denotation of a substitution. This semantics yields some non-interference results between substitutions which cannot be given at this level without the use of read and write frames.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
J-R. Abrial. The B-Book. Cambridge University Press, 1995.
R.J.R. Back and M.J. Butler. Fusion and simultaneous substitution in the refinement calculus. Acta Informatica, 35(11):921–940, 1998.
J.C. Bicarregui. Algorithm refinement with read and write frames. In J.C.P. Woodcock and P.G. Larsen, editors, Proceedings of Formal Methods Europe’ 93, volume 670 of Lecture Notes in Computer Science. Springer-Verlag, 1993.
J.C. Bicarregui. Operation semantics with read and write frames. In Sixth Refinement Workshop, Workshops in Computer Science. Springer-Verlag, 1994.
J.C. Bicarregui. Intra-Modular Structuring in Model-oriented Specification: Expressing non-interference with read and write frames. PhD thesis, Manchester University, Computer Science, June 1995. UMCS-95-10-1.
R.J.R. Back and J. von Wright. Refinement Calculus: a Systematic Introduction. Springer-Verlag, 1998.
E.W. Dijkstra. A Discipline of Programming. Prentice Hall, 1976.
S. Dunne. A theory of generalised substitutions. In D. Bert et al, editor, Proceedings of ZB2002. Springer Verlag, LNCS 2272, 2002.
C.B. Jones. Systematic Software Development using VDM. Prentice Hall, 1986.
C.B. Jones. VDM proof obligations and their justification. In M. Mac an Airchinnigh D. Bjørner, C.B. Jones and E.J. Neuhold, editors, Proceedings of VDM’ 87, volume 252 of Lecture Notes in Computer Science. Springer-Verlag, 1987.
R. Milner. Communication and Concurrency. Prentice Hall, 1989.
C. Morgan. Data refinement by miracles. Inf. Proc. Letters, 26(5), Jan. 1988.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bicarregui, J.C. (2002). Do Not Read This. In: Eriksson, LH., Lindsay, P.A. (eds) FME 2002:Formal Methods—Getting IT Right. FME 2002. Lecture Notes in Computer Science, vol 2391. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45614-7_7
Download citation
DOI: https://doi.org/10.1007/3-540-45614-7_7
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-43928-8
Online ISBN: 978-3-540-45614-8
eBook Packages: Springer Book Archive