History-based reasoning about behavioral subtyping (extended paper)

We introduce a new history-based proof method for reasoning about behavioral subtyping in class and interface hierarchies. Our approach is based on histories: sequences where method calls and their corresponding returns are recorded as a single event. Behavioral subtyping is then defined semantically as a relation between sets of histories, modulo a projection relation that captures the syntactic inheritance relation. The main contribution is a Hoare-style proof theory for the specification and verification of object-oriented programs, allowing one to reason also about interfaces where one abstracts from the state of 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 [45].

• View at Publisher