Chapter 17 — Contracts

A contract is a statement of what a function promises, written right next to its signature, in ordinary Ingle. There are two halves: requires clauses (preconditions — what must be true when you call it) and ensures clauses (postconditions — what will be true when it returns). An ensures clause may use the special name result for the return value.

fn clamp(x: int, lo: int, hi: int) -> int
    requires lo <= hi             // precondition: checked on entry
    ensures result >= lo          // postconditions: checked before every return,
    ensures result <= hi          // with 'result' bound to the returned value
{
    if x < lo { return lo }
    if x > hi { return hi }
    return x
}

That’s not a comment. It’s executable. In a normal (debug) build, requires is checked the moment the function is entered, and every ensures is checked just before each return. If one fails, the program stops with a message that tells you exactly which clause, in which function:

fn pos(x: int) -> int
    requires x > 0
{
    return x
}

fn main() -> int { return pos(-5) }

inglec: runtime error: precondition failed in 'pos' (requires, line 1)

A contract is just a bool expression, so the full language is available — including calling your own predicate functions. You can write requires is_sorted(xs) and define is_sorted normally. (Contracts should read their inputs, not change them.) Here’s the shipped examples/07_contracts.ig, which specifies Euclid’s GCD precisely — the result is positive and divides both inputs:

fn gcd(a: int, b: int) -> int
    requires a > 0
    requires b > 0
    ensures result > 0
    ensures a % result == 0
    ensures b % result == 0
{
    var x = a
    var y = b
    loop {
        if y == 0 { return x }
        let t = x % y
        x = y
        y = t
    }
}

Those three ensures clauses are a real, checkable specification of “is a common divisor,” not a vague comment hoping to stay true.

assert, for checks inside a function

For an invariant that should hold mid-function rather than at its boundary, there’s assert(cond) (or assert(cond, "message")). It lowers to the same machinery as a contract, so a failure is the same kind of structured event, not a bare crash.

The bit that makes it free in production

Contracts are checked in debug builds — the default. A --release build elides them entirely: zero runtime cost. So you get correctness-checking while you develop and pay nothing when you ship. Watch the same broken contract simply vanish under --release:

inglec --emit=run           bad.ig     # precondition failed in 'pos' ...
inglec --emit=run --release bad.ig     # => 6   (the check is gone)

This is the proven debug_assert model: the safety net is up the whole time you’re working, and folded away for the performance run. (Type-checking always happens, in every build — a contract that isn’t a bool is a compile error no matter the profile. Only the runtime check is what --release drops.)

Fireside trivia. Design by contract dates to Bertrand Meyer and the Eiffel language in the 1980s, named by analogy with business contracts: the caller promises the precondition, the function promises the postcondition, and if both keep their word the program is correct. The idea spent decades admired-but-niche. What’s new in Ingle isn’t contracts themselves — it’s fusing them with a machine-readable trace and automatic testing, which is the next chapter, and the whole reason they’re here.