We present a sound and complete method for reasoning about contextual 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 otherwise equivalent implementations. Similar reasoning techniques for class-based languages [AbrahamskyEtal04, JeffreyRathke05] don't consider inheritance at all, or forbid the context from extending related classes. Other techniques that do consider inheritance [BanerjeeNaumann05] 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 calculi admit limitations [PittsStark98, SumiiPierce05].
Adding inheritance to a class-based language increases the distinguishing power of the context. Here we show how this extra distinguishing 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.
[Full paper (pdf)]
Presented at FOOL/WOOD; Saturday, 20 January 2007; Nice, France