Do not read this

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.