Behavioral subtyping

In object-oriented programming, behavioral subtyping is the principle that subclasses should satisfy the expectations of clients accessing subclass objects through references of superclass type, not just as regards syntactic safety (absence of method-not-found errors and such) but also as regards behavioral correctness. Specifically, properties that clients can prove using the specification of an object's presumed type should hold even though the object is actually a member of a subtype of that type.

For example, consider a type Stack and a type Queue, that both have a put method to add an element and a get method to remove one. Suppose the documentation associated with these types specifies that type Stack's methods shall behave as expected for stacks (i.e. they shall exhibit LIFO behavior), and that type Queue's methods shall behave as expected for queues (i.e. they shall exhibit FIFO behavior). Suppose, now, that type Stack were declared as a subclass of type Queue. Most programming language compilers ignore documentation and perform only the checks that are necessary to preserve type safety. Since, for each method of type Queue, type Stack provides a method with a matching name and signature, this check would succeed. However, clients accessing a Stack object through a reference of type Queue would, based on Queue's documentation, expect FIFO behavior but observe LIFO behavior, invalidating these clients' correctness proofs and potentially leading to incorrect behavior of the program as a whole.

This example violates behavioral subtyping because type Stack is not a behavioral subtype of type Queue: it is not the case that the behaviors allowed by Stack are also allowed by Queue.

In contrast, a program where both Stack and Queue are subclasses of a type Bag, whose specification for get is merely that it removes some element, does satisfy behavioral subtyping and allows clients to safely reason about correctness based on the presumed types of the objects they interact with. Indeed, any object that satisfies the Stack or Queue specification also satisfies the Bag specification.

It is important to stress that whether a type S is a behavioral subtype of a type T depends only on the specification of type T; the implementation of type T, if it has any, is completely irrelevant to this question. Indeed, type T need not even have an implementation; it might be a purely abstract class. As another case in point, type Stack above is a behavioral subtype of type Bag even if type Bag's implementation exhibits FIFO behavior: what matters is that type Bag's specification does not specify which element is removed by method get. This also means that behavioral subtyping can be discussed only with respect to a particular (behavioral) specification for each type involved, and that if the types involved have no well-defined behavioral specification, behavioral subtyping cannot be discussed meaningfully.

Verifying behavioral subtyping

A type S is a behavioral subtype of a type T if each behavior allowed by the specification of S is also allowed by the specification of T. This requires, in particular, that for each method M of T, the specification of M in S is stronger than the one in T.

A method specification given by a precondition P and a postcondition Q is stronger than one given by a precondition P' and a postcondition Q' if P is weaker than P' (i.e. P' implies P) and Q is stronger than Q' (i.e. Q implies Q'). That is, strengthening a method specification can be done by strengthening the postcondition and by weakening the precondition. Indeed, a method specification is stronger if it imposes more specific constraints on the outputs for inputs that were already supported, or if it requires more inputs to be supported.

For example, consider the (very weak) specification for a method that computes the absolute value of an argument x, that specifies a precondition 0 ≤ x and a postcondition 0 ≤ result. This specification says the method need not support negative values for x, and it need only ensure the result is nonnegative as well. Two possible ways to strenghten this specification are by strengthening the postcondition to state result = |x|, i.e. the result is equal to the absolute value of x, or by weakening the precondition to "true", i.e. all values for x should be supported. Of course, we can also combine both, into a specification that states that the result should equal the absolute value of x, for any value of x.

Note, however, that it is possible to strengthen a specification without strengthening the postcondition. Consider a specification for the absolute value method that specifies a precondition 0 ≤ x and a postcondition result = x. The specification that specifies a precondition "true" and a postcondition result = |x| strengthens this specification, even though the postcondition result = |x| does not strengthen (or weaken) the postcondition result = x. The necessary condition for a specification with precondition P and postcondition Q to be stronger than a specification with precondition P' and postcondition Q' is that P is weaker than P' and "Q or not P" is stronger than "Q' or not P'". Indeed, "result = |x| or false" does strengthen "result = x or x < 0".

References

• Parkinson, Matthew J.; Bierman, Gavin M. (January 2008). "Separation logic, abstraction and inheritance". ACM SIGPLAN Notices. 43 (1): 75–86. doi:10.1145/1328897.1328451.