Toggle Main Menu Toggle Search

ePrints

Expression Decomposition in a Rely/Guarantee Context

Lookup NU author(s): Dr Joey Coleman

Downloads


Abstract

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.


Publication metadata

Author(s): Coleman JW

Publication type: Report

Series Title: School of Computing Science Technical Report Series

Year: 2008

Pages: 18

Source Publication Date: July 2008

Report Number: 1108

Institution: School of Computing Science, University of Newcastle upon Tyne

Place Published: Newcastle upon Tyne

URL: http://www.cs.ncl.ac.uk/publications/trs/papers/1108.pdf


Share