Department of Computer Science and Technology

Technical reports

Symbolic compilation and execution of programs by proof: a case study in HOL

Juanito Camilleri

December 1991, 31 pages

DOI: 10.48456/tr-240

Abstract

This paper illustrates the symbolic compilation and execution of programs by proof using the proof assistant HOL. We formalise the operational semantics of an Occam-like programming language oc and show how synchronous communication in oc compiles to an intermediate programming language Safe, whose compilation yields instructions intended to drive machines that communicate via shared memory. We show how the symbolic formal manipulation of terms of a programming language, subject to the definition of its semantics, can animate a desired effect — be it compilation or execution. Needless to say, such compilation and execution by proof is rather slow, but it is fast enough to give vital feedback about the compilation algorithm being used. Without such animation it is hard to anticipate whether the compilation algorithm is reasonable before attempting to verify it. This is particularly true when attempting to find a plausible handshaking protocol that implements synchronous communication.

Full text

PDF (1.9 MB)

BibTeX record

@TechReport{UCAM-CL-TR-240,
  author =	 {Camilleri, Juanito},
  title = 	 {{Symbolic compilation and execution of programs by proof: a
         	   case study in HOL}},
  year = 	 1991,
  month = 	 dec,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-240.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-240},
  number = 	 {UCAM-CL-TR-240}
}