LSP 这么说
如果 q(x) 是关于 T 类型的对象 x 的可证明属性，那么 q(y) 对于 S 类型的对象 y 应该为真，其中 S 是 T 的子类型。
我可以改写如下：
q(x) 对 T 的任何 x 都为真 => q(y) 对 T 的任何子类型的任何 y 都为真
现在再说一句呢？
q(x) 对 T 的任何 x 都为真，q(y) 对 S 的任何 y 都为真 => S 是 T 的子类型
这有意义吗？我们可以将它用作subtype 的定义吗？
【问题讨论】：
标签： oop programming-languages types logic liskov-substitution-principle
q(x) is true for any x of T and q(y) is true for any y of S => S is a subtype of T
答案是否。该表达式的意思是可以定义 S 和 T 的通用超类型 R，然后 LSP（对这个名称如何成为主流感到羞耻）将适用于 T->R 和 S->R。
在类型理论中，有一些类型，其中包括语义，并且有一些遵守语义的类型的实现，可能是通过继承实现。
在实践中，指定类型语义（q(x) 部分）的唯一合理方法是通过实现，因此我们留下了 接口形式的无语义签名 ，以及类为了实现目的而继承，并实现他们喜欢的接口，没有办法检查他们是否正确地做到了。
研究试图定义形式语言来指定类型，因此工具可以检查实现是否遵守类型定义，但工作量太大，编译形式语言也一样好成可执行代码。这是我认为永远无法解决的Catch-22 情况。
回到你最初的问题，在允许今天所谓的“鸭子打字”的语言中，答案是不确定的，因为任何类型的对象都可以传递给任何函数，如果正确的签名是正确的，那么打字是正确的实施，结果是正确的。让我解释一下……
在像Eiffel 这样的语言中，您可以在List.append() 上放置一个后置条件，即List.length() 在操作后必须增加。这不是 Perl、JavaScript、Python 甚至 Java 等语言的工作方式。与更严格的类型定义相比，缺乏类型严格性允许代码更简洁。
【讨论】：
这没有意义；您使用 and 的语句在 S 和 T 中是对称的。
但我认为你的意思是说以下内容
如果对于任何命题 q 使得 q(x) 对所有
x类型为T是可证明的，那么 q(y) 对所有类型为S的 y: 也是可证明的，我们可能会认为S是T的子类型。
我更喜欢使用数学逻辑而不是非正式的英语，但如果我的定义正确，这就是行为子类型，现在通常被称为“鸭子类型”。这是一个非常好的子类型化原则，并且再次导致了这样一种想法，即在任何期望T 类型的值的上下文中，您可以改为提供S 类型的值，这没关系，因为S 类型的值是保证满足上下文所期望的所有属性。
【讨论】：
我认为不，您不能将其用作定义。此外，如果 q(x) 对 T 的任何 x 为真，并且 q(y) 对 S 的任何 y 都为真 这也可能意味着 T 是 S 的一个子类型。
要确定哪个是哪个子类型（假设您知道它们之间存在继承关系），您还必须知道哪个更“通用” 或者哪个比另一个更“专业”。
【讨论】：