Preconditions and Postconditions

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

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
     */
    withdraw(amount: number): void {
        // Precondition check (defensive, not required by contract)
        if (amount <= 0) {
            throw new Error("Amount must be positive");
        }
        if (amount > this.balance) {
            throw new Error("Insufficient funds");
        }
        
        this.balance -= 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

// ═══════════════════════════════════════════════════════════════
// PARAMETER CONSTRAINTS
// Restrictions on method arguments
// ═══════════════════════════════════════════════════════════════
 
class ArrayList<T> {
    private items: T[] = [];
    
    /**
     * @precondition index >= 0 && index < this.size()
     */
    get(index: number): T {
        // Caller promises: valid index range
        return this.items[index];
    }
    
    /**
     * @precondition fromIndex >= 0 && toIndex <= this.size()
     * @precondition fromIndex <= toIndex
     */
    subList(fromIndex: number, toIndex: number): T[] {
        // Caller promises: valid range, proper ordering
        return this.items.slice(fromIndex, toIndex);
    }
}
 
// ═══════════════════════════════════════════════════════════════
// OBJECT STATE CONSTRAINTS  
// Requirements on the object's internal state
// ═══════════════════════════════════════════════════════════════
 
class FileWriter {
    private handle: FileHandle | null = null;
    
    /**
     * @precondition this.isOpen() == true
     */
    write(data: string): void {
        // Caller promises: file was opened first
        this.handle!.write(data);
    }
    
    /**
     * @precondition this.isOpen() == false  
     */
    open(path: string): void {
        // Caller promises: not already open (prevents resource leak)
        this.handle = fs.openSync(path, 'w');
    }
}
 
// ═══════════════════════════════════════════════════════════════
// ORDERING/PROTOCOL CONSTRAINTS
// Assumptions about method call sequences
// ═══════════════════════════════════════════════════════════════
 
class Transaction {
    private isStarted = false;
    private isCommitted = false;
    
    /**
     * @precondition !this.isStarted && !this.isCommitted
     */
    begin(): void {
        // Can only begin once, before any commit
        this.isStarted = true;
    }
    
    /**
     * @precondition this.isStarted && !this.isCommitted
     */
    commit(): void {
        // Must have begun, cannot commit twice
        this.isCommitted = true;
    }
    
    /**
     * @precondition this.isStarted && !this.isCommitted
     */
    rollback(): void {
        // Must have begun, cannot rollback after commit
        this.isStarted = false;
    }
}
 
// ═══════════════════════════════════════════════════════════════
// SEMANTIC TYPE CONSTRAINTS
// Requirements beyond what the type system can express
// ═══════════════════════════════════════════════════════════════
 
class SearchAlgorithms {
    /**
     * @precondition arr is sorted in ascending order
     * @precondition arr contains no duplicate elements
     */
    binarySearch<T>(arr: T[], target: T): number {
        // Caller promises: array is sorted (runtime cannot check efficiently)
        let low = 0, high = arr.length - 1;
        while (low <= high) {
            const mid = Math.floor((low + high) / 2);
            if (arr[mid] === target) return mid;
            if (arr[mid] < target) low = mid + 1;
            else high = mid - 1;
        }
        return -1;
    }
}

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

// ═══════════════════════════════════════════════════════════════
// BASE CLASS: General payment processor
// ═══════════════════════════════════════════════════════════════
 
class PaymentProcessor {
    /**
     * Processes a payment of the given amount.
     * 
     * @precondition amount > 0
     */
    processPayment(amount: number): PaymentResult {
        // Accepts any positive amount
        return this.executePayment(amount);
    }
    
    protected executePayment(amount: number): PaymentResult {
        // Base implementation
        return { success: true, transactionId: generateId() };
    }
}
 
// ═══════════════════════════════════════════════════════════════
// ❌ LSP VIOLATION: Strengthened precondition
// ═══════════════════════════════════════════════════════════════
 
class PremiumPaymentProcessor extends PaymentProcessor {
    /**
     * Processes a payment of the given amount.
     * 
     * @precondition amount > 0
     * @precondition amount >= 100  // ⚠️ NEW, STRONGER PRECONDITION!
     */
    processPayment(amount: number): PaymentResult {
        if (amount < 100) {
            // Rejects amounts the parent would accept!
            throw new Error("Minimum payment is $100");
        }
        return super.processPayment(amount);
    }
}
 
// ═══════════════════════════════════════════════════════════════
// Client code written against the base class
// ═══════════════════════════════════════════════════════════════
 
function processMicroPayments(processor: PaymentProcessor): void {
    // These are all valid according to PaymentProcessor's contract
    const amounts = [0.99, 5.00, 25.00, 50.00];
    
    for (const amount of amounts) {
        // ✅ All amounts > 0, so precondition is satisfied
        const result = processor.processPayment(amount);
        console.log(`Processed $${amount}: ${result.success}`);
    }
}
 
// ═══════════════════════════════════════════════════════════════
// The substitution problem
// ═══════════════════════════════════════════════════════════════
 
// This works perfectly:
const standard = new PaymentProcessor();
processMicroPayments(standard);  // ✅ All payments succeed
 
// This breaks the code:
const premium = new PremiumPaymentProcessor();
processMicroPayments(premium);   // ❌ Throws on $0.99, $5.00, $25.00, $50.00
 
// The client code is CORRECT according to PaymentProcessor's contract,
// but PremiumPaymentProcessor broke that contract by adding requirements.

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

// ═══════════════════════════════════════════════════════════════
// BASE CLASS: Requires positive amounts
// ═══════════════════════════════════════════════════════════════
 
class StrictCalculator {
    /**
     * Computes the square root of n.
     * 
     * @precondition n > 0 (strictly positive)
     */
    squareRoot(n: number): number {
        // Doesn't handle zero or negatives
        return Math.sqrt(n);
    }
}
 
// ═══════════════════════════════════════════════════════════════
// ✅ LSP COMPLIANT: Weakened precondition
// ═══════════════════════════════════════════════════════════════
 
class FlexibleCalculator extends StrictCalculator {
    /**
     * Computes the square root of n.
     * 
     * @precondition n >= 0 (zero is now acceptable!)
     */
    squareRoot(n: number): number {
        // Accepts everything the parent accepts, plus zero
        if (n === 0) return 0;  // Handle the new case
        return super.squareRoot(n);
    }
}
 
// ═══════════════════════════════════════════════════════════════
// Even more flexible subclass
// ═══════════════════════════════════════════════════════════════
 
class ComplexCalculator extends FlexibleCalculator {
    /**
     * Computes the square root of n (returns complex for negatives).
     * 
     * @precondition true (accepts any real number!)
     */
    squareRoot(n: number): number | { real: number; imaginary: number } {
        if (n < 0) {
            // Handle negatives by returning complex result
            return { real: 0, imaginary: Math.sqrt(-n) };
        }
        return super.squareRoot(n);
    }
}
 
// ═══════════════════════════════════════════════════════════════
// All substitutions work correctly
// ═══════════════════════════════════════════════════════════════
 
function calculateRoots(calc: StrictCalculator): void {
    // Only uses inputs valid for StrictCalculator
    const values = [1, 4, 9, 16, 25];
    for (const v of values) {
        console.log(`√${v} = ${calc.squareRoot(v)}`);
    }
}
 
// All of these work:
calculateRoots(new StrictCalculator());   // ✅ Original
calculateRoots(new FlexibleCalculator()); // ✅ Accepts everything parent accepts
calculateRoots(new ComplexCalculator());  // ✅ Accepts even more
 
// Subclasses accept MORE inputs, never fewer.
// They never surprise client code with rejected inputs.

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

// ═══════════════════════════════════════════════════════════════
// PATTERN 1: The "Innocent" Guard Clause
// ═══════════════════════════════════════════════════════════════
 
class Logger {
    log(message: string, level: LogLevel = "INFO"): void {
        // Accepts any message at any level
        this.writeLog(message, level);
    }
}
 
class ProductionLogger extends Logger {
    log(message: string, level: LogLevel = "INFO"): void {
        // ⚠️ RED FLAG: New conditional at start of override
        if (level === "DEBUG" || level === "TRACE") {
            return;  // Silently ignores valid inputs — still a violation!
        }
        super.log(message, level);
    }
}
// This is subtle: it doesn't throw, but it IGNORES inputs the parent would handle.
// A client logging DEBUG messages gets unexpected behavior.
 
// ═══════════════════════════════════════════════════════════════
// PATTERN 2: The Null Check Addition
// ═══════════════════════════════════════════════════════════════
 
class UserRepository {
    findById(id: string | null): User | null {
        if (id === null) return null;  // Explicitly handles null
        return this.database.find(id);
    }
}
 
class CachingUserRepository extends UserRepository {
    findById(id: string | null): User | null {
        // ⚠️ RED FLAG: Parent handles null, child rejects it
        if (id === null) {
            throw new Error("ID cannot be null");  // ❌ LSP Violation!
        }
        return this.cache.get(id) ?? super.findById(id);
    }
}
 
// ═══════════════════════════════════════════════════════════════
// PATTERN 3: The Hidden State Requirement
// ═══════════════════════════════════════════════════════════════
 
class Connection {
    send(data: Buffer): void {
        // Sends data (opens connection lazily if needed)
        if (!this.isConnected) this.connect();
        this.socket.write(data);
    }
}
 
class SecureConnection extends Connection {
    private tlsEstablished = false;
    
    send(data: Buffer): void {
        // ⚠️ RED FLAG: New state requirement not in parent
        if (!this.tlsEstablished) {
            throw new Error("TLS handshake not completed");  // ❌
        }
        super.send(data);
    }
    
    // The fix: establish TLS automatically in send()
    sendSecure(data: Buffer): void {
        if (!this.tlsEstablished) this.establishTLS();
        super.send(data);
    }
}

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

class Vector<T> {
    private elements: T[];
    
    /**
     * Gets the element at the specified index.
     * 
     * CONTRACT (Precondition):
     *   index >= 0 && index < this.size()
     *   
     * The caller is responsible for ensuring valid indices.
     * If precondition is violated, behavior is undefined.
     * 
     * In practice, we throw to fail fast, but this is a
     * courtesy — not a guarantee the API promises.
     */
    get(index: number): T {
        // ═══════════════════════════════════════════════════════
        // ASSERTION: Precondition check (may be stripped in prod)
        // This documents and enforces the contract during development
        // ═══════════════════════════════════════════════════════
        console.assert(
            index >= 0 && index < this.elements.length,
            `Precondition violated: index ${index} out of bounds [0, ${this.elements.length})`
        );
        
        // ═══════════════════════════════════════════════════════
        // DEFENSIVE CHECK: Kept in production for safety
        // This converts undefined behavior into a clear exception
        // ═══════════════════════════════════════════════════════
        if (index < 0 || index >= this.elements.length) {
            throw new RangeError(
                `Index ${index} out of bounds for vector of size ${this.elements.length}`
            );
        }
        
        return this.elements[index];
    }
    
    /**
     * Returns element at index, or undefined if out of bounds.
     * 
     * CONTRACT (Precondition): true (none!)
     * 
     * This method has NO preconditions — it handles all inputs.
     * Use this when you cannot guarantee valid indices.
     */
    tryGet(index: number): T | undefined {
        // No assertions needed — any input is valid
        if (index < 0 || index >= this.elements.length) {
            return undefined;  // Part of the contract, not a violation
        }
        return this.elements[index];
    }
}
 
// ═══════════════════════════════════════════════════════════════
// Usage guidance
// ═══════════════════════════════════════════════════════════════
 
// KNOWN VALID INDEX: Use get() for clear semantics
const element = vector.get(knownValidIndex);
 
// UNCERTAIN INDEX: Use tryGet() to handle gracefully
const maybeElement = vector.tryGet(userProvidedIndex);
if (maybeElement !== undefined) {
    // proceed
}