里氏替换原则远超你的想象

Hillel Wayne — Computer Things 2026/01/06 16:51 新闻

摘要

本文探讨了里氏替换原则超越其常见解释的内涵，强调其基于子类型的形式化基础，涉及前置条件、后置条件、不变量和历史属性，并引用了原始研究论文。

新年快乐！我已经结束了新闻通讯的休假，打算再次尝试每周更新。为了稍微轻松一下，我会尽量保持文章随性和随意一些，至少在 <a href="https://leanpub.com/logic/" target="_blank">Logic for Programmers</a> 完成之前是这样。顺便说一句，v0.13 应该会在本月底发布。 所以这期新闻通讯我想谈谈 <a href="https://en.wikipedia.org/wiki/Liskov_substitution_principle" target="_blank">里氏替换原则</a>（LSP）。上周我读了密码学家 Loupe Vaillant 的 <a href="https://loup-vaillant.fr/articles/solid-bull" target="_blank">A SOLID Load of Bull</a>，他在文中主张面向对象编程的 SOLID 原则不值得遵循。他特例对待 LSP，但又称它“只是子类型”，并进一步说道： <blockquote> 如果我真的想对里氏替换原则持否定态度，我会强调它只在涉及继承时才适用，而且无论如何，继承都是强烈不推荐的。 </blockquote> LSP 比那有趣多了！在原始论文 <a href="https://www.cs.cmu.edu/~wing/publications/LiskovWing94.pdf" target="_blank">A Behavioral Notion of Subtyping</a> 中，Barbara Liskov 和 Jeannette Wing 首先定义了“正确”的子类型如下： <blockquote> 子类型要求：设 ϕ(x) 是关于类型 T 的对象 x 可证明的性质。那么对于类型 S 的对象 y，其中 S 是 T 的子类型，ϕ(y) 应为真。 </blockquote> 从那以后，论文确定了什么保证子类型是正确的<a class="footnote-ref" href="#fn:safety">1</a>。他们指出了三个条件： <ol> <li>子类型的每个方法具有与超类型方法相同或更弱的前置条件，以及相同或更强的后置条件<a class="footnote-ref" href="#fn:cocontra">2</a>。</li> <li>子类型满足超类型的所有状态不变量。</li> <li>子类型满足超类型的所有“历史属性”<a class="footnote-ref" href="#fn:refinement">3</a>。例如，如果超类型有一个不可变字段，子类型不能使其可变。</li> </ol> （后来，Elisa Baniassad 和 Alexander Summers <a href="https://www.cs.ubc.ca/~alexsumm/papers/BaniassadSummers21.pdf" target="_blank">意识到</a>这些等价于“子类型通过了为超类型设计的所有黑盒测试”，我曾在<a href="https://www.hillelwayne.com/post/lsp/" target="_blank">这里</a>稍微多写过一些。） 我想重点讨论关于前置条件和后置条件的第一条规则。这指的是方法的契约。对于函数 <code>f</code>，<code>f.Pre</code> 是在进入函数时必须为真的条件，而 <code>f.Post</code> 是函数执行后保证的条件。一个经典例子是平方根： <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> 数学上我们会将其写作 <code>all x: f.Pre(x) => f.Post(x)</code>（其中 <code>=></code> 是<a href="https://en.wikipedia.org/wiki/Material_conditional" target="_blank">蕴含运算符</a>）。如果该关系对所有 <code>x</code> 成立，我们就说该函数是“正确的”。有了这个定义，我们可以实际形式化推导出第一个子类型要求。让 <code>caller</code> 是使用某个方法（称之为 <code>super</code>）的代码，并假设 <code>caller</code> 和 <code>super</code> 都是正确的。那么我们知道以下语句为真： <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> 现在假设我们用 <code>sub</code> 替换 <code>super</code>，<code>sub</code> 也是正确的。这是我们已知为真的内容： <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> 那么 <code>caller</code> 何时仍然正确？当我们能填补链条中的“空缺”时，即如果 <code>super.Pre => sub.Pre</code> 且 <code>sub.Post => super.Post</code>。换句话说，如果 <code>sub</code> 的前置条件弱于（或等价于）<code>super</code> 的前置条件，且 <code>sub</code> 的后置条件强于（或等价于）<code>super</code> 的后置条件。 注意我从未实际说过 <code>sub</code> 是 <code>super</code> 的子类型！LSP 条件（至少 LSP 的契约规则）不仅适用于子类型，而且可以应用于任何我们用另一个函数或代码块替换一个函数或代码块的情况。子类型是这种情况的常见场景，但绝非唯一！我们还可以跨时间替换。每当我们修改某些代码的行为时，我们实际上是在用新版本替换旧版本，因此新版本的契约必须与旧版本的契约兼容，以保证现有代码不被破坏。 例如，假设我们维护一个 API 或函数，有两个必需输入 <code>X</code> 和 <code>Y</code>，以及一个可选输入 <code>Z</code>。将 <code>Z</code> 设为必需会加强前置条件（“输入必须有 Z”比“输入可能有 Z”更强），因此可能会破坏现有 API 用户。将 <code>Y</code> 设为可选会减弱前置条件（“输入可能有 Y”比“输入必须有 Y”更弱），因此保证兼容。 （这也支撑了<a href="https://en.wikipedia.org/wiki/Robustness_principle" target="_blank">鲁棒性原则</a>：“发送时要保守，接收时要开放”。） 这一切的阴暗面是<a href="https://www.hyrumslaw.com/" target="_blank">Hyrum 定律</a>。在下面的代码中，<code>new</code> 的后置条件是否比 <code>old</code> 的后置条件更强？ <div class="codehilite"><pre><code>def old(): return {"a": "foo", "b": "bar"} def new(): return {"a": "foo", "b": "bar", "c": "baz"} </code></pre></div> 乍看之下，这是一个加强的后置条件：<code>out.contains_keys([a, b, c]) => out.contains_keys([a, b])</code>。但接下来有人这样做了： <div class="codehilite"><pre><code>my_dict = {"c": "blat"} my_dict |= new() as</code></pre></div>

查看原文

查看缓存全文

缓存时间: 2026/05/16 03:40

# Liskov 替换原则比你想象的更强大来源：https://buttondown.com/hillelwayne/archive/the-liskov-substitution-principle-does-more-than 新年快乐！我已经结束了通讯停更期，准备尝试恢复每周更新。为了平稳过渡，我会先让文章更随性随意一些，至少等到*《面向程序员的逻辑》*（https://leanpub.com/logic/）完成。说到这个，v0.13 版本应该会在月底发布。那么本期通讯我想谈谈 **Liskov 替换原则**（https://en.wikipedia.org/wiki/Liskov_substitution_principle）（LSP）。上周我读了密码学家 Loupe Vaillant 的《A SOLID Load of Bull》（https://loup-vaillant.fr/articles/solid-bull），他在文中论证 OOP 的 **SOLID**（https://en.wikipedia.org/wiki/SOLID）原则不值得遵循。他对 LSP 网开一面，但又声称它“只是子类型化”，并且进一步说： > 如果我非要鸡蛋里挑骨头找 Liskov 替换原则的毛病，我会强调**它只适用于涉及继承的情况**，而继承本身已是一大禁忌。 LSP 比这有趣多了！在原始论文《A Behavioral Notion of Subtyping》（https://www.cs.cmu.edu/~wing/publications/LiskovWing94.pdf）中，Barbara Liskov 和 Jeannette Wing 首先将“正确的”子类型定义如下： > **子类型要求**：设 φ(x) 是一个关于类型 T 的对象 x 的可证明属性。那么 φ(y) 对于类型 S 的对象 y 也应成立，其中 S 是 T 的子类型。接下来，论文确定了子类型正确的*保证条件*¹（https://buttondown.com/hillelwayne/archive/the-liskov-substitution-principle-does-more-than#fn:safety）。他们指出了三个条件： 1. 子类型的每个方法与其对应的父类型方法相比，前置条件相同或更弱，后置条件相同或更强²（https://buttondown.com/hillelwayne/archive/the-liskov-substitution-principle-does-more-than#fn:cocontra）。 2. 子类型满足父类型的所有状态不变量。 3. 子类型满足父类型的所有“历史属性”³（https://buttondown.com/hillelwayne/archive/the-liskov-substitution-principle-does-more-than#fn:refinement），例如，如果父类型有一个不可变字段，子类型不能使其可变。（后来，Elisa Baniassad 和 Alexander Summers 意识到（https://www.cs.ubc.ca/~alexsumm/papers/BaniassadSummers21.pdf）这些条件等价于“子类型通过所有为父类型设计的黑盒测试”，我在这里（https://www.hillelwayne.com/post/lsp/）写过一点相关内容。）我想重点讨论第一条关于前置条件和后置条件的规则。这指的是方法的**契约**。对于一个函数 `f`，`f.Pre` 是进入函数时必须为真的条件，`f.Post` 是函数执行后保证的结果。一个典型的例子是平方根： ``` sqrt.Pre(x) = x >= 0 sqrt.Post(x, out) = out >= 0 && out*out == x ``` 数学上我们会写作 `all x: f.Pre(x) => f.Post(x)`（其中 `=>` 是蕴含运算符（https://en.wikipedia.org/wiki/Material_conditional））。如果对于所有 `x` 该关系都成立，我们就说这个函数是“正确的”。有了这个定义，我们可以从形式上推导出第一个子类型要求。让 `caller` 是使用某个方法（称为 `super`）的代码，并假设 `caller` 和 `super` 都是正确的。那么我们知道以下语句成立： ``` 1. caller.Pre && stuff => super.Pre 2. super.Pre => super.Post 3. super.Post && more_stuff => caller.Post ``` 现在假设我们将 `super` 替换为同样正确的 `sub`。此时我们知道的是： ``` 1. caller.Pre => super.Pre - 2. super.Pre => super.Post + 2. sub.Pre => sub.Post 3. super.Post => caller.Post ``` `caller` 在什么时候仍然正确？当我们可以填补链中的“缺口”时，即如果 `super.Pre => sub.Pre` 且 `sub.Post => super.Post`。换句话说，如果 `sub` 的前置条件比 `super` 的前置条件更弱（或等价），并且 `sub` 的后置条件比 `super` 的后置条件更强（或等价）。注意，我实际上从未说过 `sub` 是 `super` 的子类型！LSP 的条件（至少是契约规则的部分）不仅仅适用于*子类型*，而且可以适用于任何用一个函数或代码块替换另一个函数或代码块的情况。子类型化是常发生这种情况的地方，但绝不是唯一场景！我们也可以跨时间进行替换。每当我们修改某段代码的行为时，实际上就是用新版本替换旧版本，因此新版本的契约必须与旧版本兼容，以保证现有代码不被破坏。例如，假设我们维护一个 API 或函数，它有两个必填输入 `X` 和 `Y`，以及一个可选输入 `Z`。将 `Z` 改为必填会加强前置条件（“输入必须有 Z” 强于 “输入可以有 Z”），因此可能破坏现有 API 用户。将 `Y` 改为可选则会削弱前置条件（“输入可以有 Y” 弱于 “输入必须有 Y”），因此保证兼容。（这也支撑了**鲁棒性原则**（https://en.wikipedia.org/wiki/Robustness_principle）：“发送时要保守，接收时要开放”。）然而这一切的阴暗面是 **Hyrum 定律**（https://www.hyrumslaw.com/）。在下面这段代码中，`new` 的后置条件比 `old` 的后置条件更强吗？ ``` def old(): return {"a": "foo", "b": "bar"} def new(): return {"a": "foo", "b": "bar", "c": "baz"} ``` 乍一看，这是加强后的后置条件：`out.contains_keys([a, b, c]) => out.contains_keys([a, b])`。但有人可能会这样做： ``` my_dict = {"c": "blat"} my_dict |= new() assert my_dict[c] == "blat" ``` 哦不，他们的代码现在报错了！他们认为 `old` 的后置条件是“`out` 中不包含键 `c`”，然后基于那个后置条件编写了代码。从某种意义上说，*任何*后置条件的改变都可能*在某些人*那里引发问题。“你系统的所有可观测行为都会有人依赖”，正如 **Hyrum 定律**（https://www.hyrumslaw.com/）所说。所以我们需要明确地定义我们的后置条件究竟是什么，而那些不属于明确后置条件的输出属性，在下个版本中可能被违反。你可能会破坏某些人的工作流程，但你也有理由说“我警告过你了”。总而言之，Liskov 和 Wing 的工作是在子类型化的背景下进行的，但这些原则的适用范围更广，肯定不止于继承的使用。

里氏替换原则远超你的想象

相似文章

假设弱化性质

证明可能性

状态思维

# 结合语义等价自博弈与形式化验证提升 LLM 代码推理能力

语言实现破坏语言保证时，人们会感到困惑

提交意见反馈