Abstract
This paper explains the details of the memory model underlying the verification of sequential Java programs in the “LOOP” project ([14,20]). The building blocks of this memory are cells, which are untyped in the sense that they can store the contents of the fields of an arbitrary Java object. The main memory is modeled as three infinite series of such cells, one for storing instance variables on a heap, one for local variables and parameters on a stack, and and one for static (or class) variables. Verification on the basis of this memory model is illustrated both in PVS and in Isabelle/HOL, via several examples of Java programs, involving various subtleties of the language (wrt. memory storage).
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
JavaCard API 2.1, http://java.sun.com/products/javacard/htmldoc/
Arnold, K., Gosling, J.: The Java Programming Language, 2nd edn. Addison-Wesley, Reading (1997)
Bergstra, J., Loots, M.: Empirical semantics for object-oriented programs. Artificial Intelligence Preprint Series nr. 007, Dep. Philosophy, Utrecht Univ. (1999)
Borger, E., Schulte, W.: Initialization problems in Java. Software—Concepts and Tools 20(4) (1999)
Goguen, J.A., Malcolm, G.: Algebraic Semantics of Imperative Programs. MIT Press, Cambridge (1996)
Gosling, J., Joy, B., Steele, G.: The Java Language Specification. Addison-Wesley, Reading (1996)
Griifioen, D., Huisman, M.: A comparison of PVS and Isabelle/HOL. In: Grundy, J., Newey, M. (eds.) TPHOLs 1998. LNCS, vol. 1479, pp. 123–142. Springer, Heidelberg (1998)
Huisman, M., Jacobs, B.: Inheritance in higher order logic: Modeling and reasoning. Techn. Rep. CSI-R0004, Comput. Sci. Inst., Univ. of Nijmegen (2000)
Huisman, M., Jacobs, B.: Java program verification via a Hoare logic with abrupt termination. In: Maibaum, T. (ed.) FASE 2000. LNCS, vol. 1783, pp. 284–303. Springer, Heidelberg (2000)
Huisman, M., Jacobs, B., van den Berg, J.: A case study in class library verification: Java’s Vector class. Techn. Rep. CSI-R0007, Comput. Sci. Inst., Univ. of Nijmegen. (An earlier version appeared in: Jacobs, B., Leavens, G.T., Miiller, P., Poetzsch-Heffter, A. (eds.), Formal Techniques for Java Programs. Proceedings of the ECOOP 1999 Workshop. Technical Report 251, Fernuniversitat Hagen (1999), pp. 37-44) (2000)
Jacobs, B.: Objects and classes, co-algebraically. In: Freitag, B., Jones, C.B., Lengauer, C., Schek, H.-J. (eds.) Object-Orientation with Parallelism and Persistence, pp. 83–103. Kluwer Acad. Publ., Dordrecht (1996)
Jacobs, B., Poll, E.: A monad forb asic Java semantics. In: Algebraic Methodology and Software Technology. Lecture Notes of Computer Science, Springer, Berlin (2000)
Jacobs, B., Rutten, J.: A tutorial on (co)algebras and (co)induction. EATCS Bulletin 62, 222–259 (1997)
Jacobs, B., van den Berg, J., Huisman, M., van Berkum, M., Hensel, U., Tews, H.: Reasoning about classes in Java (preliminary report). In: Object-Oriented Programming, Systems, Languages and Applications, pp. 329–340. ACM Press, New York (1998)
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
Owre, S., Rushby, J.M., Shankar, N., von Henke, F.: Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS. IEEE Trans. On Softw. Eng. 21(2), 107–125 (1995)
Paulson, L.C.: Isabelle: The next 700 theorem provers. In: Odifreddi, P. (ed.) Logic and computer science. The APIC series, vol. 31, pp. 361–386. Academic Press, London (1990)
Poetzsch-Heffter, A., Miiller, P.: A programming logic for sequential Java. In: Swierstra, S.D. (ed.) Programming Languages and Systems. LNCS, pp. 162–176. Springer, Berlin (1999)
Poll, E., van den Berg, J., Jacobs, B.: Specification of the JavaCard API in JML. Techn. Rep. CSI-R0005, Comput. Sci. Inst., Univ. of Nijmegen (2000)
Loop Project, http://www.cs.kun.nl/~bart/LOOP/
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
van den Berg, J., Huisman, M., Jacobs, B., Poll, E. (2000). A Type-Theoretic Memory Model for Verification of Sequential Java Programs. In: Bert, D., Choppy, C., Mosses, P.D. (eds) Recent Trends in Algebraic Development Techniques. WADT 1999. Lecture Notes in Computer Science, vol 1827. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-44616-3_1
Download citation
DOI: https://doi.org/10.1007/978-3-540-44616-3_1
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67898-4
Online ISBN: 978-3-540-44616-3
eBook Packages: Springer Book Archive