Reasoning about Backward Compatibility of Class Libraries

  • Backward compatibility of class libraries ensures that an old implementation of a library can safely be replaced by a new implementation without breaking existing clients. Formal reasoning about backward compatibility requires an adequate semantic model to compare the behavior of two library implementations. In the object-oriented setting with inheritance and callbacks, finding such models is difficult as the interface between library implementations and clients are complex. Furthermore, handling these models in a way to support practical reasoning requires appropriate verification tools. This thesis proposes a formal model for library implementations and a reasoning approach for backward compatibility that is implemented using an automatic verifier. The first part of the thesis develops a fully abstract trace-based semantics for class libraries of a core sequential object-oriented language. Traces abstract from the control flow (stack) and data representation (heap) of the library implementations. The construction of a most general context is given that abstracts exactly from all possible clients of the library implementation. Soundness and completeness of the trace semantics as well as the most general context are proven using specialized simulation relations on the operational semantics. The simulation relations also provide a proof method for reasoning about backward compatibility. The second part of the thesis presents the implementation of the simulation-based proof method for an automatic verifier to check backward compatibility of class libraries written in Java. The approach works for complex library implementations, with recursion and loops, in the setting of unknown program contexts. The verification process relies on a coupling invariant that describes a relation between programs that use the old library implementation and programs that use the new library implementation. The thesis presents a specification language to formulate such coupling invariants. Finally, an application of the developed theory and tool to typical examples from the literature validates the reasoning and verification approach.

Download full text files

Export metadata

Metadaten
Author:Yannick Welsch
URN:urn:nbn:de:hbz:386-kluedo-36607
Advisor:Arnd Poetzsch-Heffter
Document Type:Doctoral Thesis
Language of publication:English
Date of Publication (online):2013/08/29
Year of first Publication:2013
Publishing Institution:Technische Universität Kaiserslautern
Granting Institution:Technische Universität Kaiserslautern
Acceptance Date of the Thesis:2013/08/29
Date of the Publication (Server):2013/12/16
Page Number:XV, 163
Faculties / Organisational entities:Kaiserslautern - Fachbereich Informatik
CCS-Classification (computer science):D. Software / D.3 PROGRAMMING LANGUAGES / D.3.1 Formal Definitions and Theory (D.2.1, F.3.1-2, F.4.2-3) / Semantics
DDC-Cassification:0 Allgemeines, Informatik, Informationswissenschaft / 004 Informatik
Licence (German):Standard gemäß KLUEDO-Leitlinien vom 10.09.2012