ePubs
The open archive for STFC research publications
Home
About ePubs
Content Policies
News
Help
Privacy/Cookies
Suggest an Enhancement
Contact ePubs
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
Contributors
Juan C Bicarregui (SERC Rutherford Appleton Lab.)
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
Keywords
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
Showing record 1 of 1
Recent Additions
Browse Organisations
Browse Journals/Series
Login to add & manage publications and access information for OA publishing
Username:
Password:
Useful Links
Chadwick & RAL Libraries
SHERPA FACT
SHERPA RoMEO
SHERPA JULIET
Journal Checker Tool
Google Scholar