Is this precondition a violation of the Liskov Substitution Principle

Question

I have 3 classes, Account, CappedAccount, UserAccount,

CappedAccount, and UserAccount both extend Account.

Account contains the following:

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

CappedAccount overrides this behavior:

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

UserAccount doesn't override any methods from Account, so it doesn't need to be stated.

My question is, does CappedAccount#add violate LSP, and if it does, how can I design it to comply with LSP.

For example, does add() in CappedAccount count as "strengthening preconditions"?

Answer 1

It's important to remember the LSP covers both syntax and semantics. It covers both what the method is coded to do, and what the method is documented to do. This means vague documentation can make it difficult to apply the LSP.

How do you interpret this?

Attempts to add money to account.

It's clear the add() method is not guaranteed to add money to the account; so the fact that CappedAccount.add() may not actually add money seems acceptable. But there is no documentation of what should be expected when an attempt to add money fails. Since that use case is undocumented, "do nothing" seems like an acceptable behavior, and therefore we have no LSP violation.

To be on the safe side, I would amend the documentation to define expected behavior for a failed add() i.e. explicitly define the post-condition. Since the LSP covers both syntax and semantics, you can fix a violation by modifying either one.

Answer 2

TLDR;

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

is not a precondition but an invariant, hence not a violation (on his own) of the Liskov Substition Principle.

Now, the actual answer.

A real precondition would be (pseudo code):

[requires] balance + amount <= cap

You should be able to enforce this precondition, that is check the condtion and raise an error if it is not met. If you do enforce the precondition, you'll see that the LSP is violated:

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 !

The subtype should behave like its supertype (see below).

The only way to "strengthen" the precondition is to strenghten the invariant. Because the invariant should be true before and after each method call. The LSP is not violated (on his own) by a strengthened invariant, because the invariant is given for free before the method call: it was true at the initialisation, hence true before the first method call. Because it's an invariant, it is true after the first method call. And step by step, is always true before the next method call (this is a mathematicual induction...).

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

The invariant should be true before and after the method call:

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

How would you implement that in the add method? You have some options. This one is ok:

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

Hey, but that's exactly what you did! (There is a slight difference: this one has one exit to check the invariant.)

This one too, but the semantic is different:

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

This one too but the semantic is absurd (or a closed account?):

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

Okay, you added an invariant, not a precondition, and that's why the LSP is not violated. End of the answer.

---

But... this is not satisfying: add "attempts to add money to account". I would like to know if it was a success!! Let's try this in the base class:

/**
* 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)
}

And the implementation, with the invariant:

/**
* 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;
}

Of course, nobody writes code like that, unless you use Eiffel (that might be a good idea), but you see the idea. Here's a version without all the conditions:

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

Please note the the LSP in its original version ("If for each object o_1 of type S there is an object o_2 of type T such that for all programs P defined in terms of T, the behavior of P is unchanged when o_1 is substituted for o_2, then S is a subtype of T") is violated. You have to define o_2 that works for each program. Choose a cap, let's say 1000. I'll write the following program:

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

That's not a problem because, of course, everyone uses a weaken version of the LSP: we don't want the beahvior to be unchanged (subtype would have a limited interest, performance for instance, think of array list vs linked list)), we want to keep all "the desirable properties of that program" (see this question).