
Liskov substitution principle

Substitutability is a principle in object-oriented programming stating that, in a computer program, if S is a subtype of T, then objects of type T may be "replaced" with objects of type S (i.e., an object of type T may be "substituted" with any object of a subtype S) without altering any of the desirable properties of the program (correctness, task performed, etc.). More formally, 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 1988 conference keynote address titled "Data abstraction and hierarchy". 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:
"Subtype Requirement": Let be a property provable about objects of type . Then should be true for objects of type where is a subtype of . 
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.
Principle.
Liskov's notion of a behavioural subtype defines a notion of substitutability for objects; that is, if "S" is a subtype of "T", then objects of type "T" in a program may be replaced with objects of type "S" without altering any of the desirable properties of that program (e.g. correctness).
Behavioural subtyping is a stronger notion than typical subtyping of functions defined in type theory, which relies only on the contravariance of parameter types and covariance of the return type. Behavioural subtyping is undecidable in general: if "q" is the property "method for "x" always terminates", then it is impossible for a program (e.g. a compiler) to verify that it holds true for some subtype "S" of "T", even if "q" does hold for "T". Nonetheless, the principle is useful in reasoning about the design of class hierarchies.
Liskov substitution principle imposes some standard requirements on signatures that have been adopted in newer object-oriented programming languages (usually at the level of classes rather than types; see nominal vs. structural subtyping for the distinction):
In addition to the signature requirements, the subtype must meet a number of behavioural conditions. These are detailed in a terminology resembling that of design by contract methodology, leading to some restrictions on how contracts can interact with inheritance:
Origins.
The rules on pre- and postconditions are identical to those introduced by Bertrand Meyer in his 1988 book "Object-Oriented Software Construction". Both Meyer, and later Pierre America, who was the first to use the term "behavioral subtyping", gave proof-theoretic definitions of some behavioral subtyping notions, but their definitions did not take into account aliasing that may occur in programming languages that support references or pointers. Taking aliasing into account was the major improvement made by Liskov and Wing (1994), and a key ingredient is the history constraint. Under the definitions of Meyer and America, a mutable point would be a behavioral subtype of an immutable point, whereas Liskov substitution principle forbids this.
Criticism.
While widely used, the characterization of behavioral subtyping as the ability to substitute subtype objects for supertype objects has been said to be flawed. It makes no mention of "specifications", so it invites an incorrect reading where the "implementation" of the supertype is compared to the "implementation" of the subtype. This is problematic for several reasons, one being that it does not support the common case where the supertype is abstract and has no implementation. Also, more 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. When applying subtyping, generally we are not substituting subtype objects for supertype objects, we are simply using subtype objects as supertype objects. That is, it is the same objects, the subtype objects, that are also supertype objects.
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 on behavioral subtyping, and indeed that "technically, it's called behavioral subtyping". During the interview, she does not use substitution terminology to discuss the concepts.
Bibliography.
General references
Specific references