×

zbMATH — the first resource for mathematics

Specification and verification challenges for sequential object-oriented programs. (English) Zbl 1121.68074
Summary: The state of knowledge in how to specify sequential programs in object-oriented languages such as Java and C# and the state of the art in automated verification tools for such programs have made measurable progress in the last several years. This paper describes several remaining challenges and approaches to their solution.

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
68N19 Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Abrial J-R (1996) The B-Book: assigning programs to meanings. Cambridge University Press, Cambridge · Zbl 0915.68015
[2] Ambler AL, Good DI, Browne JC, Burger WF, Cohen RM, Hoch CG, Wells RE (1977) GYPSY: a language for specification and implementation of verifiable programs. SIGPLAN Notices 12(3):1–10. doi:10.1145/800022.808306 · doi:10.1145/390017.808306
[3] Abadi M, Leino KRM (1997) A logic of object-oriented programs. In: Bidoit M, Dauchet M (eds). Theory and practice of software development (TAPSOFT), Vol 1214 of Lecture Notes in Computer Science. Springer, Heidelberg, pp 682–696. http://www.springerlink.com/content/kp4n0b4xhn8rjg4p
[4] America P (1991) Designing an object-oriented programming language with behavioural subtyping. In: de Bakker JW, de Roever W-P, Rozenberg G (eds). Foundations of object-oriented languages. REX School/Workshop, Noordwijkerhout, The Netherlands, May/June 1990, Vol 489 of Lecture Notes in Computer Science. Springer, Heidelberg, pp 60–90. doi:10.1007/BFb0019440
[5] Apt KR (1981) Ten years of Hoare’s logic: a survey–part I. ACM Trans Program Lang Syst 3(4):431–483. doi: 10.1145/357146.357150 · Zbl 0471.68006 · doi:10.1145/357146.357150
[6] Ball T, Bounimova E, Cook B, Levin V, Lichtenberg J, McGarvey C, Ondrusek B, Rajamani SK, Ustuner A (2006) Thorough static analysis of device drivers. In: EuroSys’06. ACM, New York, pp 73–85. doi:10.1145/1217935.1217943
[7] Burdy L, Cheon Y, Cok DR, Ernst MD, Kiniry JR, Leavens GT, Leino KRM, Poll E (2005) An overview of JML tools and applications. Int J Softw Tools Technol Transf 7(3):212–232. doi:10.1007/s10009-004-0167-4 · doi:10.1007/s10009-004-0167-4
[8] Barnett M, Chang B-YE, DeLine R, Jacobs B, Leino KRM (2006) Boogie: a modular reusable verifier for object-oriented programs. In: Formal Methods for Components and Objects (FMCO) 2005, Revised Lectures, Vol 4111 of Lecture Notes in Computer Science. Springer, Heidelberg, pp 364–387. doi:10.1007/11804192_17
[9] Barnett M, DeLine R, Fähndrich M, Leino KRM, Schulte W (2004) Verification of object-oriented programs with invariants. J Object Technol 3(6):27–56. http://tinyurl.com/m2a8j · Zbl 05431131 · doi:10.5381/jot.2004.3.6.a2
[10] Beckert B (2000) A dynamic logic for Java Card. In: Drossopoulou S, Eisenbach S, Jacobs B, Leavens GT, Müller P, Poetzsch-Heffter A (eds) Workshop on formal techniques for Java Programs (FTfJP). Technical Report 269, FernUniversität Hagen
[11] Benton N (2005) A typed, compositional logic for a stack-based abstract machine. In: Yi K (eds). Programming languages and systems: third Asian symposium (APLAS), Vol 3780 of Lecture Notes in Computer Science. Springer, Heidelberg, pp 364–380. doi: 10.1007/11575467_24 · Zbl 1159.68362
[12] Barnett M, Leino KRM (2005) Weakest-precondition of unstructured programs. In: Ernst MD, Jensen TP (eds) Program analysis for software tools and engineering (PASTE). ACM, New York, pp 82–87. doi:10.1145/1108792.1108813
[13] Barnett M, Leino KRM, Schulte W (2005) The Spec# programming system: an overview. In: Barthe G, Burdy L, Huisman M, Lanet J-L, Muntean T (eds) Construction and analysis of safe, secure, and interoperable smart devices (CASSIS 2004), Vol 3362 of Lecture Notes in Computer Science. Springer, Heidelberg, pp 49–69. http://www.springerlink.com/content/0m789xre652nuv06
[14] Bannwart F, Müller P (2005) A logic for bytecode. In: Spoto F (eds). Bytecode semantics, verification, analysis and transformation (BYTECODE), Vol 141(1) of Electronic Notes in Theoretical Computer Science. Elsevier, Amsterdam, pp 255–273. doi: 10.1016/j.entcs.2005.02.026
[15] Borgida A, Mylopoulos J, Reiter R (1995) On the frame problem in procedure specifications. IEEE Trans Softw Eng 21(10):785–798. doi:10.1109/32.469460 · Zbl 05114555 · doi:10.1109/32.469460
[16] Barnett M, Naumann D (2004) Friends need a bit more: maintaining invariants over shared state. In: Kozen D (eds). Mathematics of program construction (MPC), Vol 3125 of Lecture Notes in Computer Science. Springer, Heidelberg, pp 54–84. http://www.springerlink.com/content/6gt28um7j5jgra12 · Zbl 1106.68338
[17] Boer FSd (1999) A WP-calculus for OO. In: Thomas W (eds). Foundations of software science and computation structures (FOSSACS), Vol 1578 of Lecture Notes in Computer Science. Springer, Heidelberg, pp 135–149. http://www.springerlink.com/content/ avdcmfyp8fxwk1y0
[18] Burdy L, Requet A, Lanet J-L (2003) Java applet correctness: a developer-oriented approach. In: Araki K, Gnesi S, Mandrioli D (eds) Formal methods (FME), Vol 2805 of Lecture Notes in Computer Science. Springer, Heidelberg, pp 422–439. http://www. springerlink.com/content/wje4yrg7mm7k4u88
[19] Beckert B, Sasse B (2001) Handling Java’s abrupt termination in a sequent calculus for Dynamic Logic. In: Beckert B, France R, Hähnle R, Jacobs B (eds) IJCAR Workshop on Precise Modelling and Deduction for Object-oriented Software Development, pp 5–14
[20] Büchi M (2000) Safe language mechanisms for modularization and concurrency. Technical Report TUCS Dissertations No. 28, Turku Center for Computer Science, May 2000
[21] Back R-J, von Wright J (1998) Refinement calculus: a systematic introduction. graduate texts in computer science. Springer, Heidelberg
[22] Broy M, Wirsing M (1982) Partial abstract types. Acta Informatica 18(1):47–64. doi:10.1007/BF00625280 · Zbl 0494.68020 · doi:10.1007/BF00625280
[23] Büchi M, Weck W (1999) The greybox approach: when blackbox specifications hide too much. Technical Report 297, Turku Center for Computer Science, August 1999. http://tinyurl.com/ywmuzy.
[24] Clarke DG, Drossopoulou S (2002) Ownership, encapsulation and the disjointness of type and effect. In: Object-oriented programming systems, languages, and applications (OOPSLA), Vol 37(11) of SIGPLAN Notices. ACM, New York, pp 292–310. doi:10.1145/582419.582447
[25] Chapman R (2000) Industrial experience with SPARK. ACM SIGADA Ada Lett 20(4):64–68. doi:10.1145/369264.369270 · doi:10.1145/369264.369270
[26] Chalin P (2003) Improving JML: For a safer and more effective language. In: Araki K, Gnesi S, Mandrioli D (eds) Formal methods (FME), Vol 2805 of Lecture Notes in Computer Science. Springer, Heidelberg, pp 440–461. http://www.springerlink.com/content/26cpmd9b3vbgd2et
[27] Charles J (2006) Adding native specifications to JML. In: Workshop on formal techniques for Java-like Programs (FTfJP), July 2006. http://www.disi.unige.it/person/AnconaD/FTfJP06/paper04.pdf
[28] Cheon Y (2003) A runtime assertion checker for the Java Modeling Language. PhD dissertation, Technical Report 03-09, Department of Computer Science, Iowa State University, April 2003. ftp://ftp.cs.iastate.edu/pub/techreports/TR03-09/TR.pdf
[29] Cheon Y, Hayashi Y, Leavens GT (2004) A thought on specification reflection. In: Callaos N, Lesso W, Sanchez B (eds) The 8th World multi-conference on systemics, cybernetics and informatics (SCI), Vol II, Computing Techniques, pp 485–490
[30] Cok DR, Kiniry JR (2005) ESC/Java2: Uniting ESC/Java and JML: progress and issues in building and using ESC/Java2, including a case study involving the use of the tool to verify portions of an Internet voting tally system. In: Barthe G, Burdy L, Huisman M, Lanet J-L, Muntean T (eds) Construction and analysis of safe, secure, and interoperable smart devices (CASSIS 2004), Vol 3362 of Lecture Notes in Computer Science. Springer, Heidelberg, pp 108–128. http://www.springerlink.com/content/mbxr4yj1dj0lj6ap
[31] Cook B, Kroening D, Sharygina N (2005) Cogent: accurate theorem proving for program verification. In: Etessami K, Rajamani SK (eds) Computer aided verification (CAV), Vol 3576 of Lecture Notes in Computer Science. Springer, Heidelberg, pp 296–300. doi:10.1007/11513988_30 · Zbl 1081.68673
[32] Cheon Y, Leavens GT, Sitaraman M, Edwards S (2005) Model variables: cleanly supporting abstraction in design by contract. Softw Pract Exp 35(6):583–599. doi: 10.1002/spe.649 · doi:10.1002/spe.649
[33] Calcagno C, O’Hearn P, Bornat R (2003) Program logic and equivalence in the presence of garbage collection. Theor Comput Sci 298(2):557–581. doi:10.1016/S0304-3975(02)00868-X · Zbl 1038.68011 · doi:10.1016/S0304-3975(02)00868-X
[34] Cohen E (1990) Programming in the 1990s: an introduction to the calculation of programs. Springer, Heidelberg · Zbl 0825.68262
[35] Cok DR (2005) Reasoning with specifications containing method calls and model fields. J Object Technol 4(8):77–103. http://www.jot.fm/issues/issue_2005_10/article4 · Zbl 05431197 · doi:10.5381/jot.2005.4.8.a4
[36] Clarke DG, Potter JM, Noble J (1998) Ownership types for flexible alias protection. In: Object-oriented programming systems, languages, and applications (OOPSLA), Vol 33(10) of SIGPLAN Notices. ACM, New York, pp 48–64. doi:http://doi.acm.org/10.1145/286936.286947
[37] Cook B, Podelski A, Rybalchenko A (2006) Termination proofs for systems code. In: Schwartzbach MI, Ball T (eds) Proceedings of the ACM SIGPLAN 2006 conference on programming language design and implementation (PLDI). ACM, New York, pp 415–426. doi:http://doi.acm.org/10.1145/1133981.1134029
[38] Cristian F (1984) Correct and robust programs. IEEE Trans Softw Eng 10:163–174 · Zbl 0532.68021 · doi:10.1109/TSE.1984.5010218
[39] Dhara KK, Leavens GT (1996) Forcing behavioral subtyping through specification inheritance. In: Proceedings of the 18th international conference on software engineering, March 1996, Berlin. IEEE Computer Society Press, New York, pp 258–267. A corrected version is ISU CS TR #95-20c, http://tinyurl.com/s2krg. doi:10.1109/ICSE.1996.493421
[40] DeLine R, Leino KRM (2005) Boogie PL: aA typed procedural language for checking object-oriented programs. Technical Report MSR-TR-2005-70, Microsoft Research. ftp://ftp.research.microsoft.com/pub/tr/TR-2005-70.pdf
[41] Darvas A, Müller P (2006) Reasoning about method calls in interface specifications. J Object Technol 5(5):59–85. http://www.jot.fm/issues/issue_2006_06/article3.pdf · Zbl 05431203 · doi:10.5381/jot.2006.5.5.a3
[42] Detlefs D, Nelson G, Saxe JB (2005) Simplify: a theorem prover for program checking. J ACM 52(3):365–473. http://doi.acm.org/10.1145/1066100.1066102 · Zbl 1323.68462 · doi:10.1145/1066100.1066102
[43] Ernst M, Cockrell J, Griswold WG, Notkin D (2001) Dynamically discovering likely program invariants to support program evolution. IEEE Trans Softw Eng 27(2):99–123.doi:10.1109/32.908957 · doi:10.1109/32.908957
[44] C# language specification. ECMA Standard 334, June 2005
[45] Eiffel analysis, design and programming language. ECMA Standard 367, June 2005
[46] Ehrig H, Mahr B (1985) Fundamentals of algebraic specification 1: equations and initial semantics, Vol 6 of EATCS Monographs on Theoretical Computer Science. Springer, Heidelberg · Zbl 0557.68013
[47] Feijs LMG, Jonkers HBM (1992) Formal specification and design, Vol 35 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge · Zbl 0774.68082
[48] Flanagan C, Leino KRM (2001) Houdini, an annotation assistant for ESC/Java. In: Oliveira JN, Zave P (eds) FME 2001: formal methods for increasing software productivity, Vol 2021 of Lecture Notes in Computer Science. Springer, Heidelberg, pp 500–517. http://www.springerlink.com/content/nxukfdgg7623q3a9
[49] Flanagan C, Leino KRM, Lillibridge M, Nelson G, Saxe JB, Stata R (2002) Extended static checking for Java. In: Proceedings of the 2002 ACM SIGPLAN conference on programming language design and implementation (PLDI), Vol 37(5) of SIGPLAN Notices. ACM, New York, pp 234–245. doi:10.1145/512529.512558
[50] Filliâtre J-C, Marché C (2004) Multi-prover verification of C programs. In: Formal methods and software engineering, 6th international conference on formal engineering methods, ICFEM 2004, Vol 3308 of Lecture Notes in Computer Science. Springer, Heidelberg, pp 15–29. http://www.springerlink.com/content/ejxv14xdjf5676u5
[51] Greenhouse A, Boyland J (1999) An object-oriented effects system. In: European conference on object-oriented programming (ECOOP). Springer, Heidelberg, pp 205–229. http://www.springerlink.com/content/tu309p114v1kbd8v
[52] Guttag JV, Horning JJ (1978) The algebraic specification of abstract data types. Acta Informatica 10(1):27–52. doi:10.1007/BF00260922 · Zbl 0379.68020 · doi:10.1007/BF00260922
[53] Guttag JV, Horning JJ (1993) Larch: languages and tools for formal specification. Springer, Heidelberg · Zbl 0794.68103
[54] Gamma E, Helm R, Johnson R, Vlissides J (1995) Design patterns. Addison-Wesley, Reading · Zbl 0887.68013
[55] Greenhouse A (2003) A programmer-oriented approach to safe concurrency. Technical Report CMU-CS-03-135, School of Computer Science, Carnegie Mellon University, May 2003. http://reports-archive.adm.cs.cmu.edu/anon/2003/CMU-CS-03-135.pdf
[56] Gries D (1981) The science of programming. Springer, Heidelberg · Zbl 0472.68003
[57] Gries D, Schneider FB (1994) A logical approach to discrete math. texts and monographs in computer science. Springer, Heidelberg
[58] Goguen JA, Thatcher JW, Wagner EG, Wright JB (1977) Initial algebra semantics and continuous algebras. J ACM 24:68–95. doi:10.1145/321992.321997 · Zbl 0359.68018 · doi:10.1145/321992.321997
[59] Hehner ECR (1993) A practical theory of programming. texts and monographs in computer science. Springer, Heidelberg. Available from http://www.cs.utoronto.ca/ hehner/aPToP
[60] Hehner ECR (2005) Specified blocks. Verified Software: Theories, Tools, Experiments (VSTTE), http://vstte.inf.ethz.ch/Files/ hehner.pdf, October 2005
[61] Huisman M, Jacobs B (2000) Java program verification via a Hoare logic with abrupt termination. In: Fundamental approaches to software engineering (FASE). Springer, Heidelberg, pp 284–303. http://www.springerlink.com/content/fkrbjn1vg56ra052
[62] Hudak P, Jones SP, Wadler P, Boutel B, Fairbairn J, Fasel J, Guzmán MM, Hammond K, Hughes J, Johnsson T, Kieburtz D, Nikhil R, Partain W, Peterson J (1992) Report on the programming language Haskell: a non-strict, purely functional language, version 1.2. ACM SIGPLAN Notices 27(5). doi:10.1145/130697.130699
[63] Hoare T, Misra J, Shankar N (2005) Verified software: theories, tools, experiments (VSTTE 2005). http://vstte.ethz.ch, October 2005. Sponsored by International Federation for Information Processing, Technical Committee 2
[64] Hoare CAR (1969) An axiomatic basis for computer programming. Commun ACM 12(10):576–580,583. doi:10.1145/363235.363259 · Zbl 0179.23105
[65] Hoare CAR (1972) Proof of correctness of data representations. Acta Informatica 1(4):271–281. doi:10.1007/BF00289507 · Zbl 0244.68009 · doi:10.1007/BF00289507
[66] Hoare T (2003) The verifying compiler: a grand challenge for computing research. J ACM 50(1):63–69. doi:10.1145/602382.602403 · Zbl 1032.68868 · doi:10.1145/602382.602403
[67] Jacobs B (2004) Weakest pre-condition reasoning for Java programs with JML annotations. J Logic Algebraic Program 58(1–2):61–88. doi:10.1016/j.jlap.2003.07.005 · Zbl 1073.68024 · doi:10.1016/j.jlap.2003.07.005
[68] Jacobs B, Kiniry J, Warnier M (2003) Java program verification challenges. In: de Boer FS, Bonsangue MM, Graf S, de Roever W-P (eds) FMCO 2002: formal methods for component objects, proceedings, Vol 2852 of Lecture Notes in Computer Science. Springer, Heidelberg, pp 202–219
[69] Jacobs B, Meijer E, Piessens F, Schulte W (2005) Iterators revisited: proof rules and implementation. In: Workshop on formal techniques for Java-like Programs (FTfJP), July 2005. http://www.cs.ru.nl/ftfjp/2005/Jacobs.pdf
[70] Jones CB (1990) Systematic software development using VDM International series in computer science, 2nd edn. Prentice Hall, Englewood Cliffs
[71] Jones KD (1991) LM3: A larch interface language for Modula-3: a definition and introduction: Version 1.0. Technical Report 72, Digital Equipment Corporation, Systems Research Center
[72] Jacobs B, Poll E (2001) A logic for the Java modeling language JML. In: Fundamental approaches to software engineering (FASE), Vol 2029 of Lecture Notes in Computer Science. Springer, Heidelberg, pp 284–299. http://www.springerlink.com/content/17ul9mb1y0ja42eb · Zbl 0977.68588
[73] Jacobs B, Piessens F (2006) Verification of programs with inspector methods. In: Workshop on Formal Techniques for Java-like Programs (FTfJP), July 2006. http://www.disi.unige.it/person/AnconaD/FTfJP06/paper09.pdf
[74] Katrib M, Coira J (1997) Improving Eiffel assertions using quantified iterators. J Object-Oriented Program 10(7):35–43
[75] Kramer R (1998) iContract–the Java TM design by contract TM tool. In: TOOLS 26: technology of object-oriented languages and systems, August 1998. IEEE Computer Society Press, New York, pp 295–307. doi:10.1109/TOOLS.1998.711021
[76] Leavens GT, Baker AL, Ruby C (1999) JML: a notation for detailed design. In: Kilov H, Rumpe B, Simmonds I (eds) Behavioral Specifications of businesses and systems. Kluwer, Dordrecht, pp 175–188
[77] Leavens GT, Baker AL, Ruby C (2006) Preliminary design of JML: a behavioral interface specification language for Java. ACM SIGSOFT Softw Eng Notes 31(3):1–38. doi:10.1145/1127878.1127884 · doi:10.1145/1127878.1127884
[78] Leavens GT, Cheon Y, Clifton C, Ruby C, Cok DR (2005) How the design of JML accommodates both runtime assertion checking and formal verification. Sci Comput Program 55(1–3):185–208. doi:10.1016/j.scico.2004.05.015 · Zbl 1075.68009 · doi:10.1016/j.scico.2004.05.015
[79] Leavens GT, Dhara KK (2000) Concepts of behavioral subtyping and a sketch of their extension to component-based systems. In: Leavens GT, Sitaraman M (eds) Foundations of component-based systems, Chap 6. Cambridge University Press, Cambridge, pp 113–135. http://www.cs.iastate.edu/ leavens/FoCBS-book/06-leavens-dhara.pdf
[80] Leavens GT (2006) JML’s rich, inherited specifications for behavioral subtypes. In: Liu Z, Jifeng H (eds) Formal methods and software engineering: 8th international conference on formal engineering methods (ICFEM), Vol 4260 of Lecture Notes in Computer Science, New York. Springer, Heidelberg, pp 2–34. doi:10.1007/11901433_2
[81] Leino KRM (1995) Toward reliable modular programs. PhD Thesis, California Institute of Technology. Available as Technical Report Caltech-CS-TR-95-03. http://caltechcstr.library.caltech.edu/234/00/95-03.ps
[82] Leino KRM (1997) Ecstatic: an object-oriented programming language with an axiomatic semantics. In: Pierce B (ed) Fourth international workshop on foundations of object-oriented languages (FOOL), January 1997. Available from: http://www.cis.upenn.edu/ bcpierce/FOOL/
[83] Leino KRM (1998) Data groups: specifying the modification of extended state. In: Object-oriented programming systems, languages, and applications (OOPSLA), Vol 33(10) of SIGPLAN Notices. ACM, New York, pp 144–153. doi:10.1145/286936.286953
[84] Leino KRM, Müller P (2004) Object invariants in dynamic contexts. In: Odersky M (ed) European conference on object- oriented programming (ECOOP), Vol 3086 of Lecture Notes in Computer Science, June 2004. Springer, Heidelberg, pp 491–516. http://www.springerlink.com/content/ttfnjg36yq64pah8
[85] Leino KRM, Müller P (2005) Modular verification of static class invariants. In: Fitzgerald J, Hayes IJ, Tarlecki A (eds) Formal methods (FM), Vol 3582 of Lecture Notes in Computer Science, July 2005. Springer, Heidelberg, pp 26–42. doi:10.1007/11526841_4
[86] Leino KRM, Müller P (2006) A verification methodology for model fields. In: Sestoft P (ed) European symposium on programming (ESOP), Vol 3924 of Lecture Notes in Computer Science, March 2006. Springer, Heidelberg, pp 115–130. doi:10.1007/11693024_9
[87] Leino KRM, Nelson G (2002) Data abstraction and information hiding. ACM Trans Programm Lang Syst 24(5):491–553. doi:10.1145/570886.570888 · Zbl 05459296 · doi:10.1145/570886.570888
[88] Leavens GT, Naumann DA (2006) Behavioral subtyping, specification inheritance, and modular reasoning. Technical Report 06-20a, Department of Computer Science, Iowa State University, Ames, August 2006. ftp://ftp.cs.iastate.edu/pub/techreports/TR06-20/TR.pdf
[89] Leavens GT, Poll E, Clifton C, Cheon Y, Ruby C, Cok DR, Müller P, Kiniry J, Chalin P (2006) JML reference manual. Department of Computer Science, Iowa State University. Available from http://www.jmlspecs.org, January 2006
[90] Leino KRM, Poetzsch-Heffter A, Zhou Y (2002) Using data groups to specify and check side effects. In: Proceedings of the 2002 ACM SIGPLAN conference on programming language design and implementation (PLDI), Vol 37(5) of SIGPLAN Notices, May 2002. ACM, New York, pp 246–257. doi:10.1145/512529.512559
[91] Leino KRM, Saxe JB, Stata R (1999) Checking Java programs via guarded commands. In: Jacobs B, Leavens GT, Müller P, Poetzsch-Heffter A (eds) Formal techniques for Java Programs (FTfJP), Technical Report 251. FernUniversität Hagen, May 1999. Also available as Technical Note 1999-002, Compaq Systems Research Center
[92] Luckham D (1990) Programming with specifications: an introduction to Anna, a language for specifying Ada programs. Texts and Monographs in Computer Science. Springer, Heidelberg · Zbl 0729.68007
[93] Luckham D, von Henke FW (1985) An overview of Anna–a specification language for Ada. IEEE Softw 2(2):9–23 · Zbl 05335104 · doi:10.1109/MS.1985.230345
[94] Liskov B, Wing JM (1994) A behavioral notion of subtyping. ACM Trans Program Lang Syst 16(6):1811–1841. doi:10.1145/197320.197383 · doi:10.1145/197320.197383
[95] Leavens GT, Weihl WE (1995) Specification and verification of object-oriented programs using supertype abstraction. Acta Informatica 32(8):705–778. doi:10.1007/BF01178658 · Zbl 0831.68009
[96] Meyer B (1992) Eiffel: the language. Prentice Hall, New Jersey · Zbl 0779.68013
[97] Meyer B (1997) Object-oriented software construction, 2nd edn. Prentice Hall, New Jersey · Zbl 0987.68516
[98] Miragliotta M (2004) Specification model library for the interactive program prover Jive. Student project, ETH Zurich. Available from: http://www.sct.inf.ethz.ch/projects/student_docs/Marcello_Miragliotta/M arcello_Miragliotta_paper.pdf
[99] Morgan C (1994) Programming from specifications, 2nd edn. Prentice Hall International, Hempstead, http://web.comlab.ox.ac.uk/oucl/publications/books/PfS/ · Zbl 0829.68083
[100] Müller P, Poetzsch-Heffter A, Leavens GT (2003) Modular specification of frame properties in JML. Concurr Comput Pract Exp 15(2):117–154. doi:10.1002/cpe.713 · Zbl 1005.68583 · doi:10.1002/cpe.713
[101] Müller P, Poetzsch-Heffter A, Leavens GT (2006) Modular invariants for layered object structures. Sci Comput Program 62(3):253–286. doi:10.1016/j.scico.2006.03.001 · Zbl 1100.68539 · doi:10.1016/j.scico.2006.03.001
[102] Marché C, Paulin-Mohring C, Urbain X (2004) The Krakatoa tool for certification of Java/JavaCard programs annotated in JML. J Logic Algebraic Programm 58(1–2):89–106. doi:10.1016/j.jlap.2003.07.006 · Zbl 1073.68678 · doi:10.1016/j.jlap.2003.07.006
[103] Müller P (2002) Modular specification and verification of object-oriented programs, Vol 2262 of Lecture Notes in Computer Science. Springer, Heidelberg · Zbl 0998.68034
[104] Nimmer JW, Ernst MD (2001) Static verification of dynamically detected program invariants: integrating Daikon and ESC/Java. In: Proceedings of RV’01, first workshop on runtime verification, July 2001. Elsevier, Amsterdam. doi:10.1016/S1571-0661(04)00256-7
[105] O’Hearn PW, Yang H, Reynolds JC (2004) Separation and information hiding. In: Jones ND, Leroy X (eds) Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on principles of programming languages (POPL), January 2004. ACM, New York, pp 268–280. doi:10.1145/964001.964024
[106] Parkinson M, Bierman G (2005) Separation logic and abstraction. In: Palsberg J, Abadi M (eds) Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on principles of programming languages (POPL), January 2005. ACM, New York, pp 247–258. doi:10.1145/1040305.1040326 · Zbl 1369.68151
[107] Poetzsch-Heffter A, Müller P (1999) A programming logic for sequential Java. In: Swierstra SD (ed) European symposium on programming languages and systems (ESOP), Vol 1576 of Lecture Notes in Computer Science. Springer, Heidelberg, pp 162–176. http://tinyurl.com/krjle
[108] Reynolds JC (2002) Separation logic: a logic for shared mutable data structures. In: IEEE symposium on logic in computer science. IEEE, New York, pp 55–74
[109] Rosenblum DS (1995) A practical approach to programming with assertions. IEEE Trans Softw Eng 21(1):19–31. doi:10.1109/32.341844 · Zbl 05113210 · doi:10.1109/32.341844
[110] Soundarajan N, Fridella S (2004) Incremental reasoning for object oriented systems. In: Owe O, Krogdahl S, Lyche T (eds) From object-orientation to formal methods, essays in memory of Ole–Johan Dahl, Vol 2635 of Lecture Notes in Computer Science. Springer, Heidelberg, pp 302–333. http://www.springerlink.com/content/n9uv7k2bha03l9ln
[111] Shaner S (2006) Semantics for model programs in JML. Master’s Thesis, Iowa State University (expected)
[112] Spivey JM (1992) The Z notation: a reference manual. international series in computer science, 2nd edn. Prentice-Hall, New York. http://spivey.oriel.ox.ac.uk/mike/zrm/
[113] von Oheimb D (2001) Analyzing Java in Isabelle/HOL: formalization, type safety and Hoare logic. PhD Thesis, Technische Universität München. http://www4.in.tum.de/ oheimb/diss/ · Zbl 0997.68019
[114] von Oheimb D, Nipkow T (2002) Hoare logic for NanoJava: auxiliary variables, side effects and virtual methods revisited. In: Eriksson L-H, Lindsay PA (eds) Formal methods–getting IT Right (FME’02), Vol 2391 of Lecture Notes in Computer Science. Springer, Heidelberg, pp 89–105. http://www.springerlink.com/content/bp1vtfr9ha3kl3t5 · Zbl 1064.68543
[115] von Praun C, Gross TR (2003) Static conflict analysis for multi-threaded object-oriented programs. In: Proceedings of the ACM SIGPLAN 2003 conference on programming language design and implementation (PLDI), June 2003. ACM, New York, pp 115–128. doi:10.1145/781131.781145
[116] Wand M (1979) Final algebra semantics and data type extensions. J Comput Syst Sci 19(1):27–44. doi:10.1016/0022-0000(79)90011-4 · Zbl 0418.68020 · doi:10.1016/0022-0000(79)90011-4
[117] Wahls T, Baker AL, Leavens GT (1994) The direct execution of SPECS-C++: a model-based specification language for C++ classes. Technical Report 94-02b, Department of Computer Science, Iowa State University, March 1994. ftp://ftp.cs.iastate.edu/pub/ techreports/TR94-02/TR.ps.Z
[118] Wills A (1992) Specification in Fresco. In: Stepney S, Barden R, Cooper D (eds) Object orientation in Z, workshops in computing, Chap 11. Springer, Heidelberg, pp 127–135
[119] Wing JM (1987) Writing larch interface language specifications. ACM Trans Program Lang Syst 9(1):1–24. doi:10.1145/9758.10500 · Zbl 0627.68014 · doi:10.1145/9758.10500
[120] Wing JM (1990) A specifier’s introduction to formal methods. Computer 23(9):8–24. doi:10.1109/2.58215 · Zbl 05090280 · doi:10.1109/2.58215
[121] Wilson T, Maharaj S, Clark RG (2005) Omnibus verification policies: a flexible, configurable approach to assertion-based software verification. In: Aichernig BK, Beckert B (eds) Third IEEE international conference on software engineering and formal methods (SEFM), September 2005. IEEE Comput Soc, New York, pp 150–159. doi:10.1109/SEFM.2005.29
[122] Xie Y, Aiken A (2005) Scalable error detection using boolean satisfiability. In: Palsberg J, Abadi M (eds) Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on principles of programming languages (POPL), January 2005. ACM, New York, pp 351–363. doi:10.1145/1040305.1040334 · Zbl 1369.68162
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.