3

Liskov 替换原则指出：

超类型的不变量必须保留在子类型中。

我对这个原理和多态性的交集特别感兴趣。但实际上，特别是子类型多态性，参数多态性和 Haskell 类型类似乎就是这种情况。

所以，我知道函数是子类型，当它们的参数是逆变的并且它们的返回类型是协变的。我们可以假设方法只是带有隐式“self”参数的函数。但是，这似乎暗示如果子类覆盖父类的方法，则它不再是子类型，因为其中一个方法不再是子类型。

例如。采用以下伪代码：

class Parent:
    count : int
    increment : Parent -> ()
    {
        count += 1
    }

class Child inherits Parent:
    increment : Child -> ()
    {
        count += 2
    }

所以回到 LSP：我们可以说即使这两个不遵循严格的子类型关系，属性 也Parent.increment()应该成立吗？Child.increment()

更一般地说，我的问题是：子类型化规则如何与多态函数的更具体的参数接口，以及将这两个概念结合在一起的正确思考方式是什么？

4

2 回答 2

0

引用维基百科关于Liskov 替换原则的文章

更正式地说，Liskov 替换原则 (LSP) 是子类型关系的特定定义，称为（强）行为子类型[...]

行为子类型比类型论中定义的函数的典型子类型更强大，后者仅依赖于参数类型的逆变性和返回类型的协变。行为子类型通常是难以确定的 [...]

亚型必须满足许多行为条件：

  • 先决条件不能在子类型中得到加强。
  • 后置条件不能在子类型中被削弱。
  • 超类型的不变量必须保留在子类型中。

因此，LSP 是对子类型的更强有力的定义，它依赖于类型理论之外的特征。

在您的示例中，这取决于您的不变量。

calling increment will increase count by **exactly 1**

显然Child不能用Parent表示，因为不变量被破坏了。这不能仅从语法中推断出来。

LSP 应该引导您分别定义 Parent 和 Child，让它们都继承自Incrementable具有较弱的后置条件。

于 2014-07-25T09:49:16.620 回答
0

术语“子类型”在技术上是一个语法问题。所以从句法上讲，Child <: Parent.

如维基百科所述，Liskov 原则是关于行为子类型化的。它需要句法子类型，但它也取决于您对类的不变量和前置/后置条件的定义。由于您没有定义任何内容，因此谈论违规行为是荒谬的。

如果将increment的后置条件定义为new count = old count + 1，则存在违规。

如果您将increment的后置条件定义为new count > old count，则没有。

通常，将后置条件定义为“完全是父级的后置条件”使得定义不可能包含多态性。在多态有意义的地方，后置条件的定义应该放宽。

请注意，类不变量是关于可能的值 - 对象的快照 - 并且由于您可以increment根据 Parent's定义 Child's increment，因此它不会违反任何不变量。

于 2014-07-31T15:53:29.453 回答