Expression Decomposition in a Rely/Guarantee Context
- Lookup NU author(s)
- Dr Joey Coleman
|
|
|
|
| Author(s) | | Coleman JW |
| Publication type | | Report |
| Series Title | | School of Computing Science Technical Report Series |
| Year | | 2008 |
| Date | | July 2008 |
| Report Number | | 1108 |
| Pages | | 18 |
|
|
|
| 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. |
|
|
|
| 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 |
| Actions | |  |
