Reasoning about class behavior

We present a sound and complete method for reasoning about con-textual equivalence between different implementations of classes in an imperative subset of Java. To the extent of our knowledge this is the first such method for a language with unrestricted inheritance, where the context can arbitrarily extend classes to distinguish other-wise equivalent implementations. Similar reasoning techniques for class-based languages [1, 12] don’t consider inheritance at all, or forbid the context from extending related classes. Other techniques that do consider inheritance [3] study whole-program equivalence. Our technique also handles public, private, and protected interfaces of classes, imperative fields, and invocations of callbacks. Using our technique we were able to prove equivalences in examples with higher-order behavior, where previous methods for functional cal-culi admit limitations [21, 24]. Adding inheritance to a class-based language increases the dis-tinguishing power of the context. Here we show how this extra dis-tinguishing power is reflected in the conditions for equivalence of our technique. Furthermore we show that adding a cast operator is a conservative extension of the language. 1