这个先决条件是否违反了里氏替换原则

Question

我有 3 个班级，Account, CappedAccount, UserAccount,

CappedAccount，并且UserAccount都扩展Account。

Account 包含以下内容：

abstract class Account {
   ...
   /**
   * Attempts to add money to account.
   */
   public void add(double amount) {
      balance += amount;
   }
}

CappedAccount 覆盖此行为：

public class CappedAccount extends Account {
   ...
   @Override
   public void add(double amount) {
      if (balance + amount > cap) { // New Precondition
         return;
      }
      balance += amount;
   }
}

UserAccount不会覆盖来自 的任何方法Account，因此不需要说明。

我的问题是，是否CappedAccount#add违反了 LSP，如果确实如此，我如何设计它以符合 LSP。

例如，是否add()在CappedAccount计数为“加强先决条件”？

Answer 1

太长了；

if (balance + amount > cap) {
    return;
}

不是先决条件而是不变量，因此（就其本身而言）不违反里氏替换原理。

现在，真正的答案。

真正的前提条件是（伪代码）：

[requires] balance + amount <= cap

您应该能够强制执行此前提条件，即检查条件并在不满足时引发错误。如果您确实强制执行前提条件，您将看到 LSP 被违反：

Account a = new Account(); // suppose it is not abstract
a.add(1000); // ok

Account a = new CappedAccount(100); // balance = 0, cap = 100
a.add(1000); // raise an error !

子类型的行为应与其父类型类似（见下文）。

“强化”前提的唯一方法是强化不变量。因为在每次方法调用之前和之后不变式都应该为真。强化不变量不会（就其自身而言）违反 LSP，因为不变量在方法调用之前免费给出：它在初始化时为真，因此在第一次方法调用之前为真。因为它是一个不变量，所以在第一次方法调用后它是正确的。并且一步一步，在下一个方法调用之前始终为真（这是数学归纳法...）。

class CappedAccount extends Account {
    [invariant] balance <= cap
}

在方法调用之前和之后，不变量应该为 true：

@Override
public void add(double amount) {
    assert balance <= cap;
    // code
    assert balance <= cap;
}

您将如何在该add方法中实现它？你有一些选择。这个还可以：

@Override
public void add(double amount) {
    assert balance <= cap;
    if (balance + amount <= cap) {
        balance += cap;
    }
    assert balance <= cap;
}

嘿，但这正是你所做的！（有一点细微的差别：这个有一个出口来检查不变量。）

这也是，但语义不同：

@Override
public void add(double amount) {
    assert balance <= cap;
    if (balance + amount > cap) {
        balance = cap;
    } else {
        balance += cap;
    }
    assert balance <= cap;
}

这也是，但语义是荒谬的（或者是一个封闭的帐户？）：

@Override
public void add(double amount) {
    assert balance <= cap;
    // do nothing
    assert balance <= cap;
}

好的，您添加了一个不变量，而不是前提条件，这就是不违反 LSP 的原因。回答结束。

但是......这并不令人满意：add“尝试向帐户添加资金”。我想知道是否成功！！让我们在基类中尝试一下：

/**
* Attempts to add money to account.
* @param amount  the amount of money
* @return True if the money was added.
*/
public boolean add(double amount) {
    [requires] amount >= 0
    [ensures] balance = (result && balance == old balance + amount) || (!result && balance == old balance)
}

以及实现，具有不变性：

/**
* Attempts to add money to account.
* @param amount  the amount of money
* @return True is the money was added.
*/
public boolean add(double amount) {
    assert balance <= cap;
    assert amount >= 0;
    double old_balance = balance; // snapshot of the initial state
    bool result;
    if (balance + amount <= cap) {
        balance += cap;
        result = true;
    } else {
        result = false;
    }
    assert (result && balance == old balance + amount) || (!result && balance == old balance)
    assert balance <= cap;
    return result;
}

当然，没有人会编写这样的代码，除非您使用 Eiffel（这可能是个好主意），但您会看到这个想法。这是一个没有所有条件的版本：

public boolean add(double amount) {
    if (balance + amount <= cap) {
        balance += cap;
        return true;
    } else {
        return false;
}

请注意 LSP 的原始版本（“如果对于每个类型o_1的对象S，都有一个o_2类型的对象T，使得对于P以 定义的所有程序，当被替换为时T， 的行为P保持不变，则是 的子类型”）被侵犯了。您必须定义适用于每个程序的方法。选择一顶帽子，比方说。我将编写以下程序：o_1o_2STo_21000

Account a = ...
if (a.add(1001)) {
    // if a = o_2, you're here
} else {
    // else you might be here.
}

这不是问题，因为当然，每个人都使用 LSP 的弱化版本：我们不希望行为保持不变（子类型的兴趣有限，例如性能，想想数组列表与链表）），我们希望保留“该程序的所有理想属性”（请参阅​​此问题）。