Expression Decomposition in a Rely/Guarantee Context
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.
- [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
- [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
- [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
- [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
- [Jon90]Jones., C.B. (ed.): Systematic Software Development Using VDM, 2nd edn. Prentice- Hall, Inc., Englewood Cliffs (1990)Google Scholar
- [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
- [Plo81]Plotkin, G.D.: A structural approach to operational semantics. Technical Report DAIMI FN-19, Aarhus University (1981)Google Scholar
- [Plo04]Plotkin, G.D.: A structural approach to operational semantics. Journal of Logic and Algebraic Programming, 60–61, 17–139 (2004)Google Scholar