Abstract
The meaning of a program can be specified by pre- and postconditions, and the semantics of each statement can be defined by its weakest precondition. We present the development including implementation of a simple system to verify small programs. The system contains a weakest precondition calculator and a theorem prover; it is specified using VDM (as described in [1]) and implemented in Prolog. This paper shows how VDM was used as a natural specification tool and contains in appendices some key functions in VDM and their translation into Prolog.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Dines Bjørner. Software Architectures and Programming Systems Design. 1986, Department of Computer Science, Technical University, Denmark.
J.-P. Delahaye. Formal Methods in Artificial Intelligence. 1987, North Oxford Academic Publishers Ltd.
E. W. Dijkstra. A Discipline of Programming. 1976, Prentice-Hall
Chr. Gram. Weakest Precondition for Read. Techn. Report ID-TR 1989-57, Department of Computer Science, Technical University, Denmark.
D. Gries. The Science of Programming. 1981, Springer-Verlag.
A.G. Hamilton. Logic for Mathematicians. 1978, Cambridge University Press.
Cliff B. Jones. Systematic Software Development Using VDM. 1986, Prentice-Hall.
A. Olsen. User manual for TFL's META-IV tool. 1988, TFL.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1990 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Haastrup, P., Gram, C. (1990). Correctness in the small. In: Bjørner, D., Hoare, C.A.R., Langmaack, H. (eds) VDM '90 VDM and Z — Formal Methods in Software Development. VDM 1990. Lecture Notes in Computer Science, vol 428. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-52513-0_5
Download citation
DOI: https://doi.org/10.1007/3-540-52513-0_5
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-52513-4
Online ISBN: 978-3-540-47006-9
eBook Packages: Springer Book Archive