Computer Laboratory

Technical reports

Mechanizing a theory of program composition for UNITY

Lawrence Paulson

November 2000, 28 pages

Abstract

Compositional reasoning must be better understood if non-trivial concurrent programs are to be verified. Chandy and Sanders [2000] have proposed a new approach to reasoning about composition, which Charpentier and Chandy [1999] have illustrated by developing a large example in the UNITY formalism. The present paper describes extensive experiments on mechanizing the compositionality theory and the example, using the proof tool Isabelle. Broader issues are discussed, in particular, the formalization of program states. The usual representation based upon maps from variables to values is contrasted with the alternatives, such as a signature of typed variables. Properties need to be transferred from one program component’s signature to the common signature of the system. Safety properties can be so transferred, but progress properties cannot be. Using polymorphism, this problem can be circumvented by making signatures sufficiently flexible. Finally the proof of the example itself is outlined.

Full text

PDF (0.2 MB)

BibTeX record

@TechReport{UCAM-CL-TR-507,
  author =	 {Paulson, Lawrence},
  title = 	 {{Mechanizing a theory of program composition for UNITY}},
  year = 	 2000,
  month = 	 nov,
  url = 	 {http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-507.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  number = 	 {UCAM-CL-TR-507}
}