Substitution Principle and Pre/Post Conditions

exercises
tutorial
java
solid
specification

Applied class for 2026-04-30-generics-in-java (Week 9). More practice applying the Liskov Substitution Principle (see java-solid-principles) and pre/postconditions (see java-specification).

Predicate strength

A B
1 a < 0 && b < 0 a != 0 && b < 0
2 a instanceof Animal a instanceof String
3 a instanceof Animal \|\| b instanceof Zebra a instanceof Animal && b instanceof Zebra
4 a instanceof Animal && b instanceof Zebra a instanceof Animal
5 a instanceof Animal && b instanceof Object a instanceof Animal
6 a instanceof Zebra a instanceof Tiger

For each row, identify which column is a stronger (more restrictive) condition, or state that there’s no relation.

  1. A is stronger than B — a < 0 && b < 0 implies a != 0 && b < 0 (every a < 0 is also a != 0), but not vice versa.
  2. No relation — Animal and String are unrelated types; neither instance check implies the other.
  3. B is stronger than A — A only needs either condition to hold (a looser OR), while B requires both (a stricter AND) — satisfying B always satisfies A, not the reverse.
  4. A is stronger than B — A requires everything B requires, plus more (b instanceof Zebra on top of a instanceof Animal).
  5. A looks stronger than B, but they’re equivalent — since everything is an instance of Object, b instanceof Object is always true, so it adds no actual restriction.
  6. No relation — Zebra and Tiger are siblings (both presumably subtypes of Animal, say), so neither instance check implies the other.

Now consider two possible class structures:

// Option 1: Preconditions
class ClassA {
    /** @requires A */
    void f(Object a, Object b) {}
}
class ClassB extends ClassA {
    /** @requires B */
    void f(Object a, Object b) {}
}
// Option 2: Postconditions
class ClassA {
    /** @ensures A */
    void f(Object a, Object b) {}
}
class ClassB extends ClassA {
    /** @ensures B */
    void f(Object a, Object b) {}
}

For each row above, if column A and column B are inserted as the specification text, which option (if any) satisfies the substitution principle?

Recall: a subclass must not strengthen preconditions (they may only stay the same or weaken) and must not weaken postconditions (they may only stay the same or strengthen).

  1. Option 1 (precondition) — ClassB’s precondition (B) is weaker than ClassA’s (A), which is allowed for preconditions.
  2. Neither — unrelated conditions satisfy neither the “no stronger precondition” nor “no weaker postcondition” rule.
  3. Option 2 (postcondition) — ClassB’s postcondition (B) is stronger than ClassA’s (A), which is allowed for postconditions.
  4. Option 1 (precondition) — same reasoning as row 1: B is weaker than A.
  5. Both — since A and B are equivalent here, substituting either as precondition or postcondition preserves the (unchanged) strength relationship.
  6. Neither — unrelated conditions again satisfy neither rule.

Substitution principle

class X {
    /**
     * @require fontSize >= 5
     * @ensure \result >= 0
     */
    int detexify(Object symbol, float fontSize) { ... }
}

class Y extends X {
    /**
     * @require fontSize > 0
     * @ensure \result > 0
     */
    int detexify(Object symbol, float fontSize) { ... }
}

class Z extends X {
    /**
     * @require fontSize > 5
     * @ensure \result > 0
     */
    int detexify(Object symbol, float fontSize) { ... }
}

Why would a programmer choose to use a precondition at all?

As a restriction on the allowable range of inputs, to avoid having to handle huge positive/negative numbers (or other awkward edge cases) inside the method body.

Does Y violate the substitution principle?

No. Y’s precondition (fontSize > 0) is weaker than X’s (fontSize >= 5 implies fontSize > 0, but not vice versa — the range of acceptable inputs expanded), and Y’s postcondition (\result > 0) is stronger than X’s (\result >= 0 — the range of possible outputs contracted). Both changes are allowed by the substitution principle.

Does Z violate the substitution principle?

Yes. Z’s postcondition is correctly stronger (\result > 0 vs. \result >= 0), but its precondition (fontSize > 5) is also stronger than X’s (fontSize >= 5) — it forbids fontSize == 5, which X explicitly allowed. Strengthening a precondition violates the principle, regardless of what happens to the postcondition.

Writing pre/postconditions

public boolean q2(String[] strArray, int firstIndex, int secondIndex) {
    return strArray[firstIndex] == strArray[secondIndex];
}

Write a Javadoc comment for q2.

/**
 * Determines if two indicated elements of an array of Strings
 * refer to the same String object.
 *
 * @param strArray an array of Strings
 * @param firstIndex index of the first element to compare
 * @param secondIndex index of the second element to compare
 * @return true if the indicated elements in the array refer to
 *         the same string, false otherwise
 */

Add @requires/@ensures tags.

/**
 * ...
 * @requires strArray != null && 0 <= firstIndex < strArray.length
 *               && 0 <= secondIndex < strArray.length
 * @ensures \result == true
 *              <==> strArray[firstIndex] == strArray[secondIndex]
 */

Specify that q2 does not change any elements of strArray.

/**
 * ...
 * @ensures \forall int i; 0 <= i && i < strArray.length
 *              ==> \old(strArray)[i] == strArray[i]
 */