The Liskov Substitution Principle does more than you think

Hillel Wayne — Computer Things 01/06/26, 04:51 PM News

Summary

The article explores the Liskov Substitution Principle beyond its common interpretation, emphasizing its formal basis in subtyping with preconditions, postconditions, invariants, and history properties, and citing original research papers.

Happy New Year! I'm done with the newsletter hiatus and am going to try updating weekly again. To ease into things a bit, I'll try to keep posts a little more off the cuff and casual for a while, at least until <a href="https://leanpub.com/logic/" target="_blank">Logic for Programmers</a> is done. Speaking of which, v0.13 should be out by the end of this month. So for this newsletter I want to talk about the <a href="https://en.wikipedia.org/wiki/Liskov_substitution_principle" target="_blank">Liskov Substitution Principle</a> (LSP). Last week I read <a href="https://loup-vaillant.fr/articles/solid-bull" target="_blank">A SOLID Load of Bull</a> by cryptographer Loupe Vaillant, where he argues the <a href="https://en.wikipedia.org/wiki/SOLID" target="_blank">SOLID</a> principles of OOP are not worth following. He makes an exception for LSP, but also claims that it's "just subtyping" and further: <blockquote> If I were trying really hard to be negative about the Liskov substitution principle, I would stress that it only applies when inheritance is involved, and inheritance is strongly discouraged anyway. </blockquote> LSP is more interesting than that! In the original paper, <a href="https://www.cs.cmu.edu/~wing/publications/LiskovWing94.pdf" target="_blank">A Behavioral Notion of Subtyping</a>, Barbara Liskov and Jeannette Wing start by defining a "correct" subtyping as follows: <blockquote> Subtype Requirement: Let ϕ(x) be a property provable about objects x of type T. Then ϕ(y) should be true for objects y of type S where S is a subtype of T. </blockquote> From then on, the paper determine what guarantees that a subtype is correct.<a class="footnote-ref" href="#fn:safety">1</a> They identify three conditions: <ol> <li>Each of the subtype's methods has the same or weaker preconditions and the same or stronger postconditions as the corresponding supertype method.<a class="footnote-ref" href="#fn:cocontra">2</a> </li> <li>The subtype satisfies all state invariants of the supertype. </li> <li>The subtype satisfies all "history properties" of the supertype. <a class="footnote-ref" href="#fn:refinement">3</a> e.g. if a supertype has an immutable field, the subtype cannot make it mutable. </li> </ol> (Later, Elisa Baniassad and Alexander Summers <a href="https://www.cs.ubc.ca/~alexsumm/papers/BaniassadSummers21.pdf" target="_blank">would realize</a> these are equivalent to "the subtype passes all black-box tests designed for the supertype", which I wrote a little bit more about <a href="https://www.hillelwayne.com/post/lsp/" target="_blank">here</a>.) I want to focus on the first rule about preconditions and postconditions. This refers to the method's contract. For a function <code>f</code>, <code>f.Pre</code> is what must be true going into the function, and <code>f.Post</code> is what the function guarantees on execution. A canonical example is square root: <div class="codehilite"><pre><code>sqrt.Pre(x) = x >= 0 sqrt.Post(x, out) = out >= 0 && out*out == x </code></pre></div> <div class="subscribe-form"></div> Mathematically we would write this as <code>all x: f.Pre(x) => f.Post(x)</code> (where <code>=></code> is the <a href="https://en.wikipedia.org/wiki/Material_conditional" target="_blank">implication operator</a>). If that relation holds for all <code>x</code>, we say the function is "correct". With this definition we can actually formally deduce the first subtyping requirement. Let <code>caller</code> be some code that uses a method, which we will call <code>super</code>, and let both <code>caller</code> and <code>super</code> be correct. Then we know the following statements are true: <div class="codehilite"><pre><code> 1. caller.Pre && stuff => super.Pre 2. super.Pre => super.Post 3. super.Post && more_stuff => caller.Post </code></pre></div> Now let's say we substitute <code>super</code> with <code>sub</code>, which is also correct. Here is what we now know is true: <div class="codehilite"><pre><code> 1. caller.Pre => super.Pre - 2. super.Pre => super.Post + 2. sub.Pre => sub.Post 3. super.Post => caller.Post </code></pre></div> When is <code>caller</code> still correct? When we can fill in the "gaps" in the chain, aka if <code>super.Pre => sub.Pre</code> and <code>sub.Post => super.Post</code>. In other words, if <code>sub</code>'s preconditions are weaker than (or equivalent to) <code>super</code>'s preconditions and if <code>sub</code>'s postconditions are stronger than (or equivalent to) <code>super</code>'s postconditions. Notice that I never actually said <code>sub</code> was from a subtype of <code>super</code>! The LSP conditions (at least, the contract rule of LSP) doesn't just apply to subtypes but can be applied in any situation where we substitute a function or block of code for another. Subtyping is a common place where this happens, but by no means the only! We can also substitute across time.Any time we modify some code's behavior, we are effectively substituting the new version in for the old version, and so the new version's contract must be compatible with the old version's to guarantee no existing code is broken. For example, say we maintain an API or function with two required inputs, <code>X</code> and <code>Y</code>, and one optional input, <code>Z</code>. Making <code>Z</code> required strengthens the precondition ("input must have Z" is stronger than "input may have Z"), so potentially breaks existing users of our API. Making <code>Y</code> optional weakens the precondition ("input may have Y" is weaker than "input must have Y"), so is guaranteed to be compatible. (This also underpins <a href="https://en.wikipedia.org/wiki/Robustness_principle" target="_blank">The robustness principle</a>: "be conservative in what you send, be liberal in what you accept".) Now the dark side of all this is <a href="https://www.hyrumslaw.com/" target="_blank">Hyrum's Law</a>. In the below code, are <code>new</code>'s postconditions stronger than <code>old</code>'s postconditions? <div class="codehilite"><pre><code>def old(): return {"a": "foo", "b": "bar"} def new(): return {"a": "foo", "b": "bar", "c": "baz"} </code></pre></div> On a first appearance, this is a strengthened postcondition: <code>out.contains_keys([a, b, c]) => out.contains_keys([a, b])</code>. But now someone does this: <div class="codehilite"><pre><code>my_dict = {"c": "blat"} my_dict |= new() assert my_dict[c] == "blat" </code></pre></div> Oh no, their code now breaks! They saw <code>old</code> had the postcondition "<code>out</code> does NOT contain "c" as a key", and then wrote their code expecting that postcondition. In a sense, any change the postcondition can potentially break someone. "All observable behaviors of your system will be depended on by somebody", as <a href="https://www.hyrumslaw.com/" target="_blank">Hyrum's Law</a> puts it. So we need to be explicit in what our postconditions actually are, and properties of the output that are not part of our explicit postconditions are subject to be violated on the next version. You'll break people's workflows but you also have grounds to say "I warned you". Overall, Liskov and Wing did their work in the context of subtyping, but the principles are more widely applicable, certainly to more than just the use of inheritance. <div class="footnote"> <hr/> <ol> <li id="fn:safety"> Though they restrict it to just <a href="https://www.hillelwayne.com/post/safety-and-liveness/" target="_blank">safety properties</a>. <a class="footnote-backref" href="#fnref:safety" title="Jump back to footnote 1 in the text">↩</a> </li> <li id="fn:cocontra"> The paper lists a couple of other authors as introduce the idea of "contra/covariance rules", but part of being "off-the-cuff and casual" means not diving into every referenced paper. So they might have gotten the pre/postconditions thing from an earlier author, dunno for sure! <a class="footnote-backref" href="#fnref:cocontra" title="Jump back to footnote 2 in the text">↩</a> </li> <li id="fn:refinement"> I believe that this is equivalent to the formal methods notion of a <a href="https://www.hillelwayne.com/post/refinement/" target="_blank">refinement</a>. <a class="footnote-backref" href="#fnref:refinement" title="Jump back to footnote 3 in the text">↩</a> </li> </ol> </div>

Original Article

View Cached Full Text

Cached at: 05/16/26, 03:40 AM

# The Liskov Substitution Principle does more than you think Source: [https://buttondown.com/hillelwayne/archive/the-liskov-substitution-principle-does-more-than](https://buttondown.com/hillelwayne/archive/the-liskov-substitution-principle-does-more-than) Happy New Year\! I'm done with the newsletter hiatus and am going to try updating weekly again\. To ease into things a bit, I'll try to keep posts a little more off the cuff and casual for a while, at least until[*Logic for Programmers*](https://leanpub.com/logic/)is done\. Speaking of which, v0\.13 should be out by the end of this month\. So for this newsletter I want to talk about the[Liskov Substitution Principle](https://en.wikipedia.org/wiki/Liskov_substitution_principle)\(LSP\)\. Last week I read[A SOLID Load of Bull](https://loup-vaillant.fr/articles/solid-bull)by cryptographer Loupe Vaillant, where he argues the[SOLID](https://en.wikipedia.org/wiki/SOLID)principles of OOP are not worth following\. He makes an exception for LSP, but also claims that it's "just subtyping" and further: > If I were trying really hard to be negative about the Liskov substitution principle, I would stress that**it only applies when inheritance is involved**, and inheritance is strongly discouraged anyway\. LSP is more interesting than that\! In the original paper,[A Behavioral Notion of Subtyping](https://www.cs.cmu.edu/~wing/publications/LiskovWing94.pdf), Barbara Liskov and Jeannette Wing start by defining a "correct" subtyping as follows: > Subtype Requirement: Let ϕ\(x\) be a property provable about objects x of type T\. Then ϕ\(y\) should be true for objects y of type S where S is a subtype of T\. From then on, the paper determine what*guarantees*that a subtype is correct\.[1](https://buttondown.com/hillelwayne/archive/the-liskov-substitution-principle-does-more-than#fn:safety)They identify three conditions: 1. Each of the subtype's methods has the same or weaker preconditions and the same or stronger postconditions as the corresponding supertype method\.[2](https://buttondown.com/hillelwayne/archive/the-liskov-substitution-principle-does-more-than#fn:cocontra) 2. The subtype satisfies all state invariants of the supertype\. 3. The subtype satisfies all "history properties" of the supertype\.[3](https://buttondown.com/hillelwayne/archive/the-liskov-substitution-principle-does-more-than#fn:refinement)e\.g\. if a supertype has an immutable field, the subtype cannot make it mutable\. \(Later, Elisa Baniassad and Alexander Summers[would realize](https://www.cs.ubc.ca/~alexsumm/papers/BaniassadSummers21.pdf)these are equivalent to "the subtype passes all black\-box tests designed for the supertype", which I wrote a little bit more about[here](https://www.hillelwayne.com/post/lsp/)\.\) I want to focus on the first rule about preconditions and postconditions\. This refers to the method's**contract**\. For a function`f`,`f\.Pre`is what must be true going into the function, and`f\.Post`is what the function guarantees on execution\. A canonical example is square root: ``` sqrt.Pre(x) = x >= 0 sqrt.Post(x, out) = out >= 0 && out*out == x ``` Mathematically we would write this as`all x: f\.Pre\(x\) =\> f\.Post\(x\)`\(where`=\>`is the[implication operator](https://en.wikipedia.org/wiki/Material_conditional)\)\. If that relation holds for all`x`, we say the function is "correct"\. With this definition we can actually formally deduce the first subtyping requirement\. Let`caller`be some code that uses a method, which we will call`super`, and let both`caller`and`super`be correct\. Then we know the following statements are true: ``` 1. caller.Pre && stuff => super.Pre 2. super.Pre => super.Post 3. super.Post && more_stuff => caller.Post ``` Now let's say we substitute`super`with`sub`, which is also correct\. Here is what we now know is true: ``` 1. caller.Pre => super.Pre - 2. super.Pre => super.Post + 2. sub.Pre => sub.Post 3. super.Post => caller.Post ``` When is`caller`still correct? When we can fill in the "gaps" in the chain, aka if`super\.Pre =\> sub\.Pre`and`sub\.Post =\> super\.Post`\. In other words, if`sub`'s preconditions are weaker than \(or equivalent to\)`super`'s preconditions and if`sub`'s postconditions are stronger than \(or equivalent to\)`super`'s postconditions\. Notice that I never actually said`sub`was from a subtype of`super`\! The LSP conditions \(at least, the contract rule of LSP\) doesn't just apply to*subtypes*but can be applied in any situation where we substitute a function or block of code for another\. Subtyping is a common place where this happens, but by no means the only\! We can also substitute across time\.Any time we modify some code's behavior, we are effectively substituting the new version in for the old version, and so the new version's contract must be compatible with the old version's to guarantee no existing code is broken\. For example, say we maintain an API or function with two required inputs,`X`and`Y`, and one optional input,`Z`\. Making`Z`required strengthens the precondition \("input must have Z" is stronger than "input may have Z"\), so potentially breaks existing users of our API\. Making`Y`optional weakens the precondition \("input may have Y" is weaker than "input must have Y"\), so is guaranteed to be compatible\. \(This also underpins[The robustness principle](https://en.wikipedia.org/wiki/Robustness_principle): "be conservative in what you send, be liberal in what you accept"\.\) Now the dark side of all this is[Hyrum's Law](https://www.hyrumslaw.com/)\. In the below code, are`new`'s postconditions stronger than`old`'s postconditions? ``` def old(): return {"a": "foo", "b": "bar"} def new(): return {"a": "foo", "b": "bar", "c": "baz"} ``` On a first appearance, this is a strengthened postcondition:`out\.contains\_keys\(\[a, b, c\]\) =\> out\.contains\_keys\(\[a, b\]\)`\. But now someone does this: ``` my_dict = {"c": "blat"} my_dict |= new() assert my_dict[c] == "blat" ``` Oh no, their code now breaks\! They saw`old`had the postcondition "`out`does NOT contain "c" as a key", and then wrote their code expecting that postcondition\. In a sense,*any*change the postcondition can potentially break*someone*\. "All observable behaviors of your system will be depended on by somebody", as[Hyrum's Law](https://www.hyrumslaw.com/)puts it\. So we need to be explicit in what our postconditions actually are, and properties of the output that are not part of our explicit postconditions are subject to be violated on the next version\. You'll break people's workflows but you also have grounds to say "I warned you"\. Overall, Liskov and Wing did their work in the context of subtyping, but the principles are more widely applicable, certainly to more than just the use of inheritance\.

The Liskov Substitution Principle does more than you think

Similar Articles

Assumptions weaken properties

Proving What's Possible

Thinking in States

Improving LLM Code Reasoning via Semantic Equivalence Self-Play with Formal Verification

People get confused when language implementations break language guarantees

Submit Feedback