Design-by-Contract development

Contracts (PRE/POST/INV) define behavioral specification -- design from requirements before code exists. Formalized as Hoare Triples: {P} C {Q} where P=precondition, C=code, Q=postcondition.

Modern insight (2025): DbC complements LLM-generated code by serving as safety guardrails -- contracts clarify intent and prevent AI from breaking integrations. Spec-driven development (2025) positions contracts as "executable specifications."

See libraries for language-specific contract tools. See examples for brief contract patterns per language.

Verification Hierarchy

Use compile-time verification before runtime contracts. If a property can be verified statically, do NOT add a runtime contract.

Static Assertions (compile-time) > Test/Debug Contracts > Runtime Contracts