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.

@inproceedings{Rushby97:FSE,
    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 = {http://www.csl.sri.com/papers/fse97/}
}

• fse97-slides.pdf
• fse97-slides.ps
• fse97.dvi
• fse97.pdf
• fse97.ps