SRI Logo
About Us|R and D Divisions|Careers|Newsroom|Contact Us|SRI Home
  SRI Logo

Subtypes for Specifications
 by Dr. John Rushby.

An enlarged journal version is also available.

Lecture Notes in Computer Science, Volume 1301.
From Software Engineering–ESEC/FSE '97: Sixth European Software Engineering Conference and Fifth ACM SIGSOFT Symposium on the Foundations of Software Engineering.
Edited by Mehdi Jazayeri and Helmut Schauer.
Springer-Verlag, Zurich, Switzerland.
September, 1997.
Pages 4–19.

Specification 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.
BibTEX Entry
    AUTHOR = {John Rushby},
    TITLE = {Subtypes for Specifications},
    BOOKTITLE = {Software Engineering--ESEC/FSE '97: Sixth European Software Engineering Conference and Fifth {ACM} {SIGSOFT} Symposium on the Foundations of Software Engineering},
    YEAR = {1997},
    EDITOR = {Mehdi Jazayeri and Helmut Schauer},
    SERIES = {Lecture Notes in Computer Science},
    VOLUME = {1301},
    PAGES = {4--19},
    ADDRESS = {Zurich, Switzerland},
    MONTH = {sep},
    PUBLISHER = {Springer-Verlag},
    URL = {}


About Us  |  R&D Divisions  |  Careers  |  Newsroom  |  Contact Us
© 2024 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy