Expression Decomposition in a Rely/Guarantee Context

  1. Lookup NU author(s)
  2. Dr Joey Coleman
Author(s)Coleman JW
Publication type Report
Series TitleSchool of Computing Science Technical Report Series
Source Publication DateJuly 2008
Report Number1108
Full text is available for this publication:
This paper describes a technique of expression decomposition which allows the use of rely/guarantee development rules that do not assume atomic expression evaluation. This decomposition provides a means of addressing the fact that the logical meaning of expressions relative to a single state and the semantic evaluation of expressions in a fine-grained concurrent language do not provide the same results; in particular, the former results in a single value whereas the latter can result in many possible values. Rely/guarantee development rules tend to depend on the logical meaning of expressions in cases where they are used; expression decomposition identifies where it is safe to do so, and provides some tools for where it is not.
InstitutionSchool of Computing Science, University of Newcastle upon Tyne
Place PublishedNewcastle upon Tyne
ActionsLink to this publication