×

zbMATH — the first resource for mathematics

Incremental reasoning with lazy behavioral subtyping for multiple inheritance. (English) Zbl 1221.68058
Summary: Object-orientation supports code reuse and incremental programming. Multiple inheritance increases the possibilities for code reuse, but complicates the binding of method calls and thereby program analysis. Behavioral subtyping allows program analysis under an open world assumption; i.e., under the assumption that class hierarchies are extensible. However, method redefinition is severely restricted by behavioral subtyping, and multiple inheritance may lead to conflicting restrictions from independently designed superclasses.
This paper presents a more liberal approach to incremental reasoning for multiple inheritance under an open world assumption. The approach, based on lazy behavioral subtyping, is well-suited for multiple inheritance, as it incrementally imposes context-dependent behavioral constraints on new subclasses. We first present the approach for a simple language and show how incremental reasoning can be combined with flexible code reuse. Then this language is extended with a hierarchy of interface types which is independent of the class hierarchy. In this setting, flexible code reuse can be combined with modular reasoning about external calls in the sense that each class is analyzed only once. We formalize the approach as a calculus and show soundness for both languages.

MSC:
68N19 Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] America, P.: Designing an object-oriented programming language with behavioural subtyping, Foundations of object-oriented languages, 60-90 (1991)
[2] America, P.; Van Der Linden, F.: A parallel object-oriented language with inheritance and subtyping, Proceedings of the conference on object-oriented programming systems, languages, and applications, OOPSLA, vol. 25(10) 25, 161-168 (1990)
[3] Apt, K. R.: Ten years of Hoare’s logic: A survey–part i, ACM transactions on programming languages and systems 3, No. 4, 431-483 (1981) · Zbl 0471.68006
[4] Apt, K. R.; De Boer, F. S.; Olderog, E. -R.: Verification of sequential and concurrent systems, (2009) · Zbl 1183.68361
[5] Attali, I.; Caromel, D.; Ehmety, S. O.: A natural semantics for eiffel dynamic binding, ACM transactions on programming languages and systems 18, No. 6, 711-729 (1996)
[6] Booch, G.; Rumbaugh, J.; Jacobson, I.: The unified modeling language user guide, (1999)
[7] Bracha, G.; Cook, W.: Mixin-based inheritance, Proceedings of the conference on object-oriented programming: systems, languages, and applications/European conference on object-oriented programming, 303-311 (1990)
[8] Burdy, L.; Cheon, Y.; Cok, D. R.; Ernst, M. D.; Kiniry, J. R.; Leavens, G. T.; Leino, K. R. M.; Poll, E.: An overview of JML tools and applications, International journal on software tools for technology transfer 7, No. 3, 212-232 (2005)
[9] Cardelli, L.: A semantics of multiple inheritance, Information and computation 76, No. 2–3, 138-164 (1988) · Zbl 0651.68017
[10] Chambers, C.; Ungar, D.; Chang, B. -W.; Hölzle, U.: Parents are shared parts of objects: inheritance and encapsulation in SELF, Lisp and symbolic computation 4, No. 3, 207-222 (1991)
[11] Chin, W. -N.; David, C.; Nguyen, H. H.; Qin, S.: Enhancing modular oo verification with separation logic, , 87-99 (2008) · Zbl 1295.68082
[12] De Boer, F. S.: A WP-calculus for OO, Lecture notes in computer science 1578, 135-149 (1999)
[13] Demichiel, L. G.; Gabriel, R. P.: The common lisp object system: an overview, Lecture notes in computer science 276, 151-170 (1987)
[14] Dovland, J.; Johnsen, E. B.; Owe, O.: Observable behavior of dynamic systems: component reasoning for concurrent objects, Electronic notes in theoretical computer science 203, No. 3, 19-34 (2008) · Zbl 1277.68056
[15] Dovland, J.; Johnsen, E. B.; Owe, O.; Steffen, M.: Lazy behavioral subtyping, Lecture notes in computer science 5014, 52-67 (2008) · Zbl 1204.68072
[16] Dovland, J.; Johnsen, E. B.; Owe, O.; Steffen, M.: Incremental reasoning for multiple inheritance, Lecture notes in computer science 5423, 215-230 (2009) · Zbl 1211.68084
[17] Dovland, J.; Johnsen, E. B.; Owe, O.; Steffen, M.: Lazy behavioral subtyping, Journal of logic and algebraic programming 79, No. 7, 578-607 (2010) · Zbl 1204.68072
[18] Fournet, C.; Laneve, C.; Maranget, L.; Rémy, D.: Inheritance in the join calculus, Journal of logic and algebraic programming 57, No. 1–2, 23-69 (2003) · Zbl 1035.03011
[19] Hoare, C. A. R.: An axiomatic basis of computer programming, Communications of the ACM 12, 576-580 (1969) · Zbl 0179.23105
[20] Hoare, C. A. R.: Procedures and parameters: an axiomatic approach, Lecture notes in mathematics 188, 102-116 (1971) · Zbl 0221.68020
[21] Igarashi, A.; Pierce, B. C.; Wadler, P.: Featherweight Java: a minimal core calculus for Java and GJ, ACM transactions on programming languages and systems 23, No. 3, 396-450 (2001)
[22] Johnsen, E. B.; Owe, O.: A dynamic binding strategy for multiple inheritance and asynchronously communicating objects, Lecture notes in computer science 3657, 274-295 (2005) · Zbl 1143.68356
[23] Johnsen, E. B.; Owe, O.; Yu, I. C.: Creol: A type-safe object-oriented model for distributed concurrent systems, Theoretical computer science 365, No. 1–2, 23-66 (2006) · Zbl 1118.68031
[24] Krogdahl, S.: Multiple inheritance in simula-like languages, Bit 25, No. 2, 318-326 (1985) · Zbl 0566.68005
[25] G.T. Leavens, D.A. Naumann, Behavioral subtyping, specification inheritance, and modular reasoning, Technical Report 06-20a, Department of Computer Science, Iowa State University, Ames, Iowa, 2006.
[26] X. Leroy, D. Doligez, J. Garrigue, D. Rémy, J. Vouillon, The Objective Caml system (release 3.11). Documentation and user’s manual, Institut National de Recherche en Informatique et en Automatique, 2008.
[27] Liskov, B. H.; Wing, J. M.: A behavioral notion of subtyping, ACM transactions on programming languages and systems 16, No. 6, 1811-1841 (1994)
[28] Luo, C.; Qin, S.: Separation logic for multiple inheritance, Electronic notes in theoretical computer science 212, 27-40 (2008) · Zbl 1286.68320
[29] Meyer, B.: Object-oriented software construction, (1997) · Zbl 0987.68516
[30] Nystrom, N.; Chong, S.; Meyers, A. C.: Scalable extensibility via nested inheritance, (2004)
[31] Odersky, M.; Spoon, L.; Venners, B.: Programming in scala, (2008)
[32] Owicki, S.; Gries, D.: An axiomatic proof technique for parallel programs I, Acta informatica 6, No. 4, 319-340 (1976) · Zbl 0312.68011
[33] Parkinson, M. J.; Biermann, G. M.: Separation logic, abstraction and inheritance, , 75-86 (2008) · Zbl 1295.68091
[34] Pierik, C.; De Boer, F. S.: A proof outline logic for object-oriented programming, Theoretical computer science 343, No. 3, 413-442 (2005) · Zbl 1077.68018
[35] Poetzsch-Heffter, A.; Müller, P.: A programming logic for sequential Java, Lecture notes in computer science 1576, 162-176 (1999)
[36] Jr, J. G. Rossie; Friedman, D. P.; Wand, M.: Modeling subobject-based inheritance, Lecture notes in computer science 1098, 248-274 (1996)
[37] Soundarajan, N.; Fridella, S.: Inheritance: from code reuse to reasoning reuse, IEEE computer society press, 206-215 (1998)
[38] Stroustrup, B.: Multiple inheritance for C++, Computing systems 2, No. 4, 367-395 (1989)
[39] Ungar, D.; Smith, R. B.: Self: the power of simplicity, Lisp and symbolic computation 4, No. 3, 187-206 (1991)
[40] Wasserrab, D.; Nipkow, T.; Snelting, G.; Tip, F.: An operational semantics and type safety proof for multiple inheritance in C++, Proceedings of the conference on object-oriented programming, systems, languages, and applications, 345-362 (2006)
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.