Subtypes for Specifications

John Rushby

Computer Science Laboratory, SRI International

Menlo Park, CA 94025, USA

Abstract

Specfication languages are best used in environments that provide effective theorem proving. Having such support available, it is feasible to contemplate that typechecking can use the services of the theorem prover. This allows interesting extensions to the type systems provided for specification languages. I describe one such extension called "predicate subtyping" and illustrate its utility as mechanized in PVS.