Abstract
In his extension of VDM, Jones added a rely and a guarantee-condition to the usual pre and post-condition pair. This extension to the technique permits the specification and development of concurrent, shared-variable systems. We describe the technique in detail by giving an example of a simple, but formal, development. A description of part of a substantial system development that has been carried out on a real project is given in the full version of this paper [Woodcock & Dickinson, 1988]. Conclusions are drawn, both about the rules for concurrent data reification, and about the efficacy of the technique and of the industrial use of formal methods in general.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
6 References
H. Barringer, A Survey of Verification Techniques for Parallel Programs, Lecture Notes in Computer Science 191, Springer-Verlag, 1985.
I. Hayes (editor), Specification Case Studies, Prentice-Hall International, 1987.
C.A.R. Hoare, Communicating Sequential Processes, Prentice-Hall International, 1985.
C.B. Jones, Software Development: a Rigorous Approach, Prentice-Hall International, 1980.
C.B. Jones, “Development Methods for Computer Programs Including a Notion of Interference”, D. Phil. Thesis, Technical Monograph PRG-25, Programming Research Group, Oxford University, 1981.
C.B. Jones, “Specification and Design of (Parallel) Programs” Information Processing 83, R.E.A. Mason (ed), Elsevier Science Publishers B.V. (North-Holland), 1983a.
C.B. Jones, “Tentative Steps Towards a Development Method for Interfering Programs” ACM Trans on Programming Languages and Systems, 5(4), 576–619, 1983b.
C.B. Jones, Systematic Software Development Using VDM, Prentice-Hall International, 1986.
R. Milner, A Calculus of Communicating Systems, Lecture Notes in Computer Science 92, Springer-Verlag, 1980.
J.C.P. Woodcock & B. Dickinson, “Using VDM with Rely and Guarantee-Conditions: Experiences from a Real Project”, full version, Programming Research Group, Oxford University, 1988.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1988 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Woodcock, J.C.P., Dickinson, B. (1988). Using VDM with rely and guarantee-conditions. In: Bloomfield, R.E., Marshall, L.S., Jones, R.B. (eds) VDM '88 VDM — The Way Ahead. VDM 1988. Lecture Notes in Computer Science, vol 328. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-50214-9_27
Download citation
DOI: https://doi.org/10.1007/3-540-50214-9_27
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-50214-2
Online ISBN: 978-3-540-45955-2
eBook Packages: Springer Book Archive