Behavioral subtyping, specification inheritance, and modular reasoning

Verification of a dynamically dispatched method call, E.m(), seems to depend on E's dynamic type. To avoid case analysis and allow incremental development, object-oriented program verification uses supertype abstraction. In other words, one reasons about E.m() using m's specification for E's static type. Supertype abstraction is valid when each subtype in the program is a behavioral subtype. This article semantically formalizes supertype abstraction and behavioral subtyping for a Java-like sequential language with mutation and proves that behavioral subtyping is both necessary and sufficient for the validity of supertype abstraction. Specification inheritance, as in JML, is also formalized and proved to entail behavioral subtyping.