This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Subtypes for Specifications: Predicate Subtyping in PVS
September 1998 (vol. 24 no. 9)
pp. 709-720

Abstract—A specification language used in the context of an effective theorem prover can provide novel features that enhance precision and expressiveness. In particular, typechecking for the language can exploit the services of the theorem prover. We describe a feature called "predicate subtyping" that uses this capability and illustrate its utility as mechanized in PVS.

[1] L. Cardelli, "Type Systems," Handbook of Computer Science and Eng., ch. 103, pp. 2,208-2,236. CRC Press, 1997. available at urlhttp://www.research.digital.comSRC
[2] B. Russell, "Mathematical Logic as Based on the Theory of Types," From Frege to Gödel, J. van Heijenoort, ed., pp. 150-182.Cambridge, Mass.: Harvard Univ. Press, 1967. first published in 1908
[3] F.P. Ramsey, "The Foundations of Mathematics," Philosophical Papers of F.P. Ramsey, D.H. Mellor, ed., ch. 8, pp. 164-224.Cambridge, U.K.: Cambridge Univ. Press, 1990. originally published in Proc. London Math. Soc. vol. 25, pp. 338-384, 1925
[4] A. Church, "A Formulation of the Simple Theory of Types," J. Symbolic Logic, vol. 5, pp. 56-68, 1940.
[5] S. Owry, J. Rushby, and N. Shankar, "Integration in PVS: Tables, Types, and Model Checking," Tools and Algorithms for the Construction and Analysis of Systems, TACAS'97, Enschede: The Netherlands, 1997.
[6] S. Owre, J. Rushby, N. Shankar, and F. von Henke, "Formal Verification for Fault-Tolerant Architectures: Prolegomena to the Design of PVS," IEEE Trans. Software Eng., vol. 21, pp. 107-125, Feb. 1995.
[7] P. Rudnicki, "An Overview of the MIZAR Project," Proc. 1992 Workshop on Types for Proofs and Programs,Båstad, Sweden, pp. 311-330, June 1992. available at urlhttp://web.cs.ualberta.ca/piotr/MizarMizarOverview.ps
[8] C. B. Jones,Systematic Software Development Using VDM. Englewood Cliffs, NJ: Prentice-Hall, 1990, 2nd ed.
[9] R.L. Constable et al., Implementing Mathematics with the Nuprl Proof Development System.Englewood Cliffs, N.J.: Prentice Hall, 1986.
[10] O.-J. Dahl and O. Owe, "On the Use of Subtypes in ABEL (revised version)," Technical Report 206, Dept. of Informatics, Univ. of Oslo, Oct. 1995.
[11] The RAISE Language Group, The RAISE Specification Language. The BCS Practitioners Series, Prentice Hall, 1992.
[12] F.K. Hanna, N. Daeche, and M. Longley, "Specification and Verification Using Dependent Types," IEEE Trans. Software Eng., vol. 16, no. 9, pp. 949-964, Sept. 1989.
[13] D. C. Luckham, F. W. von Henke, B. Krieg-Brückner, and O. Owe,Anna—A Language for Annotating Ada Programs. Lecture Notes in Computer Science No. 260. New York: Springer-Verlag, 1987.
[14] S. Owre, S. Rajan, J.M. Rushby, N. Shankar, and M. Srivas, "PVS: Combining Specification, Proof Checking, and Model Checking," Alur and Henzinger [4], pp. 411-414.
[15] J. Rushby, "Automated Deduction and Formal Methods," Proc. Conf. Computer-Aided Verification (CAV'96). Lecture Notes in Computer Science 1,102, pp. 169-183, Springer-Verlag, July 1996.
[16] D. Cyrluk, P. Lincoln, and N. Shankar, "On Shostak's Decision Procedure for Combinations of Theories," Automated Deduction—CADE-13, M.A. McRobbie and J.K. Slaney, eds., New Brunswick, N.J., Lecture Notes in Artificial Intelligence 1,104, pp. 463-477. Springer-Verlag, July/Aug. 1996.
[17] H. Barringer, J.H. Cheng, and C.B. Jones, "A Logic Covering Undefinedness in Program Proofs," Acta Informatica, vol. 21, pp. 251-269, 1984.
[18] M.J. Beeson, Foundations of Constructive Mathematics, Ergebnisse der Mathematik und ihrer Grenzgebiete; 3. Folge Band 6. Springer-Verlag, 1985.
[19] D.L. Parnas, “Predicate Logic for Software Engineering,” IEEE Trans Software Eng., vol. 19, no. 9 pp. 856–862 Sept. 1993.
[20] W.M. Farmer, "A Partial Functions Version of Church's Simple Theory of Types," J. Symbolic Logic, vol. 55, no. 3, pp. 1,269-1,291, Sept. 1990.
[21] W.M. Farmer, J.D. Guttman, and F.J. Thayer, "IMPS: An Interactive Mathematical Proof System," J. Automated Reasoning, vol. 11, no. 2, pp. 213-248, 1993.
[22] L. Lamport and L.C. Paulson, "Should Your Specification Language Be Typed?" SRC Research Report 147, Digital Systems Research Center, Palo Alto, Calif., May 1997. available at urlhttp://www.research.digital.comSRC.
[23] J.H. Cheng and C.B. Jones, "On the Usability of Logics which Handle Partial Functions," Proc. Third Refinement Workshop, C. Morgan and J.C.P. Woodcock, eds., pp. 51-69, Springer-Verlag Workshops in Computing, 1990.
[24] S. Maharaj and J. Bicarregui, "On the Verification of VDM Specification and Refinement with PVS," Proc. 12th IEEE Int'l Conf. Automated Software Eng.: ASE'97, pp. 280-289,Incline Village, Nev., IEEE Computer Society, Nov. 1997.
[25] M. Saaltink, "The Z/EVES system," ZUM'97: The Z Formal Specification Notation; Proc. 10th Int'l Conf. of Z Users,Reading, U.K., Lecture Notes in Computer Science 1212, pp. 72-85. Springer-Verlag, Apr. 1997.
[26] M. Saaltink, "Domain Checking Z Specifications," LFM' 97: Fourth NASA Langley Formal Methods Workshop, C.M. Holloway and K.J. Hayhurst, eds., Hampton, Va., Sept. 1997, NASA Langley Research Center, NASA Conference Publication 3356, pp. 185-192. available at urlhttp://atb-www.larc.nasa.gov/Lfm97proceedings /
[27] S.M. German, "Automating Proofs of the Absence of Common Runtime Errors," Proc., Fifth ACM Symp. Principles of Programming Languages,Tucson, Ariz., pp. 105-118, Jan. 1978.
[28] D.L. Detlefs, "An Overview of the Extended Static Checking System," Proc. First Workshop Formal Methods in Software Practice, FMSP'96, pp. 1-9,San Diego, Calif., ACM, Jan. 1996.
[29] V. Breazu-Tannen, T. Coquand, C.A. Gunter, and A. Scedrov, "Inheritance as Implicit Coercion," Information and Computation, vol. 93, no. 1, pp. 172-221, July 1991.
[30] J. Rushby, "PVS Bibliography,"Menlo Park, Calif., constantly updated. available at urlhttp://www.csl.sri.compvs-bib.html.
[31] R. Alur and T.A. Henzinger, eds. Computer Aided Verification. Proc. Eighth Int'l Conf., CAV'96, Lecture Notes in Computer Science 1102.New Brunswick, N.J.: Springer-Verlag, July/Aug. 1996.

Index Terms:
Formal methods, specification languages, type systems, subtypes, typechecking, consistency, PVS.
Citation:
John Rushby, Sam Owre, Natarajan Shankar, "Subtypes for Specifications: Predicate Subtyping in PVS," IEEE Transactions on Software Engineering, vol. 24, no. 9, pp. 709-720, Sept. 1998, doi:10.1109/32.713327
Usage of this product signifies your acceptance of the Terms of Use.