Specifications, Abstraction & Invariants

A specification (or spec) is a contract between two parties: the implementer of a piece of code, and the client (caller) who uses it. The spec says:

1. What the client must provide (inputs, preconditions)
2. What the implementer guarantees in return (outputs, postconditions)
3. What the implementer is not obligated to do (behavior outside the spec is undefined)

Critically, a good spec is implementation-independent: it describes what without saying how. This is the foundational act of abstraction — the spec is the boundary at which implementation details stop mattering.

Consider sqrt(x). A bad spec: "uses Newton's method to compute the square root." A good spec: "given a non-negative float x, returns a float r such that |r² - x| < 1e-10 and r ≥ 0."

The good spec lets you swap Newton's method for Babylonian method, lookup tables, or hardware instructions without changing any caller. This is the substitution principle in action, long before Liskov formalized it.

Why specs matter for large systems: In a 1,000-function codebase, you cannot hold all 1,000 implementations in your head at once. But you can hold 1,000 specs, because each spec is much shorter and more abstract than its implementation. Specs are the unit of reasoning at scale.

Specs also have a social dimension: they define blame. If a caller violates a precondition, the bug is the caller's fault. If the callee violates a postcondition, the bug is the callee's fault. This is not lawyering — it is the precision that makes debugging tractable.

def sqrt(x: float) -> float:
    """
    Specification:
      Requires: x >= 0  (precondition)
      Effects:  returns r >= 0 such that abs(r*r - x) < 1e-10  (postcondition)

    Note: behavior is undefined if x < 0.
    The implementation may use any algorithm.
    """
    # One valid implementation:
    if x == 0:
        return 0.0
    r = x
    for _ in range(50):
        r = (r + x / r) / 2.0
    return r

The two most important parts of any specification are the precondition and postcondition.

Precondition (requires clause): a predicate over inputs that the caller must guarantee before calling the function. The implementer is free to assume it holds; if it does not, behavior is undefined — the implementer may do anything, including crash or return nonsense.

Postcondition (effects/ensures clause): a predicate over inputs and outputs that the implementer must guarantee, but only when the precondition holds. If the precondition is violated, no postcondition is promised.

This asymmetry is subtle and important. The implementer does not have to check preconditions — doing so is often efficient, but it is optional. The caller owns the obligation to establish preconditions.

The weakest precondition: a function with precondition true is called total — it works for all inputs. A function with a nontrivial precondition is partial. Partial functions are common (division requires denominator ≠ 0; binary search requires a sorted array) and are not second-class — they are a legitimate tool. The key is making the precondition explicit.

Frame conditions: postconditions must also say what doesn't change. "Returns the sum of elements" doesn't say whether the array is modified. Real specs include frame conditions: "the input array is not modified," or in Java's Collections, "this method is optional" (meaning some implementations may throw UnsupportedOperationException).

Hoare triples: in formal verification, a spec is written as {P} C {Q}: "if precondition P holds before executing command C, and C terminates, then postcondition Q holds afterward." This notation, due to C.A.R. Hoare (1969), is the foundation of formal program verification.

def binary_search(arr: list[int], target: int) -> int:
    """
    Requires: arr is sorted in non-decreasing order (precondition)
    Effects:  returns index i such that arr[i] == target,
              or -1 if target not in arr.  (postcondition)
              arr is not modified.          (frame condition)
    """
    lo, hi = 0, len(arr) - 1
    while lo <= hi:
        mid = (lo + hi) // 2
        if arr[mid] == target:
            return mid
        elif arr[mid] < target:
            lo = mid + 1
        else:
            hi = mid - 1
    return -1

# Caller's obligation:
# data = [1, 3, 5, 7, 9]  # SORTED — precondition met
# binary_search(data, 5)  # safe
# binary_search([3,1,5], 5)  # precondition violated: undefined behavior

Design by Contract (DbC) is a software development methodology, coined by Bertrand Meyer and implemented in the Eiffel language (1986), that treats specifications as first-class citizens: every class has invariants, every method has preconditions and postconditions, and these are part of the language, enforced at runtime during testing and optionally in production.

The core metaphor is a business contract: if a client meets the preconditions, the supplier (implementer) guarantees the postconditions. Obligations and benefits are symmetric:

Three levels of contract:

1. Method contracts: preconditions + postconditions per method
2. Class invariants: properties that hold for every visible state of an object
3. Subcontracting (the Liskov Substitution Principle): a subclass may weaken preconditions (accept more) and strengthen postconditions (promise more) — but never the reverse. This ensures substitutability.

DbC is not just a style guide — it changes how you debug. When an assertion fires, you know immediately whether the bug is in the caller (precondition violated) or the callee (postcondition violated). Without contracts, you have to search the entire call stack.

Python assert as lightweight DbC: Python's assert statement is a minimal DbC tool. assert condition, message raises AssertionError if the condition is false. Use assert to check preconditions at the top of functions and postconditions before returning. In production, assertions can be disabled with python -O, making them zero-cost when not debugging.

class BankAccount:
    def __init__(self, initial_balance: float):
        assert initial_balance >= 0, "Initial balance must be non-negative"
        self._balance = initial_balance
        assert self._check_invariant()  # establish invariant at construction

    def _check_invariant(self) -> bool:
        """Class invariant: balance is always >= 0."""
        return self._balance >= 0

    def deposit(self, amount: float) -> None:
        """Requires: amount > 0
           Effects:  balance increases by amount"""
        assert amount > 0, f"Deposit amount must be positive, got {amount}"
        old_balance = self._balance  # save for postcondition check
        self._balance += amount
        assert self._balance == old_balance + amount  # postcondition
        assert self._check_invariant()

    def withdraw(self, amount: float) -> None:
        """Requires: 0 < amount <= self.balance
           Effects:  balance decreases by amount"""
        assert 0 < amount <= self._balance, "Invalid withdrawal amount"
        self._balance -= amount
        assert self._check_invariant()

An abstraction function (AF) is the mathematical map from the concrete representation of a data type to the abstract value it represents. It is the formal answer to: "what abstract object does this concrete state correspond to?"

Consider a Set of integers implemented as a sorted array [1, 3, 5]. The abstract value is the mathematical set {1, 3, 5}. The abstraction function is: AF([1, 3, 5]) = {1, 3, 5}.

But notice: [1, 3, 5] and [3, 1, 5] both represent the same abstract set {1, 3, 5} — the abstract value doesn't depend on order. The AF maps many concrete states to the same abstract value. This many-to-one mapping is the essence of abstraction: the implementation has structure (order, layout, hash buckets) that the abstraction discards.

The AF is a function from concrete to abstract:

• Domain: the set of valid concrete representations (those satisfying the RI)
• Codomain: the set of abstract values the type is meant to represent
• It is (usually) surjective: every abstract value has at least one representation
• It is (usually) not injective: multiple representations can map to the same abstract value

Why write down the AF?

1. It forces you to decide what your data structure means
2. It lets you verify that your operations are correct: add(x, s) is correct iff AF(result) = AF(s) ∪ {x}
3. It documents for future maintainers exactly what invariants the representation must satisfy

The AF is not the implementation: you do not call the AF at runtime. It is a mathematical artifact — a tool for reasoning. Write it as a comment at the top of the class, and use it mentally when verifying each method.

class IntSet:
    """
    Abstraction Function:
      AF(self._elems) = the set { self._elems[i] | 0 <= i < len(self._elems) }

    Representation Invariant:
      self._elems is a sorted list of distinct integers.

    Example:
      self._elems = [1, 3, 5, 9]  -->  abstract value {1, 3, 5, 9}
      self._elems = []             -->  abstract value {}  (empty set)
    """
    def __init__(self):
        self._elems: list[int] = []  # RI: sorted, no duplicates

    def add(self, x: int) -> None:
        """Effects: abstract set becomes AF(self) ∪ {x}"""
        import bisect
        pos = bisect.bisect_left(self._elems, x)
        if pos == len(self._elems) or self._elems[pos] != x:
            self._elems.insert(pos, x)
        # Post: self._elems still sorted, still no duplicates

    def contains(self, x: int) -> bool:
        """Effects: returns True iff x ∈ AF(self)"""
        import bisect
        pos = bisect.bisect_left(self._elems, x)
        return pos < len(self._elems) and self._elems[pos] == x

A representation invariant (RI) is a predicate over the concrete representation that must hold at every externally visible moment in the lifetime of an object. It defines which concrete states are legal — which states actually correspond to a valid abstract value via the AF.

The RI is what the AF's domain is defined over. If an object's concrete state violates the RI, the AF doesn't apply — the object is in an inconsistent, undefined state.

When must the RI hold?

• After every constructor completes
• After every mutating method completes
• Before every method begins (since it held after the last call)

During the execution of a method, the RI may be temporarily violated — that is fine, as long as it is restored before the method returns. This is the atomicity property of well-designed operations.

RI examples:

• SortedList: elements are in non-decreasing order
• BinarySearchTree: for every node n, all values in n's left subtree < n.value < all values in n's right subtree
• HashTable with open addressing: every key stored at hash(key) % capacity (mod probe sequence)
• RationalNumber(p, q): q > 0 and gcd(p, q) == 1 (canonical form)

Checking the RI: write a check_rep() (or _check_invariant()) method that asserts the RI. Call it at the end of every constructor and every mutating method during testing. In production, the assertion can be disabled. This turns RI violations from silent corruption into loud, early failures.

The RI is the immune system of your data structure: it detects when something has gone wrong and localizes the failure to the operation that violated it, rather than letting corruption propagate silently until something completely unrelated breaks.

class RationalNumber:
    """
    Represents the rational number p/q.

    Abstraction Function:
      AF(self) = self._numer / self._denom  (as a fraction)

    Representation Invariant:
      self._denom > 0
      gcd(abs(self._numer), self._denom) == 1  (canonical/reduced form)
    """
    def __init__(self, numer: int, denom: int):
        assert denom != 0, "Denominator cannot be zero"
        from math import gcd
        g = gcd(abs(numer), abs(denom))
        # Canonicalize: denom always positive
        sign = -1 if denom < 0 else 1
        self._numer = sign * numer // g
        self._denom = sign * denom // g
        self._check_rep()

    def _check_rep(self):
        from math import gcd
        assert self._denom > 0
        assert gcd(abs(self._numer), self._denom) == 1

    def add(self, other: 'RationalNumber') -> 'RationalNumber':
        # Postcondition: result represents self + other in canonical form
        return RationalNumber(
            self._numer * other._denom + other._numer * self._denom,
            self._denom * other._denom
        )

    def __repr__(self):
        return f"{self._numer}/{self._denom}"

The abstraction function and representation invariant are not independent — they form a coupled pair that together define a correct abstract data type implementation. Understanding their relationship is the key to correct-by-construction data structure design.

The RI restricts the AF's domain: the AF is only defined on representations that satisfy the RI. If R violates the RI, AF(R) is meaningless. This is why check_rep() must be called aggressively during testing — a violated RI means the AF can no longer tell you what your object is.

Proving operations correct with AF and RI: to prove that a method op is correct, you need to show:

1. If the RI holds before op, then the RI holds after op (RI preservation)
2. AF(result) equals the abstract specification of op applied to AF(input) (AF consistency)

For example, for IntSet.add(x): we need to show (1) the result's _elems is still sorted with no duplicates, and (2) AF(result) = AF(self) ∪ {x}.

Multiple representations, one abstraction: a profound insight is that the same abstract type can have many valid AF+RI pairs — one per implementation. A Set can be implemented as:

• Sorted array: RI = sorted + unique; AF = set of elements
• Hash table: RI = elements at correct buckets; AF = set of all elements
• Balanced BST: RI = BST property + balance; AF = set of elements

All three implement the same abstract type, verified by the same abstract specification. The spec is what unifies them; the AF+RI is what makes each correct.

Abstraction barriers: the AF+RI together define the abstraction barrier. Code outside the class must only depend on the abstract specification (what the AF maps to). Code inside the class may depend on the representation. Mixing these — allowing client code to depend on representation details — is called representation exposure, and it destroys the ability to change implementations.

# Two implementations of the SAME abstract type: a set of integers
# Both satisfy the same abstract specification.
# The AF and RI differ, but the public interface is identical.

class ArraySet:
    """
    AF: AF(self._data) = { x | x in self._data }
    RI: self._data contains no duplicate elements
    """
    def __init__(self): self._data = []
    def add(self, x):
        if x not in self._data: self._data.append(x)
    def contains(self, x): return x in self._data
    def size(self): return len(self._data)

class BitVectorSet:
    """
    For small non-negative integers only.
    AF: AF(self._bits) = { i | bit i of self._bits is 1 }
    RI: self._bits >= 0
    """
    def __init__(self): self._bits = 0
    def add(self, x):
        assert x >= 0
        self._bits |= (1 << x)
    def contains(self, x): return bool(self._bits & (1 << x))
    def size(self): return bin(self._bits).count('1')

# The abstract spec (client's view) is identical for both:
# add(x): effects = set now contains x
# contains(x): returns True iff x is in the set
# size(): returns |set|

Representation exposure (or rep exposure) occurs when code outside a class can access or modify the internal representation directly, bypassing the class's methods and potentially violating the RI.

Rep exposure is one of the most common and dangerous bugs in object-oriented software. It manifests in several ways:

1. Returning a mutable reference to an internal field: if a List<T> class returns its internal array directly, a caller can modify the array, violating the RI without the class knowing.

2. Storing a passed-in mutable object without copying: if a constructor takes a mutable object and stores the reference, the caller retains the ability to modify it later.

3. Public fields: any public field can be written by any code.

The fix: defensive copying. When you receive a mutable object, copy it. When you return a mutable object, return a copy (or an unmodifiable view). This ensures the only path to modifying the internal state goes through the class's own methods, which maintain the RI.

Java's Collections.unmodifiableList is the standard tool for returning an unmodifiable view. Python's tuple and frozenset are immutable alternatives. In C++, returning const references provides read-only access.

Immutability as the ultimate defense: immutable objects cannot have rep exposure because their state never changes. Once constructed correctly (RI established), an immutable object's RI holds forever. This is why immutability is so valued — it eliminates an entire class of bugs. Python's str, int, tuple, and frozenset are all immutable; Java's String is immutable.

from typing import List

# BAD: rep exposure via returned reference
class BadStack:
    def __init__(self):
        self._data: List[int] = []

    def get_data(self) -> List[int]:
        return self._data  # DANGER: caller can mutate self._data directly!

# bs = BadStack()
# bs.get_data().append(99)  # bypasses all invariant checks!

# GOOD: defensive copy
class GoodStack:
    """
    AF: AF(self._data) = stack with top at self._data[-1]
    RI: self._data is a list (no further constraint here)
    """
    def __init__(self, initial: List[int] = None):
        # Defensive copy of input
        self._data: List[int] = list(initial) if initial else []

    def push(self, x: int) -> None:
        self._data.append(x)

    def pop(self) -> int:
        assert len(self._data) > 0, "pop from empty stack"
        return self._data.pop()

    def snapshot(self) -> List[int]:
        """Returns a copy — caller cannot affect internal state."""
        return list(self._data)  # defensive copy on return

    def __len__(self) -> int:
        return len(self._data)

Writing a good specification is a skill, like writing clear prose. Here are the principles that MIT 6.031 and the Liskov/Guttag textbook emphasize:

1. Be precise but minimal: state exactly what the function does, no more, no less. Over-specifying ("uses a red-black tree internally") restricts implementation choice needlessly. Under-specifying ("does something with the list") gives callers no guarantee.

2. Use quantifiers and logical connectives: "for all i, 0 ≤ i < n: result[i] ≤ result[i+1]" is much more precise than "returns a sorted array."

3. State what doesn't change (frame conditions): if a method doesn't modify its inputs, say so. "The input array is unchanged" is a crucial guarantee for callers.

4. Use abstraction, not representation: say "returns the maximum element" not "returns the last element of the sorted internal array." The spec should be true regardless of implementation.

5. Handle errors explicitly: decide whether the function throws an exception, returns a sentinel, or has undefined behavior for invalid inputs — and document it.

6. Be consistent across mutually-related methods: the spec of add(x) and contains(x) must be consistent: after add(x), contains(x) must return true.

Specs for interfaces vs. implementations: in Java, a List interface has a spec for get(i), and ArrayList and LinkedList both implement it. The spec is written once for the interface; each implementation is verified against it. This is the power of spec-first design.

Functional vs. operational specs: a functional spec says what the output is as a function of the input (preferred). An operational spec describes an algorithm (avoid — it over-constrains). "Returns the maximum of a and b" is functional. "Compares a and b, and if a > b returns a, else returns b" is operational and unnecessarily detailed.

# Example: specifying a sort function rigorously

def sort(arr: list[int]) -> list[int]:
    """
    Requires:
      arr is a list of integers (no special constraint on order)

    Effects:
      Returns a NEW list result such that:
        1. len(result) == len(arr)                           [same length]
        2. for all i in range(len(result)-1):               [sorted]
               result[i] <= result[i+1]
        3. result is a permutation of arr                   [same elements]
             i.e., sorted(result) == sorted(arr)
             (equivalently: same multiset of elements)
        4. arr is not modified                              [frame condition]

    Note: this spec is satisfied by mergesort, quicksort,
    heapsort, timsort, etc. — any stable or unstable sort.
    The spec does NOT require stability (equal elements may
    appear in any relative order). If stability is required,
    it must be added explicitly.
    """
    return sorted(arr)  # one valid implementation

Real specifications must handle the question: what happens when the precondition is violated, or when the function encounters an error condition? There are three philosophically different approaches:

1. Undefined behavior (C-style): the precondition is a client obligation, and if it is violated, the function may do anything — return garbage, crash, corrupt memory, delete files. This is the approach of C's standard library (memcpy with overlapping regions). It gives maximum performance but is dangerous: one mistake anywhere in a large program can cause arbitrary corruption.

2. Checked exceptions (Java-style): the function declares that it may throw specific exceptions (e.g., throws IndexOutOfBoundsException). The caller is forced by the compiler to handle or propagate them. The spec includes: "throws X if condition C." This turns error handling into part of the type system.

3. Optional/Result types (Haskell/Rust-style): the function returns Maybe T (Haskell) or Result<T, E> (Rust), forcing the caller to unpack the result and handle the error case explicitly, without exceptions. This is the safest approach — errors cannot be silently ignored.

The defensive programming tradeoff: should functions check their preconditions and raise errors? The answer depends on context:

• Public APIs (library code used by unknown callers): always check, raise clear exceptions. The cost of one check per call is negligible; the cost of an uncaught violation in production is enormous.
• Internal methods (called only by known, controlled callers): use assert in debug mode; skip in production for performance.
• Performance-critical inner loops: accept that the caller must guarantee preconditions, and skip checks. Document this explicitly.

The key insight: raising an exception when a precondition is violated is not mandated by the spec — it is a defensive choice made by the implementer for better error detection. The spec says precondition violation = undefined behavior; the implementation may additionally promise to raise ValueError. This is called a stronger postcondition for the error case.

# Three styles of handling "index out of range"

# Style 1: Undefined behavior (C-like) — fastest, most dangerous
def get_c_style(arr, i):
    # No check. If i is out of range, behavior is undefined.
    return arr[i]

# Style 2: Checked exception (Java-like)
def get_checked(arr, i):
    """
    Requires: (nothing — total function)
    Effects: returns arr[i] if 0 <= i < len(arr);
             raises IndexError otherwise.
    """
    if i < 0 or i >= len(arr):
        raise IndexError(f"Index {i} out of range [0, {len(arr)})")
    return arr[i]

# Style 3: Optional (Haskell/Rust-like, using Python Optional)
from typing import Optional
def get_optional(arr, i) -> Optional[int]:
    """
    Requires: (nothing — total function)
    Effects: returns arr[i] if 0 <= i < len(arr);
             returns None otherwise.
    Caller must check for None.
    """
    if 0 <= i < len(arr):
        return arr[i]
    return None

# In Rust, this would be:
# fn get(arr: &[i32], i: usize) -> Option<i32> {
#     arr.get(i).copied()
# }

A class invariant is a predicate over an object's state that must hold at every publicly observable moment: after every constructor, and after every public method returns. It is the RI extended to the class level — not just "is this representation valid?" but "does this object satisfy its abstract contract?"

Class invariants formalize the idea that an object is always in a meaningful, consistent state. They are the key to reasoning about object-oriented programs.

Examples of class invariants:

• BinarySearchTree: for every node n, max(left subtree) < n.key < min(right subtree)
• PriorityQueue: the heap property — parent's priority ≥ children's priorities
• OrderedDict: iteration order matches insertion order
• StringBuffer (Java): count <= data.length and data != null

The invariant lifecycle:

1. Establishment: every constructor must leave the object in a state satisfying the invariant
2. Preservation: every public method that modifies the object must re-establish the invariant before returning
3. Use: every method may assume the invariant holds at entry (since the previous operation preserved it)

Invariants during mutation: a method may temporarily break the invariant during its execution. This is fine — the invariant is an external promise, not an internal straitjacket. For example, heapify_up in a priority queue may temporarily violate the heap property partway through — as long as it restores it before returning.

Inheritance and invariants: a subclass inherits the parent's invariant and may only strengthen it (add more constraints). A subclass may never weaken the parent's invariant — doing so violates the Liskov Substitution Principle. This is one of the deepest insights of object-oriented design.

class MinHeap:
    """
    Abstraction Function:
      AF(self._data) = a multiset of integers, supporting
      efficient minimum extraction.

    Representation Invariant (heap property):
      For all i > 0: self._data[(i-1)//2] <= self._data[i]
      i.e., every parent is <= its children.

    Class Invariant:
      The above RI holds after every public operation.
    """
    def __init__(self):
        self._data = []

    def push(self, x: int) -> None:
        self._data.append(x)        # temporarily may violate RI
        self._sift_up(len(self._data) - 1)  # restores RI
        assert self._check_rep()

    def pop_min(self) -> int:
        assert len(self._data) > 0
        self._data[0] = self._data[-1]
        self._data.pop()            # temporarily may violate RI
        if self._data:
            self._sift_down(0)      # restores RI
        assert self._check_rep()
        return self._data[0] if False else self._data[0]  # simplified

    def _check_rep(self) -> bool:
        for i in range(1, len(self._data)):
            if self._data[(i-1)//2] > self._data[i]:
                return False
        return True

    def _sift_up(self, i):
        while i > 0:
            parent = (i - 1) // 2
            if self._data[parent] <= self._data[i]:
                break
            self._data[parent], self._data[i] = self._data[i], self._data[parent]
            i = parent

    def _sift_down(self, i):
        n = len(self._data)
        while 2*i+1 < n:
            left, right = 2*i+1, 2*i+2
            smallest = left
            if right < n and self._data[right] < self._data[left]:
                smallest = right
            if self._data[i] <= self._data[smallest]:
                break
            self._data[i], self._data[smallest] = self._data[smallest], self._data[i]
            i = smallest

The Liskov Substitution Principle (LSP), formulated by Barbara Liskov and Jeannette Wing in 1994, is perhaps the most important principle connecting specifications to object-oriented design. It states:

If S is a subtype of T, then any program that works correctly using an object of type T must also work correctly when that object is replaced by an object of type S, without modification.

In terms of specifications, this means:

Preconditions can only be weakened in subtypes: a subtype's method may accept more inputs than the parent — but not fewer. If the parent requires x > 0, the subtype may accept x >= 0, but not x > 5. (It is always safe to accept more; accepting less breaks callers who relied on the parent's contract.)

Postconditions can only be strengthened in subtypes: a subtype's method must deliver at least as much as the parent promises — it may deliver more. If the parent promises "returns a non-negative integer," the subtype may promise "returns a positive integer," but not "returns an integer" (weaker).

Class invariants can only be strengthened in subtypes: a subtype must maintain all invariants the parent maintains, and may add more.

Why this matters: LSP is what makes polymorphism safe. When you write a function that accepts a Shape and calls area(), you can pass any subclass (Circle, Rectangle, Triangle) and the function works correctly — because the subclass's area() satisfies the parent's spec. Violating LSP (the classic example: Square as a subtype of Rectangle where setWidth and setHeight must satisfy different invariants) breaks polymorphism and leads to fragile, surprising code.

# Classic LSP example: Rectangle and Square

class Rectangle:
    """
    Invariant: width > 0 and height > 0
    """
    def __init__(self, w, h):
        assert w > 0 and h > 0
        self._w, self._h = w, h

    def set_width(self, w):
        """Postcondition: self.width == w; self.height unchanged."""
        assert w > 0
        self._w = w

    def set_height(self, h):
        """Postcondition: self.height == h; self.width unchanged."""
        assert h > 0
        self._h = h

    def area(self): return self._w * self._h

# BAD: Square violates LSP!
class BadSquare(Rectangle):
    def set_width(self, w):
        # Must also change height to maintain square invariant.
        # But this VIOLATES Rectangle's postcondition:
        # "self.height unchanged" is broken.
        self._w = self._h = w

def double_width_test(rect: Rectangle):
    rect.set_width(5)
    rect.set_height(3)
    # By Rectangle's spec, area should be 5*3 = 15
    assert rect.area() == 15  # FAILS for BadSquare!

# The CORRECT fix: Square should NOT inherit Rectangle.
# They are different abstract types with different invariants.
# Use composition or a shared interface (Shape) instead.

In industry, specifications are enforced through a spectrum of mechanisms, each with different tradeoffs between expressiveness, cost, and coverage:

1. Type systems: the most pervasive form of specification enforcement. A type int -> bool says the function takes an integer and returns a boolean — a fragment of the spec checked by the compiler. Modern type systems (Rust's borrow checker, Haskell's type classes, Python's mypy) encode increasingly rich preconditions and postconditions. Dependent types (in Idris, Agda, Coq) can encode arbitrary predicates in types — you can have a type SortedList that proves at compile time that the list is sorted.

2. Assertions (assert): the simplest runtime check. Use assert for preconditions at the top of functions and postconditions before returning. Python's assert can be disabled in production with -O; C's assert.h similarly.

3. Unit tests: a weaker but more automated form of specification checking. A test suite for sort that checks sorted output, correct length, and correct elements on a variety of inputs is an executable, partial specification. Tests catch RI violations that assertions miss (because assertions only fire on the specific execution path tested).

4. Property-based testing (e.g., Python's hypothesis, Haskell's QuickCheck): you specify properties (postconditions as predicates over random inputs), and the tool automatically generates hundreds of test cases. For sort, you'd write: "for all lists lst, the result is sorted and is a permutation of lst." This is closer to a true spec than example-based tests.

5. Formal verification tools: tools like Dafny, F*, Coq, Isabelle, and TLA+ let you write specs as formal logic and prove that implementations satisfy them. This is the gold standard — used in safety-critical systems (avionics, cryptographic protocols, OS kernels like seL4).

The pragmatic choice: most engineering uses types + assertions + property-based tests. Formal verification is reserved for the most critical components. But understanding the formal underpinnings (AF, RI, Hoare logic) makes you a better engineer at every level — even if you never write a Coq proof.

# Property-based testing with hypothesis — executable specification
from hypothesis import given, strategies as st

def my_sort(arr):
    return sorted(arr)  # implementation under test

@given(st.lists(st.integers()))
def test_sort_sorted(arr):
    result = my_sort(arr)
    # Postcondition 1: result is sorted
    for i in range(len(result) - 1):
        assert result[i] <= result[i+1]

@given(st.lists(st.integers()))
def test_sort_permutation(arr):
    result = my_sort(arr)
    # Postcondition 2: result is a permutation of input
    assert sorted(result) == sorted(arr)
    assert len(result) == len(arr)

@given(st.lists(st.integers()))
def test_sort_no_mutation(arr):
    original = list(arr)
    my_sort(arr)
    # Frame condition: input not modified
    assert arr == original

# Hypothesis generates hundreds of random lists and checks all three
# properties — it will even try edge cases: [], [1], [1,1,1], etc.