Abstract
This paper presents certain "proof obligations" which can be used to establish the correctness of software design. The design of both sequential and parallel programs is considered. The position is taken that an understanding of formal results of this kind can aid practical software development.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
A Note on Program Verification, P.Aczel, manuscript, January 1982.
On an Inference Rule for Parallel Composition, P.Aczel, manuscript, February 1983.
Now You May Compose Temporal Logic Specifications, H.Barringer, R.Kuiper and A. Pnueli, Procs. of 16th ACM Symposium on Theory of Computing, May 1984.
A Logic Covering Undefinedness in Program Proofs, H. Barringer, J.H. Cheng and C.B. Jones, ACTA Informatica, Vol 21 Part 3, pp251–269, 1984.
A Survey of Verification Techniques for Parallel Programs, H.Barringer, to be published, LNCS, Springer-Verlag.
A Compositional Temporal Approach to a CSP-Like Language, H.Barringer, R.Kuiper and A.Pnueli, IFIP Working Conference on "The Role of Abstract Model in Information Processing", Vienna, January 30th — February 1st, 1985.
Formal Specification and Software Development, D.Bjorner and C.B.Jones, Prentice-Hall International, 1982.
The Specification of Abstract Mappings and their Implementation as B +-Trees, E. Fielding, Oxford University, Monograph PRG-18, 1980.
A Proof Method for Cyclic Programs, N. Francez and A. Pnueli, ACTA Inf. Vol 9 No 2, pp133–157, April 1978.
An Axiomatic Basis of Computer Programming, C.A.R.Hoare, CACM
Parallel Programming: An Axiomatic Approach, C.A.R.Hoare, In Computer Langs, Permagon Press, Vol 1, pp 151–160.
Software Development: A Rigorous Approach, C.B. Jones, Prentice-Hall International, 400 pages, 1980.
Development Methods for Computer Program Including a Notion of Interference, C.B.Jones, Oxford University, Monograph PRG 25, June 1981.
Specification and Design of (Parallel) Programs, C.B.Jones, (invited paper), IFIP 1983, Paris, North-Holland, pp 321–332, September 1983.
Systematic Program Development, C.B.Jones, Symposium ‘Wiskunde en Informatica', Amsterdam, to be published in the Mathematical Centre Tracts.
Tentative Steps Toward a Development Method for Interfering Programs, C.B. Jones ACM Trans. Program. Lang. Syst., Vol 5 No4, pp 596–619, October 1983.
The "Hoare Logic" of Concurrent Programs, L. Lamport, Acta Inf., vol 14 no 1, pp21–37, June 1980.
What Good Is Temporal Logic?, L. Lamport, North-Holland, Proc. of the IFIP 9th World Computer Congress, Paris, pages 657–668, 1983.
A Formal Specification of Line Representations on Graphics Devices, L.S.Marshall, TAPSOFT Joint Conference on Theory and Practice of Software Development, Berlin, March 1985.
Software Construction Using Typed Fragments, N.H.Madhavji, N.Leoutsarakos, D Vouliouris, TAPSOFT Joint Conference on Theory and Practice of Software Development, Berlin, March 1985.
Intuition in Software Development, P. Naur, TAPSOFT Joint Conference on Theory and Practice of Software Development, Berlin, March 1985.
Verifying Properties of Parallel Programs: An Axiomatic Approach, S.S.Owicki and D.Gries, Comm. ACM, Vol 19 No 5, pp 279–285.
The Quest for Compositionality — a Survey of Assertion-based Proof Systems for Concurrent Programs, W.P.de Roever, IFIP Working Conference on "The Role of Abstract Models in Information Processing", Vienna, January 30th — February 1st., 1985.
Temporal Logic Specifications of Communication Protocals, J.Sa, Manchester University, 1984.
Experiences with the PSG-Programming System Generator, G.Snelting, TAPSOFT Joint Conference on Theory and Practice of Software Development, Berlin, March 1985.
The Specification, Design and Implementation of NDB, A. Welsh, M.Sc. Thesis, Manchester University, October 1982.
A Database Programming Language: Definition, Implementation and Correctness Proofs, A. Welsh, Ph.D. thesis, Manchester University, October 1984.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1985 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Jones, C.B. (1985). The role of proof obligations in software design. In: Ehrig, H., Floyd, C., Nivat, M., Thatcher, J. (eds) Formal Methods and Software Development. TAPSOFT 1985. Lecture Notes in Computer Science, vol 186. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-15199-0_3
Download citation
DOI: https://doi.org/10.1007/3-540-15199-0_3
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-15199-9
Online ISBN: 978-3-540-39307-8
eBook Packages: Springer Book Archive