Title :
Subtypes for specifications: predicate subtyping in PVS
Author :
Rushby, John ; Owre, Sam ; Shankar, Natarajan
Author_Institution :
Comput. Sci. Lab., SRI Int., Menlo Park, CA, USA
fDate :
9/1/1998 12:00:00 AM
Abstract :
A specification language used in the context of an effective theorem prover can provide novel features that enhance precision and expressiveness. In particular, type checking for the language can exploit the services of the theorem prover. We describe a feature called “predicate subtyping” that uses this capability and illustrate its utility as mechanized in PVS
Keywords :
formal specification; specification languages; theorem proving; type theory; PVS; formal specifications; predicate subtyping; specification language; theorem prover; type checking; Computer languages; Java; Logic; Security; Set theory; Specification languages;
Journal_Title :
Software Engineering, IEEE Transactions on
