Abstract
This paper aims to raise the level of verification challenges by presenting a collection of sequential Java programs with correctness annotations formulated in JML. The emphasis lies more on the underlying semantical issues than on verification.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Ábraham Mumm, E., de Boer, F.S., de Roever, W.-P., Steffen, M.: A Tool-supported Proof System for Multithreaded Java. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2002. LNCS, vol. 2852, pp. 1–32. Springer, Heidelberg (2003)
Ahrendt, W., Baar, T., Beckert, B., Bubel, R., Giese, M., Hähnle, R., Menzel, W., Mostowski, W., Roth, A., Schlager, S., Schmitt, P.H.: The KeY tool. Technical Report 2003-5, Chalmers and Göteborg University (2003), http://i12www.ira.uka.de/~key
van den Berg, J., Jacobs, B.: The LOOP compiler for Java and JML. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 299–312. Springer, Heidelberg (2001)
Bergstra, J., Loots, M.: Empirical semantics for object-oriented programs. Artificial Intelligence Preprint Series nr. 007, Dep. Philosophy, Utrecht Univ. (1999), http://preprints.phil.uu.nl/aips/
Börger, E., Schulte, W.: Initialization problems in Java. Software—Concepts and Tools 20(4) (1999)
Burdy, L., Lanet, J.-L., Requet, A.: JACK (Java Applet Correctness Kit) (2002), http://www.gemplus.com/smart/r_d/trends/jack.html
Chalin, P.: Back to basics: Language support and semantics of basic infinite integer types in JML and Larch. Technical Report, 003.1, Computer Science Department, Concordia University (2002), http://www.cs.concordia.ca/~faculty/chalin/
Chalin, P.: Improving JML: For a safer and more effective language. Technical Report 2003-001.1, Computer Science Department, Concordia University (March 2003)
Cheon, Y., Leavens, G.T.: A runtime assertion checker for the Java Modeling Language (JML). In: Arabnia, H.R., Mun, Y. (eds.) International Conference on Software Engineering Research and Practice (SERP 2002), pp. 322–328. CSREA Press, Las Vegas (2002)
Contejean, E., Duprat, J., Filliâtre, J.-C., Marché, C., Paulin-Mohring, C., Urbain, X.: The Krakatoa tool for JML/Java program certification (October 2002), Available via the Krakatoa home page at http://www.lri.fr/~marche/krakatoa/
Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)
Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). SIGPLAN Notices, vol. 37(5), pp. 234–245. ACM, New York (2002)
Gosling, J., Joy, B., Steele, G., Bracha, G.: The Java Language Specification, 2nd edn. The Java Series. Addison-Wesley, Reading (2000), http://java.sun.com/docs/books/jls/second_edition/html/j.title.doc.html
Gries, D.: The Science of Programming. Springer, Heidelberg (1981)
Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12, 576–580, 583 (1969)
Huisman, M., Jacobs, B.: Inheritance in higher order logic: Modeling and reasoning. In: Aagaard, M.D., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol. 1869, pp. 301–319. Springer, Heidelberg (2000)
Jacobs, B.: A formalisation of Java’s exception mechanism. In: Sands, D. (ed.) ESOP 2001. LNCS, vol. 2028, pp. 284–301. Springer, Heidelberg (2001)
Jacobs, B.: Java’s integral types in PVS (2003) (manuscript), http://www.cs.kun.nl/~bart/PAPERS/
Leavens, G.T., Baker, A.L., Ruby, C.: JML: A notation for detailed design. In: Kilov, H., Rumpe, B. (eds.) Behavioral Specifications of Business and Systems, pp. 175–188. Kluwer, Dordrecht (1999)
Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: A behavioral interface specification language for Java. Techn. Rep. 98-06, Dep. of Comp. Sci., Iowa State Univ. (1999), http://www.cs.iastate.edu/~leavens/JML.html
Leavens, G.T., Poll, E., Clifton, C., Cheon, Y., Ruby, C.: JML reference manual, draft (2002), http://www.jmlspecs.org
Liskov, B., Wing, J.M.: A behavioral notion of subtyping. ACM Trans. on Prog. Lang. & Syst. 7(16(6), 1811–1841 (1994)
Meyer, J., Poetzsch-Heffter, A.: An architecture for interactive program provers. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol. 1785, pp. 63–77. Springer, Heidelberg (2000)
Poll, E., van den Berg, J., Jacobs, B.: Specification of the JavaCard API in JML. In: Domingo-Ferrer, J., Chan, D., Watson, A. (eds.) Smart Card Research and Advanced Application, pp. 135–154. Kluwer Acad. Publ., Dordrecht (2000)
Szyperski, C.: Component Software. Addison-Wesley, Reading (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Jacobs, B., Kiniry, J., Warnier, M. (2003). Java Program Verification Challenges. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, WP. (eds) Formal Methods for Components and Objects. FMCO 2002. Lecture Notes in Computer Science, vol 2852. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-39656-7_8
Download citation
DOI: https://doi.org/10.1007/978-3-540-39656-7_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20303-2
Online ISBN: 978-3-540-39656-7
eBook Packages: Springer Book Archive