Expression Decomposition in a Rely/Guarantee Context

  • Joey W. Coleman
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5295)


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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [CJ00]
    Collette, P., Jones, C.B.: Enhancing the tractability of rely/guarantee specifications in the development of interfering operations. In: Foundations of Computing, pp. 277–307. MIT Press, Cambridge (2000)Google Scholar
  2. [CJ07]
    Coleman, J.W., Jones, C.B.: A structural proof of the soundness of rely/guarantee rules. Journal of Logic and Computation 17(4), 807–841 (2007)zbMATHCrossRefMathSciNetGoogle Scholar
  3. [Col08]
    Coleman, J.W.: Constructing a Tractable Reasoning Framework upon a Fine-Grained Structural Operational Semantics. PhD thesis, Newcastle University, Newcastle Upon Tyne (January 2008)Google Scholar
  4. [dR01]
    de Roever, W.-P.: Concurrency Verification: Introduction to Compositional and Noncompositional Methods. In: Tracts in Theoretical Computer Science, vol. 54. Cambridge University Press, New York (2001)Google Scholar
  5. [Jon81]
    Jones, C.B.: Development Methods for Computer Programs including a Notion of Interference. PhD thesis. Oxford University (June 1981); Printed as: Programming Research Group, Technical Monograph 25Google Scholar
  6. [Jon90]
    Jones., C.B. (ed.): Systematic Software Development Using VDM, 2nd edn. Prentice- Hall, Inc., Englewood Cliffs (1990)Google Scholar
  7. [Jon07]
    Jones, C.B.: Splitting atoms safely. Theoretical Computer Science 375(1-3), 109–119 (2007); (Festschrift for John C. Reynolds’s 70th birthday)zbMATHCrossRefMathSciNetGoogle Scholar
  8. [Owi75]
    Owicki, S.S.: Axiomatic Proof Techniques for Parallel Programs. PhD thesis, Department of Computer Science, Cornell University, Ithaca, NY, USA, 75-251 (1975)Google Scholar
  9. [Plo81]
    Plotkin, G.D.: A structural approach to operational semantics. Technical Report DAIMI FN-19, Aarhus University (1981)Google Scholar
  10. [Plo04]
    Plotkin, G.D.: A structural approach to operational semantics. Journal of Logic and Algebraic Programming, 60–61, 17–139 (2004)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Joey W. Coleman
    • 1
  1. 1.School of Computing ScienceNewcastle UniversityUK

Personalised recommendations