Toggle Main Menu Toggle Search

Open Access padlockePrints

Expression Decomposition in a Rely/Guarantee Context

Lookup NU author(s): Dr Joey Coleman



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

Publication status: Published

Series Title: School of Computing Science Technical Report Series

Year: 2008

Pages: 18

Print publication date: 01/07/2008

Source Publication Date: July 2008

Report Number: 1108

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

Place Published: Newcastle upon Tyne