Technical reports
Verifying modular programs in HOL
J. von Wright
January 1994, 25 pages
DOI: 10.48456/tr-324
Abstract
This paper describes a methodology for verifying imperative programs that are modular, i.e., built using separately defined functions and procedures.
The verification methodology is based on a simple programming notation with a weak precondition semantics. This notation has been semantically embedded in the HOL theorem prover [3] and a number of laws have been derived from the semantics.
These semantic laws are used to prove the correctness of functional procedures, by showing that a call to the procedure in question is equivalent to a call to the corresponding function as it is defined in the logic. This makes it possible to specify a program in an essentially functional style, but the functions are then implemented as imperative procedures (like user-defined functions in FORTRAN or Pascal).
We also show how to define non-functional procedures and calls to such procedures. Procedures may be recursive. Altogether, this gives us a basis for mechanical verification of modular imperative programs.
Full text
PDF (1.3 MB)
BibTeX record
@TechReport{UCAM-CL-TR-324, author = {von Wright, J.}, title = {{Verifying modular programs in HOL}}, year = 1994, month = jan, url = {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-324.pdf}, institution = {University of Cambridge, Computer Laboratory}, doi = {10.48456/tr-324}, number = {UCAM-CL-TR-324} }