Subtypes for specifications: predicate subtyping in PVS

摘要

A specification language used in the context of an effectiventheorem prover can provide novel features that enhance precision andnexpressiveness. In particular, type checking for the language cannexploit the services of the theorem prover. We describe a feature calledn“predicate subtyping” that uses this capability andnillustrate its utility as mechanized in PVS