Theory Interpretations in PVS
- Sam Owre and N. Shankar
- SRI CSL Technical Report SRI-CSL-01-01
Abstract
We describe a mechanism for theory interpretations in PVS. The
mechanization makes it possible to show that one collection of theories is
correctly interpreted by another collection of theories under a
user-specified interpretation for the uninterpreted types and constants.
A theory instance is generated and imported, while the axiom instances are
generated as proof obligations to ensure that the interpretation is valid.
Interpretations can be used to show that an implementation is a correct
refinement of a specification, that an axiomatically defined specification
is consistent, or that a axiomatically defined specification captures its
intended models.
In addition, the theory parameter mechanism has been extended with a
notion of theory as parameter so that a theory instance can be
given as an actual parameter to an imported theory. Theory
interpretations can thus be used to refine an abstract specification or to
demonstrate the consistency of an axiomatic theory. In this report we
describe the mechanism in detail. This extension is a part of PVS version
3.0.
gzipped postscript
or
postscript
or
PDF
BibTeX Entry
@techreport{PVS:Interpretations,
Author= {S. Owre and N. Shankar},
Title= {Theory Interpretations in PVS},
Number= {SRI-CSL-01-01},
Institution= {Computer Science Laboratory, SRI International},
Address= {Menlo Park, CA},
Month= {April},
Year= {2001}}
Sam Owre:
owre@csl.sri.com