Abstract
This paper describes a specialised logic for proving specifications in the Java Modeling Language (JML). JML is an interface specification language for Java. It allows assertions like invariants, constraints, pre- and post-conditions, and modifiable clauses as annotations to Java classes, in a design-by-contract style. Within the LOOP project at the University of Nijmegen JML is used for specification and verification of Java programs. A special compiler has been developed which translates Java classes together with their JML annotations into logical theories for a theorem prover (PVS or Isabelle). The logic for JML that will be described here consists of tailor-made proof rules in the higher order logic of the back-end theorem prover for verifying translated JML specifications. The rules efficiently combine partial and total correctness (like in Hoare logic) for all possible termination modes in Java, in a single correctness formula.
Chapter PDF
Similar content being viewed by others
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.
References
JavaCard API 2.1. http://java.sun.com/products/javacard/htmldoc/.
P. America. Designing an object-oriented language with behavioural subtyping. In J.W. de Bakker, W.P. de Roever, and G. Rozenberg, editors, Foundations of Object-Oriented Languages, number 489 in Lect. Notes Comp. Sci., pages 60–90. Springer, Berlin, 1990.
K.R. Apt. Ten years of Hoare’s logic: A survey—part I. ACM Trans. on Progr. Lang. and Systems, 3(4):431–483, 1981.
J. van den Berg, M. Huisman, B. Jacobs, and E. Poll. A type-theoretic memory model for verification of sequential Java programs. In D. Bert, C. Choppy, and P. Mosses, editors, Recent Trends in Algebraic Development Techniques, number 1827 in Lect. Notes Comp. Sci., pages 1–21. Springer, Berlin, 2000.
J. van den Berg and B. Jacobs. The LOOP compiler for Java and JML. Techn. Rep. CSI-R0019, Comput. Sci. Inst., Univ. of Nijmegen. To appear at TACAS’01., 2000.
A. Bhorkar. A run-time assertion checker for Java using JML. Techn. Rep. 00-08, Dep. of Comp. Science, Iowa State Univ. http://www.cs.iastate.edu/~leavens/JML.html, 2000.
F.S. de Boer. A WP-calculus for OO. In W. Thomas, editor, Foundations of Software Science and Computation Structures, number 1578 in Lect. Notes Comp. Sci., pages 135–149. Springer, Berlin, 1999.
M. Huisman. Reasoning about JAVA Programs in higher order logic with PVS and Isabelle. PhD thesis, Univ. Nijmegen, 2001.
M. Huisman and B. Jacobs. Inheritance in higher order logic: Modeling and reasoning. In M. Aagaard and J. Harrison, editors, Theorem Proving in Higher Order Logics, number 1869 in Lect. Notes Comp. Sci., pages 301–319. Springer, Berlin, 2000.
M. Huisman and B. Jacobs. Java program verification via a Hoare logic with abrupt termination. In T. Maibaum, editor, Fundamental Approaches to Software Engineering, number 1783 in Lect. Notes Comp. Sci., pages 284–303. Springer, Berlin, 2000.
M. Huisman, B. Jacobs, and J. van den Berg. A case study in class library verification: Java’s Vector class. Techn. Rep. CSI-R0007, Comput. Sci. Inst., Univ. of Nijmegen. To appear in Software Tools for Technology Transfer, 2001.
B. Jacobs. A formalisation of Java’s exception mechanism. Techn. Rep. CSI-R0015, Comput. Sci. Inst., Univ. of Nijmegen. To appear at ESOP’01., 2000.
B. Jacobs, J. van den Berg, M. Huisman, M. van Berkum, U. Hensel, and H. Tews. Reasoning about classes in Java (preliminary report). In Object-Oriented Programming, Systems, Languages and Applications (OOPSLA), pages 329–340. ACM Press, 1998.
G.T. Leavens, A.L. Baker, and C. Ruby. JML: A notation for detailed design. In H. Kilov and B. Rumpe, editors, Behavioral Specifications of Business and Systems, pages 175–188. Kluwer, 1999.
G.T. Leavens, A.L. Baker, and C. Ruby. Preliminary design of JML: A behavioral interface specification language for Java. Techn. Rep. 98-06, Dep. of Comp. Sci., Iowa State Univ. http://www.cs.iastate.edu/~leavens/JML.html, 1999.
K.R.M. Leino. Toward Reliable Modular Programs. PhD thesis, California Inst. of Techn., 1995.
K.R.M. Leino, J.B. Saxe, and R. Stata. Checking java programs via guarded commands. In B. Jacobs, G. T. Leavens, P. Muller, and A. Poetzsch-Heffter, editors, Formal Techniques for Java Programs. Proceedings of the ECOOP’99 Workshop. Techn. Rep. 251, Fernuniversitat Hagen, 1999. Also as Technical Note 1999-002, Compaq Systems Research Center, Palo Alto.
B. Meyer. Object-Oriented Software Construction. Prentice Hall, 2nd rev. edition, 1997.
D. von Oheimb. Axiomatic semantics for Javalight in Isabelle/HOL. Technical Report CSE 00-009, Oregon Graduate Inst., 2000. TPHOLS 2000 Supplemental Proceedings.
S. Owre, S. Rajan, J.M. Rushby, N. Shankar, and M. Srivas. PVS: Combining specification, proof checking, and model checking. In R. Alur and T.A. Henzinger, editors, Computer Aided Verification, number 1102 in Lect. Notes Comp. Sci., pages 411–414. Springer, Berlin, 1996.
L.C. Paulson. Isabelle: A Generic Theorem Prover. Number 828 in Lect. Notes Comp. Sci. Springer, Berlin, 1994.
A. Poetzsch-He-ter and P. Muller. A programming logic for sequential Java. In S.D. Swierstra, editor, Programming Languages and Systems, number 1576 in Lect. Notes Comp. Sci., pages 162–176. Springer, Berlin, 1999.
E. Poll. A coalgebraic semantics of subtyping. In H. Reichel, editor, Coalgebraic Methods in Computer Science, number 33 in Elect. Notes in Theor. Comp. Sci. Elsevier, Amsterdam, 2000.
E. Poll, J. van den Berg, and B. Jacobs. Specification of the JavaCard API in JML. In J. Domingo-Ferrer, D. Chan, and A. Watson, editors, Smart Card Research and Advanced Application, pages 135–154. Kluwer Acad. Publ., 2000.
E. Poll, J. van den Berg, and B. Jacobs. Formal specification of the JavaCard API in JML: the APDU class. Comp. Networks Mag., 2001. To appear.
Loop Project. http://www.cs.kun.nl/~bart/LOOP/.
Extended static checker ESC/Java. Compaq System Research Center. http://www.research.digital.com/SRC/esc/Esc.html.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Jacobs, B., Poll, E. (2001). A Logic for the Java Modeling Language JML. In: Hussmann, H. (eds) Fundamental Approaches to Software Engineering. FASE 2001. Lecture Notes in Computer Science, vol 2029. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45314-8_21
Download citation
DOI: https://doi.org/10.1007/3-540-45314-8_21
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41863-4
Online ISBN: 978-3-540-45314-7
eBook Packages: Springer Book Archive