×

zbMATH — the first resource for mathematics

An assertion-based proof system for multithreaded Java. (English) Zbl 1070.68016
Summary: Besides the features of a class-based object-oriented language, Java integrates concurrency via its thread classes, allowing for a multithreaded flow of control. The concurrency model includes synchronous message passing, dynamic thread creation, shared-variable concurrency via instance variables, and coordination via reentrant synchronization monitors.
To reason about safety properties of multithreaded Java programs, we introduce an assertional proof method for a multithreaded sublanguage of Java, covering the mentioned concurrency issues as well as the object-based core of Java. The verification method is formulated in terms of proof-outlines, where the assertions are layered into local ones specifying the behavior of a single instance, and global ones taking care of the connections between objects. We establish the soundness and the relative completeness of the proof system. From an annotated program, a number of verification conditions are generated and handed over to the interactive theorem prover PVS.

MSC:
68N15 Theory of programming languages
Software:
JML; PVS
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Abadi, M.; Cardelli, L., A theory of objects monographs in computer science, (1996), Springer Berlin
[2] M. Abadi, K.R.M. Leino, A logic of object-oriented programs, in: M. Bidoit, M. Dauchet (Eds.), Proc. TAPSOFT ’97, Lecture Notes in Computer Science, Vol. 1214, Springer, Lille, France, 1997, pp. 682-696. An extended version of this paper appeared as SRC Research Report 161 (September, 1998).
[3] E. Ábrahám, An assertional proof system for multithreaded Java—theory and tool support, Ph.D. Thesis, University of Leiden, to appear. A preliminary version can be found at \(\sim\), 2004.
[4] E. Ábrahám, F.S. de Boer, W.-P. de Roever, M. Steffen, A Hoare logic for monitors in Java, Technical Report TR-ST-03-1, Lehrstuhl für Software-Technologie, Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität zu Kiel, April, 2003, URL \(<\)>.
[5] E. Ábrahám, F.S. de Boer, W.-P. de Roever, M. Steffen, A compositional operational semantics for Java\({}_{\mathit{MT}}\), in: N. Derschowitz (Ed.), International Symposium on Verification (Theory and Practice), Lecture Notes in Computer Science, Vol. 2772, Springer, Berlin, 2003, pp. 290-303. A preliminary version appeared as Technical Report TR-ST-02-2, May 2002.
[6] E. Ábrahám, F.S. de Boer, W.-P. de Roever, M. Steffen, Inductive proof outlines for multithreaded Java with exceptions, Technical Report 0313, Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität zu Kiel, December, 2003. URL \(<\)>. · Zbl 1253.68080
[7] E. Ábrahám-Mumm, F.S. de Boer, Proof-outlines for threads in Java, in: C. Palamidessi (Ed.), Proc. CONCUR’00, Lecture Notes in Computer Science, Vol. 1877, Springer-Berlin, 2000, pp. 229-242. · Zbl 0999.68504
[8] E. Ábrahám-Mumm, F.S. de Boer, W.-P. de Roever, M. Steffen, Verification for Java’s reentrant multithreading concept, in: M. Nielsen, U.H. Engberg (Eds.), Proc. FoSSaCS’02, Lecture Notes in Computer Science, Vol. 2303, Springer, Berlin, 2002, pp. 4-20. A longer version, including the proofs for soundness and completeness, appeared as Technical Report TR-ST-02-1, March 2002. · Zbl 1077.68552
[9] E. Ábrahám, F.S. de Boer, W.-P. de Roever, M. Steffen, Inductive proof-outlines for monitors in Java, in: E. Najm, U. Nestmann, P. Stevens (Eds.), Proc. 6th IFIP Internat. Conf. Formal Methods for Open Object-Based Distributed Systems (FMOODS’03), Paris, Lecture Notes in Computer Science, Vol. 2884, Springer, Berlin, 2003, pp. 155-169. A longer version appeared as technical report TR-ST-03-1, April 2003 \(<\)http://www.informatik.uni-kiel.de/inf/deRoever/techreports/03/tr-st-03-1.pdf>.
[10] E. Ábrahám-Mumm, F.S. de Boer, W.-P. de Roever, M. Steffen, A tool-supported proof system for monitors in Java, in: M. Bonsangue, F.S. de Boer, W.-P. de Roever, S. Graf (Eds.), Proc. First Internat. Symp. Formal Methods for Components and Objects (FMCO’02), Leiden, Lecture Notes in Computer Science, Vol. 2852, Springer, Berlin, 2003, pp. 1-32.
[11] J. Alves-Foss (Ed.), Formal Syntax and Semantics of Java, Lecture Notes in Computer Science State-of-the-Art-Survey, Vol. 1523, Springer, Berlin, 1999.
[12] P. America, A behavioural approach to subtyping in object-oriented programming languages, 443, Phillips Research Laboratories, January/April 1989. · Zbl 0681.68010
[13] P. America, F.S. de Boer, A sound and complete proof system for SPOOL, Technical Report 505, Philips Research Laboratories, 1990.
[14] Andrews, G.R., Foundations of multithreaded parallel and distributed programming, (2000), Addison-Wesley Reading, MA
[15] Apt, K.R.; Francez, N.; deRoever, W.-P., A proof system for communicating sequential processes, ACM trans. programming languages systems, 2, 359-385, (1980) · Zbl 0468.68023
[16] D. Basin, S. Friedrich, M. Gawkowski, Verified bytecode model checkers, in: V.A. Carreño, C.A. Muñoz, S. Tahar (Eds.), Proc. TPHOLs’02, Lecture Notes in Computer Science, Vol. 2410, Springer, Berlin, 2002, pp. 47-66. · Zbl 1013.68544
[17] Buhr, P.A.; Fortier, M.; Coffin, M.H., Monitor classification, ACM comput. surveys, 27, 1, 63-107, (1995)
[18] P. Cenciarelli, A. Knapp, B. Reus, M. Wirsing, An event-based structural operational semantics of multi-threaded Java, in: J. Alves-Foss (Ed.), Formal Syntax and Semantics of Java, Lecture Notes in Computer Science State-of-the-Art-Survey, Vol. 1523, Springer, Berlin, 1999, pp. 157-200.
[19] F.S. de Boer, A WP-calculus for OO, in: W. Thomas (Ed.), Proc. FoSSaCS’99, Lecture Notes in Computer Science, Vol. 1578, Springer, Berlin, 1999, pp. 135-156.
[20] F.S. de Boer, C. Pierik, Computer-aided specification and verification of annotated object-oriented programs, in: B. Jacobs, A. Rensink (Eds.), Proc. FMOODS’02, Vol. 209, Kluwer, Dordrecht, 2002, pp. 163-177. · Zbl 1048.68050
[21] F.S. de Boer, C. Pierik, Towards an environment for the verification of annotated object-oriented programs, Technical report UU-CS-2003-002, Institute of Information and Computing Sciences, University of Utrecht, January 2003.
[22] C.C. de Figueiredo, A proof system for a sequential object-oriented language, Technical Report UMCS-95-1-1, University of Manchester, 1995.
[23] R.W. Floyd, Assigning meanings to programs, in: J.T. Schwartz (Ed.), Proc. Symp. Appl. Math. Vol. 19, 1967, pp. 19-32. · Zbl 0189.50204
[24] Gosling, J.; Joy, B.; Steele, G.L., The Java language specification, (1996), Addison-Wesley Reading, MA · Zbl 0865.68001
[25] Hartel, P.H.; Moreau, L., Formalizing the safety of Java, The Java virtual machine and Java card, ACM comput. surveys, 33, 4, 517-558, (2001)
[26] Hoare, C.A.R., An axiomatic basis for computer programming, Comm. ACM, 12, 576-580, (1969) · Zbl 0179.23105
[27] M. Huisman, Java program verification in higher-order logic with PVS and Isabelle, Ph.D. Thesis, University of Nijmegen, 2001.
[28] B. Jacobs, J. Kiniry, M. Warnier, Java program verification challenges, in: M. Bonsangue, F.S. de Boer, W.-P. de Roever, S. Graf (Eds.), Proc. First Internat. Symp. Formal Methods for Components and Objects (FMCO’02), Leiden, Lecture Notes in Computer Science, Vol. 2852, Springer, Berlin, 2003, pp. 202-220.
[29] B. Jacobs, J. van den Berg, M. Huisman, M. van Barkum, U. Hensel, H. Tews, Reasoning about classes in Java (preliminary report), in: Proc. OOPSLA’98, ACM, 1998, pp. 329-340 (in SIGPLAN Not. 30(10)).
[30] G.T. Leavens, A.L. Baker, C. Ruby, Preliminary design of JML: a behavioral interface specification language for Java, Technical Report TR #98-06f, Iowa State University. Revised version from July 1999, 2000.
[31] G.T. Leavens, Y. Cheon, C. Clifton, C. Ruby, D.R. Cok, How the design of JML accommodates both runtime assertion, checking and formal verification, in: M. Bonsangue, F.S. de Boer, W.-P. de Roever, S. Graf (Eds.), Proc. First Internat. Symp. Formal Methods for Components and Objects (FMCO’02), Leiden, Lecture Notes in Computer Science, Vol. 2852, Springer, Berlin, 2003, pp. 262-284. · Zbl 1075.68009
[32] G.T. Leavens, W.E. Wheil, Reasoning about object-oriented programs that use subtypes, in: Proc. OOPSLA’90, ACM, 1990, pp. 212-223, extended abstract.
[33] G.T. Leavens, W.E. Wheil, Specification and verification of object-oriented programs using supertype abstraction, Acta Inform. 32 (8) (1995) 705-778. An expanded version appeared as Iowa State University Report, 92-28d. · Zbl 0831.68009
[34] X. Leroy, Java bytecode verification: an overview, in: G. Berry, H. Comon, A. Finkel (Eds.), Proc. CAV’01, Lecture Notes in Computer Science, Vol. 2102, Springer, Berlin, 2001, pp. 265-285. · Zbl 0996.68591
[35] Levin, G.; Gries, D., A proof technique for communicating sequential processes, Acta inform., 15, 3, 281-302, (1981) · Zbl 0463.68034
[36] Owicki, S.; Gries, D., An axiomatic proof technique for parallel programs, Acta inform., 6, 4, 319-340, (1976) · Zbl 0312.68011
[37] S. Owre, J.M. Rushby, N. Shankar, PVS: a prototype verification system, in: D. Kapur (Ed.), Automated Deduction (CADE-11), Lecture Notes in Computer Science, Vol. 607, Springer, Berlin, 1992, pp. 748-752.
[38] A. Poetzsch-Heffter, Specification and verification of object-oriented programs, Technische Universität München, Habilitationsschrift, 1997.
[39] A. Poetzsch-Heffter, A logic for the verification of object-oriented programs, in: R. Berghammer, F. Simon (Eds.), Proc. Programming Languages and Fundamentals of Programming, Bericht Nr. 9717, Institut für Informatik und Praktische Mathematik, Christian-Albrechts-Universität zu Kiel, 1997, pp. 31-42.
[40] A. Poetzsch-Heffter, P. Müller, Logical foundations for typed object-oriented languages, in: D. Gries, W.-P. de Roever (Eds.), Proc. PROCOMET ’98, International Federation for Information Processing (IFIP), Chapman & Hall, London, 1998, pp. 404-423.
[41] A. Poetzsch-Heffter, P. Müller, A programming logic for sequential Java, in: S. Swierstra (Ed.), Proc. ESOP’99, Lecture Notes in Computer Science, Vol. 1576, Springer, Berlin, 1999, pp. 162-176.
[42] C. Pierik, F.S. de Boer, A syntax-directed Hoare logic for object-oriented programming concepts, in: E. Najm, U. Nestmann, P. Stevens (Eds.), Proc. 6th IFIP Internat. Conf. Formal Methods for Open Object-Based Distributed Systems (FMOODS’03), Paris, Lecture Notes in Computer Science, Vol. 2884, Springer, Berlin, 2003, pp. 64-78. An extended version appeared as University of Utrecht Technical Report UU-CS-2003-010. · Zbl 1253.68087
[43] B. Reus, R. Hennicker, M. Wirsing, A Hoare calculus for verifying Java realizations of OCL-constrained design models, in: H. Hussmann (Ed.), Fundamental Approaches to Software Engineering, Lecture Notes in Computer Science, Vol. 2029, Springer, Berlin, 2001, pp. 300-316. · Zbl 0977.68858
[44] B. Reus, M. Wirsing, A Hoare-logic for object-oriented programs, Technical report, LMU München, 2000.
[45] Stärk, R.; Schmid, J.; Börger, E., Java and the Java virtual machinedefinition, verification, validation, (2001), Springer Berlin · Zbl 0978.68033
[46] F. Tang, M. Hofmann, Generation of verification conditions for Abadi and Leino’s logic of objects (extended abstract), in: Proc. FOOL’02, 2002, A longer version is available as LFCS Technical Report.
[47] The LOOP project: formal methods for object-oriented systems, 2001, \(<\) >.
[48] J.V. Tucker, J.I. Zucker, Program Correctness over Abstract Data Types, with Error-State Semantics, CWI Monograph Series, Vol. 6, North-Holland, Amsterdam, 1988. · Zbl 0641.68028
[49] von Oheimb, D., Hoare logic for Java in isabelle/HOL, Concurrency comput.practice experience, 13, 13, 1173-1214, (2001) · Zbl 0997.68019
[50] D. von Oheimb, T. Nipkow, Hoare logic for NanoJava: auxiliary variables, side effects and virtual methods revisited, in: L.-H. Eriksson, P. A. Lindsay (Eds.), Proc. FME’02, Lecture Notes in Computer Science, Vol. 2391, Springer, Berlin, 2002, pp. 89-105. · Zbl 1064.68543
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.