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. © 2008 Springer-Verlag.

Publication metadata

Author(s): Coleman J

Publication type: Conference Proceedings (inc. Abstract)

Publication status: Published

Conference Name: Verified Software: Theories, Tools, Experiments

Year of Conference: 2008

Pages: 146-160

Date deposited: 14/01/2011

ISSN: 9783540878728

Publisher: Springer


DOI: 10.1007/978-3-540-87873-5_14

Library holdings: Search Newcastle University Library for this item

Series Title: Lecture Notes in Computer Science

ISBN: 3540878726


Find at Newcastle University icon    Link to this publication