The open archive for STFC research publications

Full Record Details

Persistent URL http://purl.org/net/epubs/work/25595
Record Status Checked
Record Id 25595
Title Operation Semantics with Read and Write Frames
Abstract The read and write "externals" clauses in VDM implicit operation definitions play two distinct roles. On the one hand, they bind the free variables that appear in the preconditions and postconditions, whilst on the other hand, they can be understood to indicate the sets of state variables that an implementation of the operation can be permitted to "read" and "write". However, in the case of the read frame, existing semantic models for VDM give no formal interpretation to this latter role. This paper investigates an extension to the denotational model of operations which captures this informal understanding of the read frame. It interprets the read frame via an extra constraint on the semantics of operations which formalises the idea that the behaviour of an operation should not depend on the variables outside the read frame. This semantics is shown to justify a new formalisation of the satisfiability obligation and to yield a property of non-interference between operations with sufficiently disjoint frames. However, some difficulties remain with this approach as a means of justifying algorithm refinement with read frames the resolution of which would require more substantial changes to the semantic model.
Organisation SERC
Funding Information
Related Research Object(s):
Licence Information:
Language English (EN)
Type Details URI(s) Local file(s) Year
Report RAL Technical Reports RAL-93-098. 1993. RAL-TR-1993-098.pdf 1993