Contracts

Goth supports runtime-checked preconditions and postconditions on function declarations.

Preconditions (⊢)

Checked before the function body executes:

╭─ sqrt_safe : F → F
│  ⊢ ₀ ≥ 0
╰─ √₀

In preconditions, ₀ is the last argument, ₁ the second-to-last, etc.

Unicode: ⊢ / ASCII: |-

Multiple preconditions:

╭─ divide : F → F → F
│  ⊢ ₀ ≠ 0
│  ⊢ abs ₁ < 1000
╰─ ₁ / ₀

Postconditions (⊨)

Checked after the function body executes:

╭─ double : F → F
│  ⊨ ₀ = ₁ × 2
╰─ ₀ × 2

In postconditions, ₀ is the result, ₁ is the first argument (shifted), etc.

Unicode: ⊨ / ASCII: |=

Contract Violations

Violations produce runtime errors:

╭─ positive_only : F → F
│  ⊢ ₀ > 0
╰─ ₀

positive_only(-5)
# Error: Precondition violated: precondition #1 failed

Examples

Safe division (div_safe.goth):

╭─ divSafe : I64 → I64 → I64
│  ⊢ ₀ ≠ 0
╰─ ₁ / ₀

Factorial with bounds (factorial_contract.goth):

╭─ factorial : F → F
│  ⊢ ₀ ≥ 0
│  ⊨ ₀ ≥ 1
╰─ if ₀ < 1 then 1 else ₀ × factorial(₀ - 1)

Safe square root (sqrt_safe.goth):

╭─ sqrtSafe : F64 → F64
│  ⊢ ₀ >= 0.0
╰─ √₀