Generating Boogie Verification Conditions for Backward Compatibility of Class Libraries
When changing the implementation of a library, the behavior of the old implementation has to be retained, such that programs using the old implementation still work as expected with the new implementation. If the behavior exhibited by a new library implementation is the same as the behavior of an old implementation, the new implementation is backward compatible.
This thesis presents a tool which is capable of automatically verifying backward compatibility of two Java library implementations using a coupling invariant relating the internal state of both implementations. Checking the equality of the well-defined interactions between the context and the library is the basis for verifying backward compatibility. The tool called BCVerifier works by generating a model from the byte code of both library implementations in the intermediate verification language Boogie. Support for dynamic method dispatch and recursive computation are the features that distinguish the approach from existing equivalence checking tools. Working examples show the applicability of the approach to non-trivial examples of library evolution.