Loading learning content...
If preconditions are the caller's promises to the method, postconditions are the method's promises to the caller. They complete the contract, defining what the caller can rely on after the method returns.
A postcondition is a logical assertion that must be true at the moment a method completes execution, assuming all preconditions were satisfied. It defines the guaranteed outcomes — what the method commits to delivering.
Consider the symmetry:
| Direction | Promise Type | Example |
|---|---|---|
| Caller → Method | Precondition | "I promise amount > 0" |
| Method → Caller | Postcondition | "I promise balance will decrease by amount" |
When you call withdraw(100) on a bank account with $500, the method's postcondition guarantees that afterward, balance == 400. Not 399. Not "approximately 400." Exactly 400. This guarantee is what allows you to write correct code without inspecting the method's implementation.
This page explores postconditions in depth, culminating in the critical LSP rule: subclasses may strengthen postconditions but must never weaken them — the mirror image of the precondition rule.
By the end of this page, you will: • Understand postconditions as formal guarantees that methods make to callers • Recognize postconditions in real-world code (return values, state changes, side effects) • Master the LSP rule: subclasses may strengthen but never weaken postconditions • Know how to design, document, and verify postconditions in your code • Understand the relationship between postconditions, defensive programming, and robust design
A postcondition is a logical assertion that must be true at the moment a method successfully completes, given that all preconditions were satisfied when the method began. It defines what the method guarantees to accomplish.
Postconditions answer the question: "What can I promise you will be true when I'm done?"
Let's revisit our bank account example with explicit postconditions:
12345678910111213141516171819202122232425262728
class BankAccount { private balance: number; /** * Withdraws the specified amount from the account. * * @param amount The amount to withdraw * @precondition amount > 0 * @precondition amount <= this.balance * * @postcondition this.balance == old(this.balance) - amount * @postcondition return value is the withdrawn amount * @postcondition transaction is logged in history */ withdraw(amount: number): number { const previousBalance = this.balance; this.balance -= amount; this.transactionHistory.push({ type: 'withdrawal', amount }); // All postconditions are now satisfied: // ✓ balance == previousBalance - amount // ✓ returning the amount // ✓ transaction logged return amount; }}This withdraw method has three postconditions:
balance == old(balance) - amount — The balance is exactly reduced by the withdrawal amountIf any of these postconditions fail, the method implementation is buggy, even if it doesn't crash. A method that withdraws $100 but only decreases the balance by $99 violates its postcondition — it broke its contract.
In contract specifications, old(expression) refers to the value of expression at the moment the method started executing — before any changes occurred.
this.balance == old(this.balance) - amount means: "After the method completes, the balance equals whatever the balance was before, minus the withdrawal amount."
This notation lets us express relationships between pre-execution and post-execution state.
Postconditions can describe various aspects of a method's effects. Let's categorize them:
| Category | Description | Example |
|---|---|---|
| Return Value | Constraints on what the method returns | return >= 0 (non-negative result) |
| Object State Change | How the object's fields are modified | this.size == old(this.size) + 1 |
| Relationship Preservation | Invariants maintained or relationships held | this.items is still sorted |
| Side Effects | Observable effects on external systems | log file contains new entry |
| Exception Guarantees | What's true if the method throws | if throws, state unchanged (strong guarantee) |
| Ordering Guarantees | Relative ordering of elements | returned list is sorted ascending |
Let's examine each category with realistic examples:
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137
// ═══════════════════════════════════════════════════════════════// RETURN VALUE POSTCONDITIONS// What the method returns, and constraints on that return// ═══════════════════════════════════════════════════════════════ class MathUtils { /** * @postcondition return >= 0 (absolute value is non-negative) */ abs(n: number): number { return n >= 0 ? n : -n; } /** * @postcondition return >= Math.min(a, b) * @postcondition return <= Math.max(a, b) * @postcondition return is the value closest to target */ clamp(value: number, min: number, max: number): number { return Math.max(min, Math.min(max, value)); } /** * @postcondition return * return == n (for perfect squares) * @postcondition return >= 0 */ sqrt(n: number): number { return Math.sqrt(n); }} // ═══════════════════════════════════════════════════════════════// OBJECT STATE CHANGE POSTCONDITIONS// How the object is modified// ═══════════════════════════════════════════════════════════════ class Stack<T> { private items: T[] = []; /** * @postcondition this.size() == old(this.size()) + 1 * @postcondition this.peek() == item */ push(item: T): void { this.items.push(item); } /** * @postcondition this.size() == old(this.size()) - 1 * @postcondition return == old(this.peek()) */ pop(): T { return this.items.pop()!; } /** * @postcondition this.isEmpty() == true * @postcondition this.size() == 0 */ clear(): void { this.items = []; }} // ═══════════════════════════════════════════════════════════════// RELATIONSHIP PRESERVATION POSTCONDITIONS// Invariants that the method maintains// ═══════════════════════════════════════════════════════════════ class SortedList<T> { private items: T[] = []; /** * @postcondition this.items remains sorted in ascending order * @postcondition element is in this.items */ insert(element: T): void { // Find correct position and insert const index = this.findInsertPosition(element); this.items.splice(index, 0, element); // Postcondition: sortedness preserved } /** * @postcondition return is sorted ascending * @postcondition all elements from original are in return */ toArray(): T[] { return [...this.items]; // Returns sorted copy }} // ═══════════════════════════════════════════════════════════════// SIDE EFFECT POSTCONDITIONS// Observable effects beyond the object itself// ═══════════════════════════════════════════════════════════════ class AuditedRepository { /** * @postcondition user is saved in database * @postcondition audit log contains entry for this save * @postcondition 'user.created' event is published */ async saveUser(user: User): Promise<void> { await this.database.save(user); await this.auditLog.record('user_saved', user.id); await this.eventBus.publish('user.created', user); }} // ═══════════════════════════════════════════════════════════════// EXCEPTION SAFETY POSTCONDITIONS// What's guaranteed if the method throws// ═══════════════════════════════════════════════════════════════ class TransactionalAccount { /** * Transfers money between accounts. * * @postcondition SUCCESS: from.balance decreased, to.balance increased * @postcondition EXCEPTION: both balances unchanged (strong guarantee) */ transfer(from: Account, to: Account, amount: number): void { const originalFrom = from.balance; const originalTo = to.balance; try { from.withdraw(amount); to.deposit(amount); } catch (e) { // Rollback to maintain strong exception guarantee from.balance = originalFrom; to.balance = originalTo; throw e; } }}C++ defines three levels of exception safety that apply broadly:
No-throw guarantee: Method never throws exceptions (strongest) Strong exception guarantee: If exception thrown, state is unchanged (rollback) Basic exception guarantee: If exception thrown, no leaks/corruption, but state may change
Document which guarantee your methods provide. It's a critical postcondition.
Now we reach the heart of postconditions in LSP. When a subclass overrides a method, how must it handle the parent's postconditions?
The rule is the mirror image of the precondition rule:
A subclass may strengthen (tighten) postconditions but must never weaken (loosen) them.
This means a subclass must deliver at least what the parent promised, but can promise more. The subclass can never deliver less than what the parent guaranteed. Let's understand why.
If S is a subtype of T, and method m in T has postcondition Q_T, then the overriding method m in S must have a postcondition Q_S such that:
Q_S ⟹ Q_T (Q_S implies Q_T)
In other words: the child's postcondition must be at least as strong as the parent's. Everything the parent guaranteed must still be true, plus the child can add more guarantees.
Why does weakening postconditions break LSP?
Consider this scenario:
12345678910111213141516171819202122232425262728293031323334353637383940414243444546474849505152535455565758596061626364656667686970717273747576777879808182
// ═══════════════════════════════════════════════════════════════// BASE CLASS: Reliable search with guaranteed return// ═══════════════════════════════════════════════════════════════ class Collection<T> { protected items: T[] = []; /** * Finds and returns an item matching the predicate. * * @precondition true (accepts any predicate) * @postcondition if item found: returns the item * @postcondition if not found: returns null * @postcondition original collection unchanged */ find(predicate: (item: T) => boolean): T | null { for (const item of this.items) { if (predicate(item)) return item; } return null; // Guaranteed: returns null if not found }} // ═══════════════════════════════════════════════════════════════// ❌ LSP VIOLATION: Weakened postcondition// ═══════════════════════════════════════════════════════════════ class CachedCollection<T> extends Collection<T> { private cache: Map<string, T> = new Map(); /** * @postcondition if item found: returns the item * @postcondition if not found: may return null OR throw // ⚠️ WEAKENED! */ find(predicate: (item: T) => boolean): T | null { // Check cache first const cacheKey = predicate.toString(); if (this.cache.has(cacheKey)) { return this.cache.get(cacheKey)!; } // If not in cache and cache is corrupted, throw if (this.isCacheCorrupted()) { throw new Error("Cache corrupted"); // ❌ Parent promised null! } const result = super.find(predicate); if (result) this.cache.set(cacheKey, result); return result; }} // ═══════════════════════════════════════════════════════════════// Client code written against the base class// ═══════════════════════════════════════════════════════════════ function findUserOrCreateDefault(collection: Collection<User>): User { // Client RELIES on the postcondition: returns null if not found const user = collection.find(u => u.name === "admin"); if (user === null) { // Parent's postcondition guarantees we reach here if not found return createDefaultAdmin(); } return user;} // ═══════════════════════════════════════════════════════════════// The substitution problem// ═══════════════════════════════════════════════════════════════ // This works perfectly:const standard = new Collection<User>();findUserOrCreateDefault(standard); // ✅ Gets null, creates default // This breaks:const cached = new CachedCollection<User>();findUserOrCreateDefault(cached); // ❌ May THROW instead of returning null! // Client code that correctly handles the parent's contract is broken// because the child WEAKENED what it promises.The violation is clear: Client code relies on the Collection contract: "returns null if not found." It handles null correctly. But CachedCollection sometimes throws instead of returning null—that's less than what was promised. The client's null-handling code never executes for failures that throw.
Now let's see the correct approach—strengthening postconditions:
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101
// ═══════════════════════════════════════════════════════════════// BASE CLASS: Returns nullable result// ═══════════════════════════════════════════════════════════════ class Parser { /** * Parses the input into a structured document. * * @postcondition returns Document if valid, null if invalid */ parse(input: string): Document | null { try { return this.doParse(input); } catch { return null; } } protected doParse(input: string): Document { // Basic parsing... return new Document(input); }} // ═══════════════════════════════════════════════════════════════// ✅ LSP COMPLIANT: Strengthened postcondition// ═══════════════════════════════════════════════════════════════ class StrictParser extends Parser { /** * @postcondition returns Document (never null!) * @postcondition throws ParseError if invalid (instead of null) * * This STRENGTHENS: parent returns Document|null, * child guarantees Document (stronger — fewer possible outcomes) */ parse(input: string): Document { const result = super.parse(input); if (result === null) { // Convert "weak" null to "strong" exception with details throw new ParseError("Invalid input", this.analyzeFaiure(input)); } return result; }} // Wait — doesn't this break client code expecting null? // ═══════════════════════════════════════════════════════════════// Actually, it's STILL LSP-compliant! Here's why:// ═══════════════════════════════════════════════════════════════ function processDocument(parser: Parser): void { const doc = parser.parse("some input"); if (doc === null) { console.log("Parse failed, using default"); return; } // Use doc console.log(doc.title);} // With StrictParser:// - If valid input: returns Document ✅ (client proceeds to use doc)// - If invalid input: throws before returning ⚠️ // The subtle point: StrictParser still SATISFIES the postcondition// "returns Document if valid, null if invalid" because:// - It returns Document when valid ✅// - It never returns null when valid ✅// - When invalid, it throws BEFORE returning, so the postcondition// about the return value doesn't apply (method didn't complete normally) // ═══════════════════════════════════════════════════════════════// Better example: truly strengthened postcondition// ═══════════════════════════════════════════════════════════════ class Repository { /** * @postcondition returns list (may be empty) */ findAll(): User[] { return this.db.query("SELECT * FROM users"); }} class CachedRepository extends Repository { /** * @postcondition returns list (may be empty) * @postcondition result is sorted by name (NEW, STRONGER!) * @postcondition result is deduplicated (NEW, STRONGER!) */ findAll(): User[] { const users = super.findAll(); return this.sortAndDeduplicate(users); // Client gets AT LEAST what parent promised (a list) // PLUS extra guarantees (sorted, deduped) }}When postconditions are properly strengthened (or kept the same): • Every guarantee the parent made is STILL true • Client code can rely on exactly what it expected • Substitution is always safe — clients get what they asked for (or more)
The subclass delivers "at least as much" as promised, never less.
The postcondition rule becomes intuitive when visualized. Think of postconditions as defining "possible outcome regions." Let's visualize:
The geometry is the opposite of preconditions:
Clients write code that handles the parent's possible outcomes. If a subclass adds NEW possible outcomes the client doesn't expect, things break.
T | null → T (never null now)number → positive number (constrained range)list → sorted list (extra property)eventually consistent → immediately consistentmay have duplicates → no duplicatesT → T | null (might return null now)positive number → number (could be negative)sorted list → list (no ordering guarantee)immediately consistent → eventually consistentno duplicates → may have duplicatesNow we can see the beautiful symmetry of Design by Contract and LSP. The rules are opposites because preconditions and postconditions serve opposite roles:
| Aspect | Preconditions | Postconditions |
|---|---|---|
| Define | What method requires (inputs) | What method guarantees (outputs) |
| Fulfilled by | Caller | Method |
| Safe change | Accept MORE inputs (weaken) | Promise MORE results (strengthen) |
| Dangerous change | Reject inputs (strengthen) | Deliver less (weaken) |
| LSP Rule | Subclass may weaken, never strengthen | Subclass may strengthen, never weaken |
| Reasoning | Clients send valid parent inputs | Clients expect parent's outcomes |
The underlying principle is substitutability:
A subclass is a valid substitute if it:
The subclass can be "more generous" on both ends:
But it can never be less generous:
12345678910111213141516171819202122232425262728293031323334353637383940414243444546
// ═══════════════════════════════════════════════════════════════// PERFECT LSP-COMPLIANT SUBCLASS// Weaker preconditions + Stronger postconditions// ═══════════════════════════════════════════════════════════════ class DataProcessor { /** * @precondition data.length > 0 (must have at least one element) * @postcondition returns number (may be any number) */ process(data: number[]): number { return data.reduce((a, b) => a + b, 0) / data.length; }} class RobustDataProcessor extends DataProcessor { /** * @precondition true (accepts empty arrays too!) // WEAKER ✅ * @postcondition returns non-negative number // STRONGER ✅ * @postcondition returns 0 for empty input // STRONGER ✅ */ process(data: number[]): number { if (data.length === 0) return 0; // Handle case parent couldn't const result = super.process(data); return Math.abs(result); // Guarantee non-negative }} // ═══════════════════════════════════════════════════════════════// LSP Analysis:// ═══════════════════════════════════════════════════════════════ // PRECONDITION:// Parent requires: data.length > 0// Child requires: true (anything)// Is parent ⟹ child? YES! (length > 0 implies true)// Valid weakening ✅ // POSTCONDITION:// Parent promises: some number// Child promises: non-negative number, 0 for empty// Is child ⟹ parent? YES! (non-negative implies it's a number)// Valid strengthening ✅ // This subclass is a PERFECT substitute!Think of it this way: • Preconditions: The subclass says "Don't worry, I can handle even MORE cases than parent!" • Postconditions: The subclass says "Don't worry, I guarantee even BETTER results than parent!"
In both cases, the subclass is making the client's life easier, never harder.
Let's examine postcondition patterns you'll encounter in real systems:
Factory methods have postconditions about what they create:
12345678910111213141516171819202122232425262728293031323334353637383940414243
abstract class ConnectionFactory { /** * @postcondition returns open, valid connection * @postcondition connection is ready for queries */ abstract createConnection(config: Config): Connection;} // ═══════════════════════════════════════════════════════════════// ✅ Strengthened: returns connection with more guarantees// ═══════════════════════════════════════════════════════════════ class PooledConnectionFactory extends ConnectionFactory { /** * @postcondition returns open, valid connection * @postcondition connection is ready for queries * @postcondition connection is from pool (reusable) // STRONGER * @postcondition connection has health-check passed // STRONGER */ createConnection(config: Config): Connection { const conn = this.pool.acquire(); if (!conn.healthCheck()) { conn.reconnect(); } return conn; }} // ═══════════════════════════════════════════════════════════════// ❌ Weakened: returns connection with fewer guarantees// ═══════════════════════════════════════════════════════════════ class LazyConnectionFactory extends ConnectionFactory { /** * @postcondition returns connection object * @postcondition connection MAY not be open yet // ⚠️ WEAKER! * @postcondition first query will open it */ createConnection(config: Config): Connection { // Returns a proxy that connects on first use return new LazyConnection(config); // ❌ Violates "open, valid, ready" }}Weakened postconditions often appear as "optimizations" or "flexibility improvements." Here's how to spot them:
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081
// ═══════════════════════════════════════════════════════════════// PATTERN 1: The "Optimization" That Weakens// ═══════════════════════════════════════════════════════════════ class Counter { private count = 0; /** * @postcondition count increased by exactly 1 */ increment(): void { this.count += 1; }} class BatchedCounter extends Counter { private pendingIncrements = 0; /** * @postcondition count WILL BE increased by 1 (eventually) // ⚠️ WEAKER */ increment(): void { this.pendingIncrements += 1; // Actual increment happens later in flush() // ❌ Violates "count increased" — count hasn't changed yet! }} // ═══════════════════════════════════════════════════════════════// PATTERN 2: The Nullable Return// ═══════════════════════════════════════════════════════════════ class UserService { /** * @postcondition returns User for given ID * @throws UserNotFoundError if ID doesn't exist */ getUser(id: string): User { const user = this.db.find(id); if (!user) throw new UserNotFoundError(id); return user; }} class CachedUserService extends UserService { /** * @postcondition returns User for given ID, or null if not in cache * * ⚠️ WEAKER! Parent guaranteed User return, this returns nullable */ getUser(id: string): User | null { // ❌ Type changed! return this.cache.get(id) ?? null; // Doesn't check DB, just returns null if not cached }} // ═══════════════════════════════════════════════════════════════// PATTERN 3: The "Approximate" Result// ═══════════════════════════════════════════════════════════════ class Calculator { /** * @postcondition returns exact result of a^b */ power(a: number, b: number): number { return Math.pow(a, b); }} class FastCalculator extends Calculator { /** * @postcondition returns approximate result of a^b * @postcondition result is within 0.01% of exact value * * ⚠️ WEAKER! Parent promised exact, this is approximate */ power(a: number, b: number): number { // Uses faster but less precise algorithm return this.approximatePow(a, b); }}When reviewing an override, ask: "Is there ANY outcome that the child could produce that the parent never would?" If yes, postconditions are weakened, and LSP is violated.
Think about: return values, state changes, side effects, exceptions, timing guarantees, ordering, precision. Any weakening in any dimension is a violation.
We've thoroughly explored postconditions as the second half of Design by Contract. Let's consolidate the key insights:
What's next:
We've covered preconditions (caller's promises) and postconditions (method's promises). But contracts have a third critical element: invariants — conditions that must always be true. The next page explores how weakening vs. strengthening applies to invariants, and page 4 brings everything together with the complete contract rules for LSP.
You now understand postconditions as formal guarantees and can recognize LSP violations from weakened postconditions. Combined with precondition knowledge, you can analyze half of the behavioral compatibility question for inheritance hierarchies.