A fully abstract trace-based semantics for reasoning about backward compatibility of class libraries

•We develop a fully abstract trace-based semantics for class libraries.•The trace-based semantics is directly tied to a standard small-step operational model.•Full abstraction is proven using specialized simulation relations.•A sound and complete proof method for reasoning about backward compatibility is provided.

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.