Abstract
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.
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
This work was supported by the Air Force Office of Scientific Research, Air Force Materiel Command, USAF, under contract F49620-95-CO044 and by the National Science Foundation under contract CCR-9509931.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
Rajeev Alur and Thomas A. Henzinger, editors. Computer-Aided Verification, CAV '96, volume 1102 of Lecture Notes in Computer Science, New Brunswick, NJ, July/August 1996. Springer-Verlag.
Luca Cardelli. Type systems. In Handbook of Computer Science and Engineering, chapter 103, pages 2208–2236. CRC Press, 1997. Available at http: //www.research.digital.com/SRC.
J. H. Cheng and C. B. Jones. On the usability of logics which handle partial functions. In Carroll Morgan and J. C. P. Woodcock, editors, Proceedings of the Third Refinement Workshop, pages 51–69. Springer-Verlag Workshops in Computing, 1990.
A. Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5:56–68, 1940.
R. L. Constable, S. F. Allen, H. M. Bromley, W. R. Cleaveland, J. F. Cremer, R. W. Harper, D. J. Howe, T. B. Knoblock, N. P. Mendler, P. Panangaden, J. T. Sasaki, and S. F. Smith. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, Englewood Cliffs, NJ, 1986.
David L. Detlefs. An overview of the Extended Static Checking system. In First Workshop on Formal Methods in Software Practice (FMSP '96), pages 1–9, San Diego, CA, January 1996. Association for Computing Machinery.
Richard A. Kemmerer. Verification assessment study final report. Technical Report C3-CR01-86, National Computer Security Center, Ft. Meade, MD, 1986. 5 Volumes (Overview, Gypsy, Affirm, FDM, and EHDM). US distribution only.
Leslie Lamport and Lawrence C. Paulson. Should your specification language be typed? SRC Research Report 147, Digital Systems Research Center, Palo Alto, CA, May 1997. Available at http://www.research.digital.com/SRC.
David C. Luckham, Friedrich W. von Henke, Bernd Krieg-Brückner, and Olaf Owe. ANNA: A Language for Annotating Ada Programs, volume 260 of Lecture Notes in Computer Science. Springer-Verlag, 1987.
S. Owre, S. Rajan, J.M. Rushby, N. Shankar, and M.K. Srivas. PVS: Combining specification, proof checking, and model checking. In Alur and Henzinger [1], pages 411–414.
Sam Owre, John Rushby, and N. Shankar. Integration in PVS: Tables, types, and model checking. In Ed Brinksma, editor, Tools and Algorithms for the Construction and Analysis of Systems (TACAS '97), volume 1217 of Lecture Notes in Computer Science, pages 366–383, Enschede, The Netherlands, April 1997. Springer-Verlag.
Sam Owre, John Rushby, Natarajan Shankar, and Friedrich von Henke. Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS. IEEE Transactions on Software Engineering, 21(2):107–125, February 1995.
F. P. Ramsey. The foundations of mathematics. In D. H. Mellor, editor, Philosophical Papers of F. P. Ramsey, chapter 8, pages 164–224. Cambridge University Press, Cambridge, UK, 1990. Originally published in Proceedings of the London Mathematical Society, 25, pp. 338–384, 1925.
John Rushby. Automated deduction and formal methods. In Alur and Henzinger
Bertrand Russell. Mathematical logic as based on the theory of types. In Jean van Heijenoort, editor, From Frege to Gödel, pages 150–182. Harvard University Press, Cambridge, MA, 1967. First published 1908.
Mark Saaltink. The Z/EVES system. In ZUM '97: The Z Formal Specification Notation; 10th International Conference of Z Users, volume 1212 of Lecture Notes in Computer Science, pages 72–85, Reading, UK, April 1997. Springer-Verlag.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Rushby, J. (1997). Subtypes for specifications. In: Jazayeri, M., Schauer, H. (eds) Software Engineering — ESEC/FSE'97. ESEC SIGSOFT FSE 1997 1997. Lecture Notes in Computer Science, vol 1301. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63531-9_2
Download citation
DOI: https://doi.org/10.1007/3-540-63531-9_2
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63531-4
Online ISBN: 978-3-540-69592-9
eBook Packages: Springer Book Archive