Postconditions — What Must Be True After

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28

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

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137

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

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82

// ═══════════════════════════════════════════════════════════════
// 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.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101

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

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46

// ═══════════════════════════════════════════════════════════════
// 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!

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81

// ═══════════════════════════════════════════════════════════════
// 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);
    }
}