In object-oriented programming, behavioral subtyping requires that subclasses meet the behavioral expectations set by the specifications of their superclasses, ensuring clients relying on the superclass type remain correct. For instance, a Stack exhibiting LIFO behavior should not be a subtype of a Queue expecting FIFO behavior, as this violates the principle despite being syntactically type-safe. Instead, both Stack and Queue can be behavioral subtypes of a more general type Bag that only specifies removal of some element, preserving correctness. Behavioral subtyping depends solely on the specification, not the implementation, of the types, emphasizing the importance of clear behavioral documentation in OOP.
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 Ps and a postcondition Qs is stronger than one given by a precondition Pt and a postcondition Qt (formally: (Ps, Qs) ⇒ (Pt, Qt)) if Ps is weaker than Pt (i.e. Pt implies Ps) and Qs is stronger than Qt (i.e. Qs implies Qt). 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 ((Ps, Qs) ⇒ (Pt, Qt)) without strengthening the postcondition (Qs ⇏ Qt).23 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 Ps and postcondition Qs to be stronger than a specification with precondition Pt and postcondition Qt is that Ps is weaker than Pt and "Qs or not Ps" is stronger than "Qt or not Pt". Indeed, "result = |x| or false" does strengthen "result = x or x < 0".
"Substitutability"
In an influential keynote address4 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 o 1 {\displaystyle o_{1}} of type S there is an object o 2 {\displaystyle o_{2}} of type T such that for all programs P defined in terms of T, the behavior of P is unchanged when o 1 {\displaystyle o_{1}} is substituted for o 2 {\displaystyle o_{2}} , then S is a subtype of T." This characterization 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.5 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 publication6 on behavioral subtyping, and indeed that "technically, it's called behavioral subtyping".7 During the interview, she does not use substitution terminology to discuss the concepts.
Notes
- 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.
References
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. https://doi.org/10.1145%2F197320.197383 ↩
Parkinson, Matthew J. (2005). Local reasoning for Java (PDF) (PhD). University of Cambridge. https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-654.pdf ↩
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. https://lib.dr.iastate.edu/cgi/viewcontent.cgi?article=1249&context=cs_techreports ↩
Liskov, B. (May 1988). "Keynote address - data abstraction and hierarchy". ACM SIGPLAN Notices. 23 (5): 17–34. doi:10.1145/62139.62141. /wiki/Barbara_Liskov ↩
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. https://lib.dr.iastate.edu/cgi/viewcontent.cgi?article=1249&context=cs_techreports ↩
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. https://doi.org/10.1145%2F197320.197383 ↩
van Vleck, Tom (April 20, 2016). Interview with Barbara Liskov. ACM. Archived from the original on 2021-12-21. https://www.youtube.com/watch?v=-Z-17h3jG0A ↩