A structural proof of the soundness of rely/guarantee rules (revised)
- Lookup NU author(s)
- Dr Joey Coleman
- Professor Cliff Jones
|
|
|
|
| Author(s) | | Coleman JW, Jones CB |
| Publication type | | Report |
| Series Title | | School of Computing Science Technical Report Series |
| Year | | 2007 |
| Date | | June 2007 |
| Report Number | | 1029 |
| Pages | | 31 |
|
|
|
| Full text is available for this publication: |
|
|
|
|
| Various forms of rely/guarantee conditions have been used to record and reason about interference in ways that provide compositional development methods for concurrent programs. This paper illustrates such a set of rules and proves their soundness. The underlying concurrent language allows fine-grained interleaving and nested concurrency; it is defined by an operational semantics; the proof that the rely/guarantee rules are consistent with that semantics (including termination) is by a structural induction. A key lemma which relates the states which can arise from the extra interference that results from taking a portion of the program out of context makes it possible to do the proofs without having to perform induction over the computation history. This lemma also offers a way to think about expressibility issues around auxiliary variables in rely/guarantee conditions. |
|
|
|
| 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/1029.pdf |
| Actions | |  |
