Computer Laboratory

Technical reports

C formalised in HOL

Michael Norrish

December 1998, 156 pages

This technical report is based on a dissertation submitted August 1998 by the author for the degree of Doctor of Philosophy to the University of Cambridge.

Abstract

We present a formal semantics of the C programming language, covering both the type system and the dynamic behaviour of programs. The semantics is wide-ranging, covering most of the language, with its most significant omission being the C library. Using a structural operational semantics we specify transition relations for C’s expressions, statements and declarations in higher order logic.

The consistency of our definition is assured by its specification in the HOL theorem prover. With the theorem prover, we have used the semantics as the basis for a set of proofs of interesting theorems about C. We investigate properties of expressions and statements separately.

In our chapter of results about expressions, we begin with two results about the interaction between the type system and the dynamic semantics. We have both type preservation, that the values produced by expressions conform to the type predicted for them; and type safety, that typed expressions will not block, but will either evaluate to a value, or cause undefined behaviour. We then also show that two broad classes of expression are deterministic. This last result is of considerable practical value as it makes later verification proofs significantly easier.

In our chapter of results about statements, we prove a series of derived rules that provide C with Floyd-Hoare style “axiomatic” rules for verifying properties of programs. These rules are consequences of the original semantics, not independently stated axioms, so we can be sure of their soundness. This chapter also proves the correctness of an automatic tool for constructing post-conditions for loops with break and return statements.

Finally, we perform some simple verification case studies, going some way towards demonstrating practical utility for the semantics and accompanying tools.

This technical report is substantially the same as the PhD thesis I submitted in August 1998. The minor differences between that document and this are principally improvements suggested by my examiners Andy Gordon and Tom Melham, whom I thank for their help and careful reading.

Full text

PDF (0.8 MB)

BibTeX record

@TechReport{UCAM-CL-TR-453,
  author =	 {Norrish, Michael},
  title = 	 {{C formalised in HOL}},
  year = 	 1998,
  month = 	 dec,
  url = 	 {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-453.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  number = 	 {UCAM-CL-TR-453}
}