里氏替换原则

里氏替代原则 (LSP) 是子类型关系的特定定义，称为强行为子类型，最初由 Barbara Liskov 在 1988 年题为数据抽象和层次结构的会议主题演讲中引入。

它基于可替换性的概念——面向对象编程中的一个原则，指出一个对象（例如一个类）可以被一个子对象（例如一个扩展第 一个类的类）替换而不会破坏程序。

它是一种语义关系，而不仅仅是句法关系，因为它旨在保证层次结构中类型（尤其是对象类型）的语义互操作性。

芭芭拉·利斯科夫 (Barbara Liskov) 和珍妮特·温 (Jeannette Wing) 在 1994 年的一篇论文中简要描述了该原理，如下所示：

子类型要求：设 ϕ ( x ) {displaystyle phi (x)} 是关于类型 T 的对象 x {displaystyle x} 的可证明属性。然后 ϕ ( y ) {displaystyle phi (y )} 对于类型 S 的对象 y {displaystyle y} 应该为真，其中 S 是 T 的子类型。

也就是说，如果 S 是 T 的子类型，则适用于 T 对象的内容也适用于 S 对象。在同一篇论文中，Liskov 和 Wing 在 Hoare 逻辑的扩展中详细描述了他们的行为子类型概念，这与 Bertrand Meyer 有一定的相似之处 的契约设计，因为它考虑了子类型与先决条件、后置条件和不变量的相互作用。

Liskov 的行为子类型概念定义了对象可替代性的概念； 也就是说，如果 S 是 T 的子类型，则程序中类型 T 的对象可以替换为类型 S 的对象，而不会改变该程序的任何所需属性（例如正确性）。

行为子类型化是比类型论中定义的典型函数子类型化更强大的概念，后者仅依赖于参数类型的逆变性和返回类型的协变性。

行为子类型通常是不可判定的：如果 q 是 x 的属性方法总是终止，那么程序（例如编译器）不可能验证它对 T 的某些子类型 S 是否成立，即使 q 对 T 成立。尽管如此，该原则在推理类层次结构的设计时还是很有用的。

里氏替代原则对更新的面向对象编程语言中采用的签名施加了一些标准要求：

• 子类型中方法参数类型的逆变。
• 子类型中方法返回类型的协变。
• 子类型中的方法不能抛出新异常，除非它们是超类型方法抛出的异常的子类型。

除了签名要求外，子类型还必须满足许多行为条件。这些在类似于契约设计方法的术语中进行了详细说明，从而导致对契约如何与继承交互的一些限制：

• 前提条件不能在子类型中加强。
• 不能在子类型中弱化后置条件。
• 子类型中必须保留不变量。
• 历史约束（历史规则）。对象被认为只能通过它们的方法（封装）进行修改。因为子类型可能会引入超类型中不存在的方法，所以这些方法的引入可能会允许子类型中的状态更改，而这在超类型中是不允许的。历史约束禁止这样做。这是 Liskov 和 Wing 引入的新颖元素。可以通过将可变点定义为不可变点的子类型来举例说明违反此约束的情况。这违反了历史约束，因为在不可变点的历史中，创建后状态始终相同，因此它不能包含一般可变点的历史。但是，可以安全地修改添加到子类型的字段，因为它们无法通过超类型方法观察到。因此，可以在不违反历史约束的情况下，将具有不可变中心和可变半径的圆定义为不可变点的子类型。

前置条件和后置条件的规则与 Bertrand Meyer 在其 1988 年出版的《面向对象的软件构造》一书中介绍的规则相同。

Meyer 和后来第 一个使用行为子类型化术语的 Pierre America 都给出了一些行为子类型化概念的证明理论定义，但他们的定义没有考虑支持引用或指针的编程语言中可能出现的别名。

考虑别名是 Liskov 和 Wing (1994) 所做的主要改进，其中一个关键因素是历史约束。根据 Meyer 和 America 的定义。