Department of Computer Science and Technology

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