Contracts

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:

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:

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:

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:

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:

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:

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:

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:

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.

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.

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:

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.

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:

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.

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:

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

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.

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).