A fully abstract trace-based semantics for reasoning about backward compatibility of class libraries |
| |
Affiliation: | Department of Computer Science, University of Kaiserslautern, Germany |
| |
Abstract: | Backward compatibility is the property that an old version of a library can safely be replaced by a new version 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, such a model must account for the complex interface between library implementations and clients.In this paper, we develop a fully abstract trace-based semantics for class libraries in object-oriented languages, in particular for Java-like sealed packages. Our approach enhances a standard operational semantics such that the change of control between the library and the client context is made explicit in terms of interaction labels. By using traces over these labels, we abstract from the data representation in the heap, support class hiding, and provide fully abstract package denotations. Soundness and completeness of the trace semantics is proven using specialized simulation relations on the enhanced operational semantics. The simulation relations also provide a proof method for reasoning about backward compatibility. |
| |
Keywords: | Full abstraction Class libraries Trace semantics Contextual preorder Backward compatibility |
本文献已被 ScienceDirect 等数据库收录! |
|