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 (such as absence of "method-not-found" errors) 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. [1]

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_s and a postcondition Q_s is stronger than one given by a precondition P_t and a postcondition Q_t (formally: (P_s, Q_s) ⇒ (P_t, Q_t)) if P_s is weaker than P_t (i.e. P_t implies P_s) and Q_s is stronger than Q_t (i.e. Q_s implies Q_t). 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 strengthen 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 ((P_s, Q_s) ⇒ (P_t, Q_t)) without strengthening the postcondition (Q_s ⇏ Q_t).[2][3] 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_s and postcondition Q_s to be stronger than a specification with precondition P_t and postcondition Q_t is that P_s is weaker than P_t and "Q_s or not P_s" is stronger than "Q_t or not P_t". Indeed, "result = |x| or false" does strengthen "result = x or x < 0".

"Substitutability"

In an influential keynote address[4] on data abstraction and class hierarchies at the OOPSLA 1987 programming language research conference, Barbara Liskov said the following: "What is wanted here is something like the following substitution property: If for each object ${\displaystyle o_{1}}$ of type S there is an object ${\displaystyle o_{2}}$ of type T such that for all programs P defined in terms of T, the behavior of P is unchanged when ${\displaystyle o_{1}}$ is substituted for ${\displaystyle o_{2}}$, then S is a subtype of T." This characterisation has since been widely known as the Liskov Substitution Principle (LSP). Unfortunately, though, it has several issues. Firstly, in its original formulation, it is too strong: we rarely want the behavior of a subclass to be identical to that of its superclass; substituting a subclass object for a superclass object is often done with the intent to change the program's behavior, albeit, if behavioral subtyping is respected, in a way that maintains the program's desirable properties. Secondly, it makes no mention of specifications, so it invites an incorrect reading where the implementation of type S is compared to the implementation of type T. This is problematic for several reasons, one being that it does not support the common case where T is abstract and has no implementation. Thirdly, and most subtly, in the context of object-oriented imperative programming it is difficult to define precisely what it means to universally or existentially quantify over objects of a given type, or to substitute one object for another.[3] In the example above, we are not substituting a Stack object for a Bag object, we are simply using a Stack object as a Bag object.

In an interview in 2016, Liskov herself explains that what she presented in her keynote address was an "informal rule", that Jeannette Wing later proposed that they "try to figure out precisely what this means", which led to their joint publication[1] on behavioral subtyping, and indeed that "technically, it's called behavioral subtyping".[5] During the interview, she does not use substitution terminology to discuss the concepts.

Notes

1. Liskov, Barbara; Wing, Jeannette (1994-11-01). "A behavioral notion of subtyping". ACM Transactions on Programming Languages and Systems. 16 (6): 1811–1841. doi:10.1145/197320.197383.
2. Parkinson, Matthew J. (2005). Local reasoning for Java (PDF) (PhD). University of Cambridge.
3. Leavens, Gary T.; Naumann, David A. (August 2015). "Behavioral subtyping, specification inheritance, and modular reasoning". ACM Transactions on Programming Languages and Systems. 37 (4). doi:10.1145/2766446.
4. Liskov, B. (May 1988). "Keynote address - data abstraction and hierarchy". ACM SIGPLAN Notices. 23 (5): 17–34. doi:10.1145/62139.62141.
5. van Vleck, Tom (April 20, 2016). Interview with Barbara Liskov. ACM.

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.