Function Contracts
The canonical v0.34.7 Design by Contract guide now lives in
guide/dbc/. This verification page remains as a legacy
entry point.
Current contract topics:
requires— preconditions and caller obligations.ensures— postconditions and theresultpseudo-variable.invariant— loop entry/back-edge obligations.prove— hard compile-time proof directives.assert_static— CTFE assertions with runtime fallback for dynamic cases.limit<Rules>— named range contracts.- Z3 cookbook — reports, SMT-LIB dumps, and solver-friendly patterns.
For broad verification topics that are not DbC-specific, continue with: