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

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.