Abstract
This paper describes a way of modeling inheritance (in object-oriented programming languages) in higher order logic. This particular approach is used in the LOOP project for reasoning about JAVA classes, with the proof tools PVS and ISABELLE. It relies on nested interface types to capture the superclasses, fields, methods, and constructors of classes, together with suitable casting functions incorporating the difference between hiding of fields and overriding of methods. This leads to the proper handling of late binding, as illustrated in several verification examples.
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
M. Abadi and L. Cardelli. A Theory of Objects. Monographs in Comp. Sci. Springer, 1996.
K. Arnold and J. Gosling. The Java Programming Language. Addison-Wesley, 1996.
J. van den Berg, M. Huisman, B. Jacobs, and E. Poll. A type-theoretic memory model for verification of sequential Java programs. Techn. Rep. CSI-R9924, Comput. Sci. Inst., Univ. of Nijmegen, 1999.
K.B. Bruce, L. Cardelli, and B. C. Pierce. Comparing object encodings. In M. Abadi and T. Ito, editors, Theoretical Aspects of Computer Software, number 1281 in Lect. Notes Comp. Sci., pages 415–438. Springer, Berlin, 1997.
L. Cardelli. A semantics of multiple inheritance. Inf. & Comp., 76(2/3):138–164, 1988.
W. Cook and J. Palsberg. A denotational semantics of inheritance and its correctness. Inf. & Comp., 114(2):329–350, 1995.
J. Gosling, B. Joy, and G. Steele. The Java Language Specification. Addison-Wesley, 1996.
M. Hofmann, W. Naraschewski, M. Steffen, and T. Stroup. Inheritance of proofs. Theory & Practice of Object Systems, 4(1):51–69, 1998.
M. Huisman. Reasoning about Java Programs in Higher-Order Logic, using PVS and Isabelle/HOL. PhD thesis, Univ. Nijmegen, 2000. Forthcoming.
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. (An earlier version appeared in: B. Jacobs, G.T. Leavens, P. Müller, and A. Poetzsch-Heffter (eds.), Formal Techniques for Java Programs. Proceedings of the ECOOP’99 Workshop. Technical Report 251, Fernuniversität Hagen, 1999, pages 37–44), 2000.
B. Jacobs. Inheritance and cofree constructions. In P. Cointe, editor, European Conference on Object-Oriented Programming, number 1098 in Lect. Notes Comp. Sci., pages 210–231. Springer, Berlin, 1996.
B. Jacobs. Objects and classes, co-algebraically. In B. Freitag, C.B. Jones, C. Lengauer, and H.-J. Schek, editors, Object-Orientation with Parallelism and Persistence, pages 83–103. Kluwer Acad. Publ., 1996.
B. Jacobs and J. Rutten. A tutorial on (co)algebras and (co)induction. EATCS Bulletin, 62:222–259, 1997.
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.
B. Meyer. Object-Oriented Software Construction. Prentice Hall, 2nd rev. edition, 1997.
J.C. Mitchell. Toward a typed foundation for method specialization and inheritance. In Principles of Programming Languages, pages 109–124. ACM Press, 1990.
W. Naraschewski and M. Wenzel. Object-oriented verification based on record subtyping in higher-order logic. In J. Grundy and M. Newey, editors, Theorem Proving in Higher Order Logics, number 1479 in Lect. Notes Comp. Sci., pages 349–366. Springer, Berlin, 1998.
S. Owre, J.M. Rushby, N. Shankar, and F. von Henke. Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS. IEEE Trans. on Softw. Eng., 21(2):107–125, 1995.
L.C. Paulson. Isabelle: The next 700 theorem provers. In P. Odifreddi, editor, Logic and computer science, pages 361–386. Academic Press, London, 1990. The APIC series, vol. 31.
B.C. Pierce and D.N. Turner. Simple type theoretic foundations for object-oriented programming. Journ. Funct. Progr., 4(2):207–247, 1994.
E. Poll, J. van den Berg, and B. Jacobs. Specification of the JavaCard API in JML. In Fourth Smart Card Research and Advanced Application Conference (CARDIS). Kluwer Acad. Publ., 2000, to appear. Available as Techn. Rep. CSI-R0005, Corn-put. Sci. Inst., Univ. of Nijmegen.
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
Huisman, M., Jacobs, B. (2000). Inheritance in Higher Order Logic: Modeling and Reasoning. In: Aagaard, M., Harrison, J. (eds) Theorem Proving in Higher Order Logics. TPHOLs 2000. Lecture Notes in Computer Science, vol 1869. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44659-1_19
Download citation
DOI: https://doi.org/10.1007/3-540-44659-1_19
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67863-2
Online ISBN: 978-3-540-44659-0
eBook Packages: Springer Book Archive