Abstract
Tools for automatically extracting the conditions for which a program is correct with respect to a precondition and postcondition can make proving program correctness easier. We build a HOL-based tool that uses weakest preconditions and semantically derived rules to prove correctness theorems with the verification conditions as assumptions. The rules include two new rules for calculating loop preconditions and recursion correctness while taking specification variables into consideration. The programming language has (recursive) procedures, and both demonic and angelic nondeterminism, which can be used to model interaction. Program variables can be of arbitrary types. Programs with procedures are handled modularly, and proved facts about individual procedures are stored in a database available to all programs.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
R. J. Back and J. von Wright. Refinement Calculus: A Systematic Introduction. Springer-Verlag, 1998.
S. Bensalem, Y. Lakhnech, S. Saidi. Powerful Techniques for the Automatic Generation of Invariants. In Computer Aided Verification, CAV’ 96, LNCS 1102, 1996.
M. J. Butler, J. Grundy, T. Långbacka, R. Rukšenas, and J. von Wright. The Refinement Calculator: Proof Support for Program Refinement. In Proc. FMP’97-Formal Methods Pacific, Discrete Mathematics and Theoretical Computer Science, Wellington, New Zealand, July 1997. Springer-Verlag.
L. A. Dennis, G. Collins, M. Norrish, R. Boulton, K. Slind, G. Robinson, M. Gordon, and T. Melham, The PROSPER Toolkit. In Proc. of TACAS 2000, LNCS 1785, Springer-Verlag.
E. W. Dijkstra. A Discipline of Programming. Prentice-Hall International, 1976.
J. C. Filliatre. Proof of imperative programs in Type Theory. In International Workshop, TYPES’98, Kloster Irsee, Germany. LNCS 1657, Springer-Verlag, 1998.
M. Gordon. Mechanizing Programming Logics in Higher Order Logic. In G. Birtwistel and P. Subrahmanyam, editors, Current Trends in Hardware Verification and Automated Theorem Proving. Springer-Verlag, 1989.
M. J. C. Gordon and T. F. Melham. Introduction to HOL. Cambridge University Press, New York, 1993.
N. Heintze, J. Jaffar, and R. Voicu. A Framework for Combining Analysis and Verification. In Proc. of POPL 2000, pp 26–39, 2000.
C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM, 12(10):576–583, 1969.
P. V. Homeier. Trustworthy Tools for Trustworthy Programs: A Mechanically Verified Verification Condition Generator for the Total Correctness of Procedures. Ph.D. Dissertation, UCLA Computer Science Department, 1995.
C. B. Jones. Systematic Software Development Using VDM. Prentice-Hall International, 1986.
T. Kleymann. Hoare Logic and VDM: Machine-Checked Soundness and Completeness Proofs. Ph.D. Thesis, University of Edinburgh, ECS-LFCS-98-392, FCS, 1998.
L. Laibinis. Mechanized Formal Reasoning about Modular Programs. Ph.D. Thesis, Turku Centre for Computer Science Dissertations, 24, Finland, April, 2000.
L. Laibinis and J. von Wright. What’s in a Specification. In Proc. International Refinement Workshop and Formal Methods Pacific 1998, Discrete Mathematics and Theoretical Computer Science, Canberra, Australia, 1998. Springer-Verlag.
T. Nipkow. Winskel is (almost) Right: Towards a Mechanized Semantics Textbook. Formal Aspects of Computing, 10(2):171–186, 1998.
D. von Oheimb. Hoare Logic for Mutual Recursion and Local Variables. In Foundations of Software Technology and Theoretical Computer Science (FST and TCS), Springer LNCS, 1999.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Celiku, O., von Wright, J. (2002). Theorem Prover Support for Precondition and Correctness Calculation. In: George, C., Miao, H. (eds) Formal Methods and Software Engineering. ICFEM 2002. Lecture Notes in Computer Science, vol 2495. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36103-0_32
Download citation
DOI: https://doi.org/10.1007/3-540-36103-0_32
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00029-7
Online ISBN: 978-3-540-36103-9
eBook Packages: Springer Book Archive