nach oben

Erschienen in:

2016 | OriginalPaper | Buchkapitel

Reasoning About Inheritance and Unrestricted Reuse in Object-Oriented Concurrent Systems

verfasst von : Olaf Owe

Erschienen in: Integrated Formal Methods

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

Code reuse is a fundamental aspect of object-oriented programs, and in particular, the mechanisms of inheritance and late binding provide great flexibility in code reuse, without semantical limitations other than type-correctness. However, modular reasoning about late binding and inheritance is challenging, and formal reasoning approaches place semantical restrictions on code reuse in order to preserve properties from superclasses. The overall aim of this paper is to develop a formal framework for modular reasoning about classes and inheritance, supporting unrestricted reuse of code, as well as of specifications. The main contribution is a Hoare-style logic supporting free reuse, worked out for a high-level concurrent object-oriented language. We also show results on verification reuse, based on a combination of Hoare-style logic and static checking. An example illustrates the difference to comparable reasoning formalisms.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Towards a Thread-Local Proof Technique for Starvation Freedom

Nächstes Kapitel A Formal Model of the Safety-Critical Java Level 2 Paradigm

Ahrendt, W., Dylla, M.: A system for compositional verification of asynchronous objects. Sci. Comput. Program. 77(12), 1289–1309 (2012)CrossRefMATH

America, P.: A behavioural approach to subtyping in object-oriented programming languages. 443, Phillips Research Laboratories, January/April (1989)

Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: an overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 49–69. Springer, Heidelberg (2005)CrossRef

Burdy, L., Cheon, Y., Cok, D.R., Ernst, M., Kiniry, J., Leavens, G.T., Leino, K.R.M., Poll, E.: An overview of JML tools and applications. In: FMICS 2003, Electron. Notes Theor. Comput. Sci. 80, 73–89 (2003). Elsevier

Chin, W.-N., David, H., Nguyen, H.-H., Qin, S.: Enhancing modular OO verification with separation logic. In: POPL 2008, pp. 87–99. ACM (2008)

Dahl, O.-J.: Verifiable Programming, vol. Prentice Hall. International Series in Computer Science, New York (1992)MATH

Dhara, K.K., Leavens, G.T.: Forcing behavioural subtyping through specification inheritance. In: 18th International Conference on Software Engineering, pp. 258–267. IEEE (1996)

Din, C.C., Owe, O.: Compositional reasoning about active objects with shared futures. Formal Aspects Comput. 27, 1–22 (2014)MathSciNetMATH

Din, C.C., Owe, O.: A sound and complete reasoning system for asynchronous communication with shared futures. JLAP 83(5–6), 360–383 (2014)MathSciNetMATH

10.

Dovland, J., Johnsen, E.B., Owe, O., Steffen, M.: Lazy behavioral subtyping. J. Logic Algebraic Program. 79(7), 578–607 (2010)MathSciNetCrossRefMATH

11.

Hoare, C.A.R.: An axiomatic basis of computer programming. Commun. ACM 12, 576–580 (1969)CrossRefMATH

12.

Johnsen, E.B., Owe, O., Creol, I.C.Y.: A type-safe object-oriented model for distributed concurrent systems. Theor. Comp. Sci. 365(1–2), 23–66 (2006)MathSciNetCrossRefMATH

13.

Leavens, G.T., Naumann, D.A.: Behavioral subtyping, specification inheritance, and modular reasoning. ACM Trans. Program. Lang. Syst. 37(4), 13 (2015)CrossRef

14.

Leino, K.R.M., Wallenburg, A.: Class-local Object Invariants. In: 1st India Software Engineering Conference (ISEC 2008), pp. 57–66. ACM (2008)

15.

Liskov, B.H., Wing, J.M.: A behavioral notion of subtyping. ACM Trans. Program. Lang. Syst. 6(16), 1811–1841 (1994)CrossRef

16.

Middelkoop, R., Huizing, C., Kuiper, R., Luit, E.J.: Invariants for non-hierarchical object structures. Electron. Notes Theor. Comput. Sci. 195, 211–229 (2008)CrossRefMATH

17.

Mikhajlov, L., Sekerinski, E.: A study of the fragile base class problem. In: Jul, E. (ed.) ECOOP ’98 – Object-Oriented Programming. LNCS, vol. 1445, pp. 355–382. Springer, Heidelberg (1998)CrossRef

18.

Owe, O.: Verifiable programming of object-oriented and distributed systems. In: From Action System to Distributed Systems, pp. 61–80. Taylor & Francis (2016)

19.

Owe, O., Ryl, I.: On combining object orientation, openness and reliability. In: Norwegian Informatics Conference (NIK 1999), Tapir (1999)

20.

Parkinson, M.J., Biermann, G.M.: Separation logic, abstraction, and inheritance. In: POPL 2008, ACM (2008)

21.

Pierik, C., de Boer, F.S.: A proof outline logic for object-oriented programming. Theor. Comput. Sci. 343(3), 413–442 (2005)MathSciNetCrossRefMATH

22.

Poetzsch-Heffter, A., Müller, P.O.: A programming logic for sequential Java. In: Swierstra, S.D. (ed.) ESOP 1999. LNCS, vol. 1576, pp. 162–176. Springer, Heidelberg (1999)CrossRef

23.

Polikarpova, N., Tschannen, J., Furia, C.A., Meyer, B.: Flexible invariants through semantic collaboration. CoRR, abs/1311.6329 (2013)

24.

Pradel, M., Gross, T.R.: Automatic testing of sequential and concurrent substitutability. In: International Conference on Software Engineering (ICSE) (2013)

25.

Soundarajan, N., Fridella, S.: Inheritance: From code reuse to reasoning reuse. In: Fifth International Conference on Software Reuse (ICSR5), pp. 206–215. IEEE (1998)

26.

Soundararajan, N.: A proof technique for parallel programs. Theor. Comput. Sci. 31(1–2), 13–29 (1984)MathSciNetCrossRefMATH

27.

Summers, A.J., Drossopoulou, S.: Considerate reasoning and the composite design pattern. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol. 5944, pp. 328–344. Springer, Heidelberg (2010)CrossRef

28.

Wehrheim, H.: Behavioral subtyping relations for active objects. Formal Methods Syst. Des. 23(2), 143–170 (2003)CrossRefMATH

Titel: Reasoning About Inheritance and Unrestricted Reuse in Object-Oriented Concurrent Systems
verfasst von: Olaf Owe
Verlag: Springer International Publishing
Buch: Integrated Formal Methods
Print ISBN: 978-3-319-33692-3

Electronic ISBN: 978-3-319-33693-0

Copyright-Jahr: 2016
DOI: https://doi.org/10.1007/978-3-319-33693-0_14

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"