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} }