Expression decomposition in a rely/guarantee context

Coleman, J

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

Expression decomposition in a rely/guarantee context

Lookup NU author(s): Dr Joey Coleman

Downloads

Accepted version [.pdf]

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