In Eiffel a subtype literally cannot tighten an inherited precondition, while in Python or Kotlin an override can silently demand more than its parent did. Explain the mechanism behind that difference and what each approach costs.

## The specification, not the signature Most languages check that an override is *type*-compatible: the parameter types line up, the return type is compatible, visibility is not reduced. None of that says anything about the *conditions* the routine imposes. A subtype can keep a perfectly legal signature and still demand that the argument now be positive, or stop guaranteeing something the parent promised. That is a substitutability defect, and it is the part of the story that Design by Contract mechanises. (The principle itself belongs to the Liskov Substitution Principle; here the question is purely how languages implement it.) The two directions are: - **Preconditions may only be weakened.** A subtype may accept more than its parent, never less, because client code holding a parent-typed reference was written against the parent's requirement. - **Postconditions and invariants may only be strengthened.** A subtype may promise more, never less, because clients were told to expect at least the parent's guarantee. ## Enforcement by construction: Eiffel Eiffel does not add a checker that rejects a tightened clause. It removes the ability to write one. A redefined routine may not write a bare `require`; it writes `require else <extra>`, and the runtime evaluates `parent_clause or extra`. Symmetrically `ensure then <extra>` evaluates `parent_clause and extra`. Because the parent's clause is always a disjunct of the effective precondition, the effective precondition can only get looser as you descend; because the parent's postcondition is always a conjunct, the guarantee can only get tighter. A routine that omits the clauses entirely inherits them unchanged. This is the key insight to state in an interview: the language makes the illegal state unrepresentable at the *specification* level, exactly as a newtype does at the value level. There is no rule to remember, no lint to run and no way for a careless override to slip through review. ## The same idea with different scoping: Ada 2012 Ada 2012 added `Pre` and `Post` aspects, and then had to answer a question Eiffel never faced: Ada separates a subprogram from the tagged type it dispatches on. The answer is two spellings. `Pre'Class` and `Post'Class` are the *class-wide* contracts: they are inherited by every overriding subprogram, with `Pre'Class` combined by disjunction and `Post'Class` by conjunction, exactly as in Eiffel. A plain `Pre` is *specific*: it applies to that one body only, is not inherited, and is checked in addition. So in Ada the very same source line means one thing with the `'Class` suffix and something incompatible without it, and only the class-wide form participates in substitutability. Candidates who have only seen Eiffel are usually surprised by this. ## The same rules, no dispatch story: D D builds contracts into the language with `in`, `out` and `invariant` blocks. Inherited `in` contracts are combined disjunctively: if the base class's `in` block passes, the call proceeds even when the derived class's `in` block throws. `out` contracts are combined conjunctively — all of them must hold. Again the combination rule, not a diagnostic, does the work. ## No mechanism at all: Kotlin, Python, Java In Kotlin, `require(...)` in an override is an ordinary statement in an ordinary function body. Nothing links it to whatever the parent's body did. The same is true of Python's bare `assert`, of Java's `assert` and of hand-written `if (...) throw` guards. An override can therefore raise the bar in silence, and the failure will appear in production only when a client that had a parent-typed reference happens to pass a value the parent accepted. Python's third-party `icontract` restores the model deliberately — its decorators track inherited preconditions and weaken them by disjunction — which is itself evidence that the language does not. The practical consequence for a reviewer: in these languages, a tightened precondition in an override is a defect that only code review or a property test comparing subtype against supertype behaviour will catch. That is why the substitutability rule is taught as a principle in mainstream languages and as a keyword in Eiffel. ## What OR-ing does not buy you Mechanised weakening prevents one failure mode and creates another. Because the effective precondition is a disjunction, a subtype can write `require else True` and thereby accept every input — including inputs it has no sensible behaviour for. The contract is now technically weaker (legal) and practically useless, and the burden moves to the postcondition, which must still be at least as strong as the parent's for those newly accepted inputs. A subtype that widens acceptance without being able to deliver the inherited guarantee has broken the contract on the other side. So the honest summary is: Eiffel and Ada make the *direction* of change unmistakable and unforgeable, but no language can stop you from specifying something vacuous.