Liskov substitution principle

This article includes a list of general references, but it lacks sufficient corresponding inline citations. Please help to improve this article by introducing more precise citations. (October 2018) (Learn how and when to remove this message)

The Liskov substitution principle (LSP) is a particular definition of a subtyping relation, called strong behavioral subtyping, that was initially introduced by Barbara Liskov in a 1987 conference keynote address titled Data abstraction and hierarchy. It is based on the concept of "substitutability" – a principle in object-oriented programming stating that an object (such as a class) may be replaced by a sub-object (such as a class that extends the first class) without breaking the program. It is a semantic rather than merely syntactic relation, because it intends to guarantee semantic interoperability of types in a hierarchy, object types in particular. Barbara Liskov and Jeannette Wing described the principle succinctly in a 1994 paper as follows:^[1]

Subtype Requirement: Let ⁠${\displaystyle \phi (x)}$⁠ be a property provable about objects ⁠${\displaystyle x}$⁠ of type T. Then ⁠${\displaystyle \phi (y)}$⁠ should be true for objects ⁠${\displaystyle y}$⁠ of type S where S is a subtype of T.

Symbolically:

${\displaystyle S\leq T\to (\forall x{:}T.\phi (x)\to \forall y{:}S.\phi (y))}$

That is, if S subtypes T, what holds for T-objects holds for S-objects. In the same paper, Liskov and Wing detailed their notion of behavioral subtyping in an extension of Hoare logic, which bears a certain resemblance to Bertrand Meyer's design by contract in that it considers the interaction of subtyping with preconditions, postconditions and invariants.