Predicate Transformers and Higher Order Logic
- Creators
- Back, R. J. R.
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.
Additional Information
© 1992 California Institute of Technology.Attached Files
Submitted - 92.24.pdf
Submitted - 92.24.ps
Files
Additional details
- Eprint ID
- 26767
- Resolver ID
- CaltechCSTR:1992.cs-tr-92-24
- Created
-
2001-04-25Created from EPrint's datestamp field
- Updated
-
2019-10-03Created from EPrint's last_modified field
- Caltech groups
- Computer Science Technical Reports
- Series Name
- Computer Science Technical Reports
- Other Numbering System Name
- Computer Science Technical Reports
- Other Numbering System Identifier
- 92-24