
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
John Rushby, Sam Owre, Natarajan Shankar, "Subtypes for Specifications: Predicate Subtyping in PVS," IEEE Transactions on Software Engineering, vol. 24, no. 9, pp. 709720, September, 1998.  
BibTex  x  
@article{ 10.1109/32.713327, author = {John Rushby and Sam Owre and Natarajan Shankar}, title = {Subtypes for Specifications: Predicate Subtyping in PVS}, journal ={IEEE Transactions on Software Engineering}, volume = {24}, number = {9}, issn = {00985589}, year = {1998}, pages = {709720}, doi = {http://doi.ieeecomputersociety.org/10.1109/32.713327}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Software Engineering TI  Subtypes for Specifications: Predicate Subtyping in PVS IS  9 SN  00985589 SP709 EP720 EPD  709720 A1  John Rushby, A1  Sam Owre, A1  Natarajan Shankar, PY  1998 KW  Formal methods KW  specification languages KW  type systems KW  subtypes KW  typechecking KW  consistency KW  PVS. VL  24 JA  IEEE Transactions on Software Engineering ER   
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,2082,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. 150182.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. 164224.Cambridge, U.K.: Cambridge Univ. Press, 1990. originally published in Proc. London Math. Soc. vol. 25, pp. 338384, 1925
[4] A. Church, "A Formulation of the Simple Theory of Types," J. Symbolic Logic, vol. 5, pp. 5668, 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 FaultTolerant Architectures: Prolegomena to the Design of PVS," IEEE Trans. Software Eng., vol. 21, pp. 107125, Feb. 1995.
[7] P. Rudnicki, "An Overview of the MIZAR Project," Proc. 1992 Workshop on Types for Proofs and Programs,Båstad, Sweden, pp. 311330, June 1992. available at urlhttp://web.cs.ualberta.ca/piotr/MizarMizarOverview.ps
[8] C. B. Jones,Systematic Software Development Using VDM. Englewood Cliffs, NJ: PrenticeHall, 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. 949964, Sept. 1989.
[13] D. C. Luckham, F. W. von Henke, B. KriegBrückner, and O. Owe,Anna—A Language for Annotating Ada Programs. Lecture Notes in Computer Science No. 260. New York: SpringerVerlag, 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. 411414.
[15] J. Rushby, "Automated Deduction and Formal Methods," Proc. Conf. ComputerAided Verification (CAV'96). Lecture Notes in Computer Science 1,102, pp. 169183, SpringerVerlag, July 1996.
[16] D. Cyrluk, P. Lincoln, and N. Shankar, "On Shostak's Decision Procedure for Combinations of Theories," Automated Deduction—CADE13, M.A. McRobbie and J.K. Slaney, eds., New Brunswick, N.J., Lecture Notes in Artificial Intelligence 1,104, pp. 463477. SpringerVerlag, 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. 251269, 1984.
[18] M.J. Beeson, Foundations of Constructive Mathematics, Ergebnisse der Mathematik und ihrer Grenzgebiete; 3. Folge Band 6. SpringerVerlag, 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,2691,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. 213248, 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. 5169, SpringerVerlag 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. 280289,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. 7285. SpringerVerlag, 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. 185192. available at urlhttp://atbwww.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. 105118, 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. 19,San Diego, Calif., ACM, Jan. 1996.
[29] V. BreazuTannen, T. Coquand, C.A. Gunter, and A. Scedrov, "Inheritance as Implicit Coercion," Information and Computation, vol. 93, no. 1, pp. 172221, July 1991.
[30] J. Rushby, "PVS Bibliography,"Menlo Park, Calif., constantly updated. available at urlhttp://www.csl.sri.compvsbib.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.: SpringerVerlag, July/Aug. 1996.