Let U = the universe of all valid entities in this domain
Let S ⊆ U = the subset currently under consideration
Let ∅ = the empty/null case (always handle this explicitly)

f: A → B

Precondition:  P(a) must hold before f is applied
Postcondition: Q(f(a)) must hold after f is applied
Invariant:     I(a) = I(f(a))  [what must NOT change]

classify: Document → Category

Pre:  Document is non-empty, language is detected
Post: Category ∈ {defined_taxonomy}
Inv:  Document content is unchanged by classification

∀ x ∈ S: P(x)           — Universal invariant
∃ x ∈ S: P(x)           — Existence guarantee
P(x) ⟹ Q(f(x))          — Conditional guarantee
¬(P(x) ∧ Q(x))          — Mutual exclusion

h = f ∘ g   (h(x) = f(g(x)))

Verify:
  - Codomain of g matches domain of f
  - Preconditions of f are implied by postconditions of g
  - Invariants of both f and g are preserved by h

P(outcome | evidence)     — conditional probability
E[X]                      — expected value
Var(X)                    — variance / spread
argmax_{x} f(x)           — best choice under a criterion

## Specification: [Name]

### 1. Domain Model
[Named sets, types, and primitives]

### 2. Functions / Operations
[Signatures, preconditions, postconditions, invariants]

### 3. Invariants
[Formal or semi-formal statements of what must always hold]

### 4. Edge Cases
[Explicit boundary conditions and their specified behavior]

### 5. Composition / Interaction
[How components combine; verification that composition is sound]

### 6. Open Questions
[What is explicitly left unspecified and why]

## Specification: Content Router

### 1. Domain Model
Let M = set of all incoming messages (finite, non-empty)
Let C = {c₁, c₂, …, cₙ} = finite set of destination categories
Let R = set of routing rules, where each r ∈ R is a predicate r: M → Bool
Let priority: R → ℕ = total ordering on rules (lower = higher priority)

### 2. Functions / Operations

route: M → C ∪ {⊥}

Pre:  m ∈ M, |R| ≥ 1
Post: 
  If ∃ r ∈ R such that r(m) = true:
    route(m) = category associated with highest-priority matching r
  Else:
    route(m) = ⊥  [unrouted — must trigger fallback handler]
Inv:  m is not modified by route(m)

### 3. Invariants
∀ m ∈ M: route(m) is deterministic (same input → same output)
∀ m ∈ M: at most one category is assigned (no split routing)
If route(m) = ⊥, an alert must be emitted

### 4. Edge Cases
M = ∅        → route is never called; system is idle (valid state)
R = ∅        → route(m) = ⊥ for all m (all messages unrouted)
|C| = 1      → route(m) = c₁ for all matched m (trivial routing)
Two rules match → highest priority(r) wins; tie-break by rule index

### 5. Composition
filter ∘ route:
  filter: M → M' removes malformed messages before routing
  Pre of route is satisfied by Post of filter
  Composition valid iff filter guarantees m' ∈ M for all outputs

### 6. Open Questions
- How are rules added/removed at runtime? (Mutation spec not defined here)
- What is the SLA on route latency? (Performance spec out of scope)