You hire a contractor to renovate your kitchen. Before work starts, you agree on the terms: the budget is $3,000 and the plumbing has to pass inspection. Those terms are the contract. If the contractor tears out a wall and finds rot, the budget might change, but the contract makes the change explicit. No $5,000 bill by surprise.
Software has the same problem. A function accepts certain inputs and promises certain outputs, but those promises usually live in the programmer's head or in a comment that falls out of date. When the function changes, nothing enforces the old promises. Bugs happen in the gap between what a function used to guarantee and what it actually does now.
Contracts make those promises explicit, and the machine checks them for you.
Vary has three kinds of contracts, each written as a block at the top of a function body.
A precondition says "do not call me unless these things are true." If a caller breaks this rule, the program fails immediately with a clear error instead of producing a wrong answer silently.
def divide(a: Int, b: Int) -> Int {
in {
b != 0
}
return a // b
}
That in {} block runs before the function body. If b is zero, you get a ContractViolation error pointing at the exact condition that failed. No division by zero. No mysterious Infinity return value that corrupts data downstream.
You can check multiple conditions:
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
}
Each condition is checked independently. If lo > hi, you find out before the function does anything at all.
An out(r) {} block names the return value and checks conditions about it after the function finishes:
def abs_val(x: Int) -> Int {
out(r) {
r >= 0
}
if x < 0 {
return -x
}
return x
}
Every return path goes through the out check. If any code path accidentally returns a negative number, the contract catches it. This is not a test you run separately. It is baked into the function itself.
For functions that modify state (like methods on a class), post {} checks conditions after the body runs. Combined with old(), which snapshots a value at function entry, you can express relationships between the before and after:
class Account {
mut balance: Int = 0
def deposit(self, amount: Int) -> None {
in { amount > 0 }
post { self.balance == old(self.balance) + amount }
self.balance = self.balance + amount
}
}
That post block says: after deposit runs, the balance must equal whatever it was before plus the amount deposited. If someone later refactors deposit and introduces a rounding error or an off-by-one, the contract fires on the first call.
A test verifies specific examples. A contract verifies a rule that holds for every call, forever. When new team members add features, they do not need to know which examples the original author thought were important. The contract tells them what the function promises.
# b must not be zero <-- a human might ignore this
def divide(a: Int, b: Int) -> Int {
return a // b
}
versus:
def divide(a: Int, b: Int) -> Int {
in { b != 0 } # <-- the machine enforces this
return a // b
}
The comment and the contract say the same thing. The difference: the comment is a suggestion. The contract is a wall.
This is the part specific to Vary. The compiler has mutation testing built in, where it makes small changes to your code and checks whether tests catch them. Contract violations count as kills. If a mutant changes self.balance + amount to self.balance - amount, the post {} contract fires and the mutant is dead. No test needed.
In practice, functions with good contracts tend to have high mutation scores without many tests. The contracts already catch deviations from the specified behaviour, so the mutation engine has less work to do.
Classes and data types can declare invariants that are checked after construction:
data PositivePoint {
invariant {
self.x > 0
self.y > 0
}
x: Int
y: Int
}
Try to create PositivePoint(-1, 5) and you get a ContractViolation. The type system guarantees the struct exists. The invariant guarantees it makes sense.
pure def is related to contracts in spirit: it is a promise that a function has no side effects. The compiler enforces this statically (not at runtime). A pure function cannot call print, read files, or modify global state:
pure def add(a: Int, b: Int) -> Int {
return a + b
}
If you try to call an impure function from inside a pure def, the compiler rejects it. This matters for mutation testing: pure functions are deterministic, so every mutant produces a stable, reproducible result. No flaky failures from timing or randomness.
A function can use in, post, and out together. They run in order: precondition first, then the body, then state postcondition, then return postcondition.
def withdraw(self, amount: Int) -> Int {
in {
amount > 0
amount <= self.balance
}
post { self.balance >= 0 }
out(r) { r == amount }
let prev = self.balance
self.balance = self.balance - amount
return amount
}
That is four promises in six lines: the amount is positive, the account has enough, the balance stays non-negative, and the returned value equals what was requested. If any future change to withdraw breaks any of these, the contract fires on the first call that hits the violation.
Contracts do not replace tests.
Use contracts when you can state a rule that should hold for every possible call: "the denominator is never zero," "the output is always positive," "the balance changed by exactly the deposited amount."
Use tests when you need to check specific scenarios, integration behaviour, or outcomes that depend on multiple components working together.
The strongest code has both. Contracts catch the structural guarantees, tests check specific scenarios, and mutation testing tells you whether the combination actually covers what you think it does.