SUBTYPES FOR SPECIFICATIONS - PREDICATE SUBTYPING IN PVS

Authors
RUSHBY J OWRE S SHANKAR N
Citation
J. Rushby et al., SUBTYPES FOR SPECIFICATIONS - PREDICATE SUBTYPING IN PVS, IEEE transactions on software engineering, 24(9), 1998, pp. 709-720
Citations number
31
Categorie Soggetti
Computer Science Software Graphycs Programming","Engineering, Eletrical & Electronic","Computer Science Software Graphycs Programming
Journal title
IEEE transactions on software engineering → ACNP
ISSN journal
00985589
Volume
24
Issue
9
Year of publication
1998
Pages
709 - 720
Database
ISI
SICI code
0098-5589(1998)24:9<709:SFS-PS>2.0.ZU;2-9
Abstract
A specification language used in the context of an effective theorem p rover can provide novel features that enhance precision and expressive ness. in particular, typechecking for the language can exploit the ser vices of the theorem prover. We describe a feature called ''predicate subtyping'' that uses this capability and illustrate its utility as me chanized in PVS.