The open archive for STFC research publications

Full Record Details

Persistent URL http://purl.org/net/epubs/work/33534
Record Status Checked
Record Id 33534
Title Do Not Read This
Abstract We discuss the interpretation of read and write frames in mode-l­oriented specification taking the B's generalised substitutions as the vehicle for the presentation. In particular, we focus on the interpre­tation 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 imple­mentation 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 sub­stitution. This semantics yields some non-­interference results between substitutions which cannot be given at this level without the use of read and write frames.
Organisation CCLRC , ESC
Funding Information
Related Research Object(s):
Language English (EN)
Type Details URI(s) Local file(s) Year
Paper In Conference Proceedings In International Symposium of Formal Methods Europe, Copenhagen, Denmark, 22-24 Jul 2002, (2002): 106-125. doi:10.1007/3-540-45614-7_7 2002