Welcome to the new version of CaltechAUTHORS. Login is currently restricted to library staff. If you notice any issues, please email coda@library.caltech.edu
Published April 25, 2001 | Submitted
Report Open

Refinement Calculus, Lattices and Higher Order Logic

Back, R. J. R.

Abstract

We show how to describe refinement calculus in a lattice theoretic framework. The predicate transformer lattice is built by pointwise extensions from the truth value lattice. A simple but very powerful statement language characterizes the monotonic predicate transformer lattice. We show how to formalize the calculus in higher order logic. We also show how to express data refinement in this framework. A theorem of data refinement with stuttering is proved, to illustrate the algebraic nature of reasoning in this framework.

Additional Information

© 1992 California Institute of Technology. I would like to thank Robert Barta, Ulla Binau, Marcel van de Groot, Peter Hofstee, Rustan Leino, Carroll Morgan, Jan van de Snepscheut and Joakim von Wright for very helpful discussions on the topics treated here.

Attached Files

Submitted - 92-22.pdf

Submitted - 92-22.ps

Files

92-22.pdf
Files (1.8 MB)
Name Size Download all
md5:c2b1ffb2fa52f92079d51915173551e0
829.3 kB Preview Download
md5:6ab70cdabbf492718b82714dd8468379
1.0 MB Download

Additional details

Created:
August 20, 2023
Modified:
January 13, 2024