Predicate Transformers and Higher Order Logic

Back, R.J.R. (1992) Predicate Transformers and Higher Order Logic. Technical Report. California Institute of Technology. [CaltechCSTR:1992.cs-tr-92-24]

Full text available as:

	Postscript - Requires a viewer, such as GhostView
	Other (Adobe PDF (1MB))

Abstract

Predicate transformers are formalized in higher order logic. This gives a basis for mechanized reasoning about total correctness and refinement of programs. The notions of program variables and logical variables are explicated in the formalization. We show how to describe common program constructs, such as assignment statements, sequential and conditional composition, iteration, recursion, blocks and procedures with parameters, axe described as predicate transformers in this framework. We also describe some specification oriented constructs, such as assert statements, guards and nondeterministic assignments. The monotonicity of these constructs over the lattice of predicates is proved, as well as the monotonicity of the statement constructors with respect to the refinement ordering on predicate transformers.

EPrint Type:	Monograph (Technical Report)
Subjects:	All Records
ID Code:	116
Deposited By:	Caltech Library System
Deposited On:	25 April 2001
Record Number:	CaltechCSTR:1992.cs-tr-92-24
Official Persistent URL:	http://resolver.caltech.edu/CaltechCSTR:1992.cs-tr-92-24
Usage Policy:	You are granted permission for individual, educational, research and non-commercial reproduction, distribution, display and performance of this work in any format.

Archive Staff Only: edit this record