History-based reasoning about behavioral subtyping

We introduce a new history-based proof-theory for reasoning about behavioral subtyping in class and interface hierarchies. Our approach is based on a semantic definition of types in terms of sets of sequences of method calls and returns, so-called histories.Behavioral subtyping is then naturally defined semantically as a set-theoretic subset relation between sets of histories, modulo a projection relation that captures the syntactic subtype relation. The main contribution is a Hoare-style proof theory for the specification and verification of the behavioral subtyping relation in terms of histories, abstracting from the underlying implementation.Through the use of a banking example we show the practical applicability of our approach. Open Science. Includes a source code artifact [8].

• View at Publisher