Functions can declare preconditions and postconditions. These are boolean expressions that the runtime checks on every call. A failed contract throws `ContractViolation`. There are three contract forms: `in {}` for preconditions, `post {}` for state postconditions, and `out(r) {}` for return-value postconditions.

## Preconditions

An `in {}` block at the start of a function body declares what must be true when the function is called:

```vary
def divide(a: Int, b: Int) -> Int {
    in {
        b != 0
    }
    return a // b
}

divide(10, 2)   # returns 5
divide(10, 0)   # throws ContractViolation
```

Multiple expressions are allowed. Each one is checked independently:

```vary
def clamp(x: Int, lo: Int, hi: Int) -> Int {
    in {
        lo <= hi
        hi - lo > 0
    }
    if x < lo {
        return lo
    }
    if x > hi {
        return hi
    }
    return x
}
```

Preconditions run after parameter binding and before the first body statement. They can reference any parameter.

## State postconditions

A `post {}` block declares what must be true after the function body runs. This is the contract form for void functions and side-effect assertions:

```vary
class Account(balance: Int) {
    mut balance: Int = balance

    def deposit(self, amount: Int) -> None {
        in { amount > 0 }
        post { self.balance == old(self.balance) + amount }
        self.balance = self.balance + amount
    }
}
```

`post {}` checks run after the function body completes, before control returns to the caller. Multiple expressions are allowed, each checked independently. `old()` is allowed inside `post {}` to compare post-call state against the pre-call snapshot.

Multiple `post {}` blocks can appear on the same function. They are checked in order.

## Return-value postconditions

An `out (result) {}` block declares what must be true about the return value:

```vary
def abs_val(x: Int) -> Int {
    out (r) {
        r >= 0
    }
    if x < 0 {
        return -x
    }
    return x
}
```

The name inside the parentheses (`r` above) binds the return value so postcondition expressions can reference it. Every `return` statement and every fall-through path goes through the postcondition check before the value is actually returned.

`out(r)` requires a non-`None` return type. For void functions, use `post {}` instead. Writing `out(_)` is a compile error that directs you to use `post {}`.

All three contract forms can appear together. The required order is `in` then `post` then `out`:

```vary
def double_positive(x: Int) -> Int {
    in {
        x > 0
    }
    post {
        True
    }
    out (r) {
        r > x
    }
    return x * 2
}
```

Evaluation order: preconditions run first, then the body, then `post` checks, then `out` checks. If the precondition fails, the function body never runs and neither postcondition is evaluated. If a `post` check fails, `out` is not evaluated.

## old()

Inside `post {}` or `out(r) {}`, `old(expr)` captures the value of an expression at the moment the function was called, before the body executes:

```vary
def increment(x: Int) -> Int {
    out (r) {
        r == old(x) + 1
    }
    return x + 1
}
```

`old()` evaluates its argument at function entry and saves the result. When the postcondition runs after the body, `old(x)` produces the saved value rather than the current one.

This is useful when parameters are immutable (which they are in Vary), but becomes essential for contracts on methods that mutate object state: you can compare the post-call state against the pre-call snapshot.

## ContractViolation

When a precondition or postcondition fails, the runtime throws `ContractViolation`. This is a subtype of `Error`, so it works with `try/except`:

```vary
def divide(a: Int, b: Int) -> Int {
    in {
        b != 0
    }
    return a // b
}

def main() {
    try {
        divide(10, 0)
    } except ContractViolation as e {
        print("Contract failed")
    }
}
```

The error message includes the kind of violation (pre or post), the function name, the failing expression as source text, and the file and line number:

```text
ContractViolation(pre: divide: [b != 0] at math.vary:3)
```

## Contracts and mutation testing

Contracts are treated as stable oracles by the mutation runner. `vary mutate` does not mutate expressions inside `in {}`, `post {}`, or `out {}` blocks, for the same reason it does not mutate `observe` expressions: the contract is the specification, not the code under test.

When a mutant changes a function's behaviour, a postcondition violation throws `ContractViolation`, which the runner counts as a kill. This means contracts strengthen your mutation score without writing additional test code.

```vary
def abs_val(x: Int) -> Int {
    out (r) {
        r >= 0
    }
    if x < 0 {
        return -x
    }
    return x
}

test "abs of negative" {
    observe abs_val(-3) == 3
}
```

If a mutant changes `return -x` to `return x`, the test catches it via `observe`. If a different mutant changes `x < 0` to `x < 1`, the postcondition catches it when `abs_val(0)` is called from anywhere, not just from the test.

## Contracts and validation

`vary validate` detects contract violations that occur during test execution and reports them in a structured block. This surfaces violations that might otherwise appear as opaque test failures.

```bash
vary validate --only contracts src/
```

When a test triggers a contract violation, the output shows the kind (PRE or POST), the function name, file and line, and the failing expression:

```text
vary validate · contracts · FAILED

CONTRACTS   2 violation(s)

CONTRACT VIOLATIONS (2)

  1) PRE  submit_order
     src/engine/exchange.vary:42
     amount > 0

  2) POST  match_orders
     src/engine/matching.vary:88
     old(book.size) <= book.size
```

In the default profile (`vary validate`), contract violations appear alongside normal test output. With `--only contracts`, only the contract summary is shown.

If no test files are found, the output reads `CONTRACTS   not exercised (no tests found)`. If tests run but no contracts are violated, it reads `CONTRACTS   no violations`.

## Pure functions

The `pure` modifier marks a function as side-effect-free. The type checker enforces that pure functions only call other pure functions and do not perform I/O, mutate module-level state, or call impure builtins like `print`.

```vary
pure def add(a: Int, b: Int) -> Int {
    return a + b
}

pure def quadruple(x: Int) -> Int {
    return add(add(x, x), add(x, x))
}
```

A pure function that tries to call an impure function produces a compile error:

```vary-snippet
pure def bad(x: Int) -> Int {
    print(str(x))   # error: pure function cannot call impure function 'print'
    return x
}
```

Pure functions can have contracts (`in`/`post`/`out`). Purity helps mutation testing by creating deterministic regions where survivors are easier to diagnose.

## Invariants

Classes and data types can declare an `invariant {}` block. The runtime checks every expression in the block after construction completes. A failed invariant throws `ContractViolation`.

```vary
class BoundedCounter(value: Int, max_val: Int) {
    invariant {
        self.value >= 0
        self.value <= self.max_val
    }
    let value: Int = value
    let max_val: Int = max_val
}

let c = BoundedCounter(5, 10)   # passes
let bad = BoundedCounter(-1, 10) # throws ContractViolation
```

Data types support invariants too:

```vary
data PositivePoint {
    invariant {
        self.x > 0
        self.y > 0
    }
    x: Int
    y: Int
}

let p = PositivePoint(3, 5)    # passes
let bad = PositivePoint(-1, 5)  # throws ContractViolation
```

The invariant block must appear before any field or method declarations. Each expression is checked independently. Invariant expressions can reference `self` and any fields declared on the type.

## Restrictions

| Rule | Details |
|------|---------|
| `out(r)` needs a return type | `out(r)` requires a non-`None` return type. Use `post {}` for void functions. |
| `out(_)` is not allowed | Use `post {}` for state postconditions; `out(r)` requires a named binding. |
| `old()` placement | `old()` can appear inside `post {}` and `out {}` blocks. |
| No shadowing | The `out` variable name cannot shadow a parameter name. |
| Ordering | `in` must appear before `post`, which must appear before `out`. |
| Position | Contract blocks must appear before any body statements. |
| Contextual keywords | `post`, `out`, and `old` are contextual keywords. They can still be used as variable names outside of contract blocks. |

## When to use contracts

Contracts are useful for documenting and enforcing function-level invariants that should hold regardless of how the function is called. They complement tests: a test checks specific inputs and outputs, while a contract checks a property over all calls.

| Technique | What it checks | When it runs |
|-----------|---------------|-------------|
| `observe` in test | Specific input/output pair | During `vary test` |
| `in {}` precondition | Caller responsibilities | Every call at runtime |
| `post {}` state postcondition | Side-effect guarantees | Every call at runtime |
| `out(r) {}` return postcondition | Return-value promises | Every call at runtime |

Preconditions are useful for functions with restricted domains (no division by zero, no negative indices, range constraints). `post {}` is useful for void methods that mutate state, where you want to assert the state transition is correct. `out(r) {}` is useful for functions where the return value has a known structural property (always positive, always sorted, length preserved).