Contracts serve two roles in mutation testing: they act as runtime oracles that kill mutants without dedicated tests, and their clauses are mutated to measure whether your tests exercise the boundaries contracts define.
For contract syntax (in {}, out (r) {}, post {}), see Contracts. For an overview of all advanced features, see Advanced overview.
When you run vary mutate, the engine treats contract violations as kills. A mutant that changes return -x to return x in a function with out (r) { r >= 0 } gets killed when called with a negative input, without you writing a specific test for it.
def abs_val(x: Int) -> Int {
out (r) {
r >= 0
}
if x < 0 {
return -x
}
return x
}
Separately, the engine generates mutants that target the code constrained by each contract clause using dedicated contract_precondition and contract_postcondition operators. These mutants are tracked in the contract adequacy score.
The mutation summary shows contract kills:
Killed by contracts: PRE: 2, POST: 5
The contract adequacy score measures what fraction of contract-related mutants were killed:
Contract adequacy: 85% (17/20 obligations killed)
Gaps: 3 undefended contract boundaries
When contract mutants survive, the engine reports which clauses are undefended:
Contract gaps:
withdraw() out(r) { r >= 0 } — no test triggers violation
transfer() in { amount > 0 } — precondition never falsified
Write contracts on functions where correctness has clear boundaries:
def withdraw(balance: Int, amount: Int) -> Int {
in {
amount > 0
amount <= balance
}
out (r) {
r >= 0
r == balance - amount
}
return balance - amount
}
Run mutation testing normally. Contract kills happen automatically:
vary mutate account.vary --tests test_account.vary
Set a contract adequacy threshold in vary.toml:
[mutation]
min_contract_adequacy = 90.0 # Fail if contract adequacy < 90%
When the threshold is set, vary mutate exits with code 1 if contract adequacy falls below it.
A surviving contract mutant means the contract exists but nothing in the test suite exercises the boundary it defines. The contract is undefended.
A project can have a high code mutation score but low contract adequacy. This means the tests are strong on implementation details but weak on specification boundaries.
Each gap points to a contract clause that no test exercises. The fix is usually a test that calls the function with inputs that would violate the contract if the implementation were wrong.
Contract strength measures how much a contract actually constrains program behaviour. A function can have contracts that look comprehensive but only catch a narrow slice of mutations. The strength score quantifies that.
Contract strength
process_order() 87% strong
validate_input() 45% weak
abs_val() 92% strong
The score combines four dimensions:
| Dimension | What it measures |
|---|---|
| Reach | Fraction of mutants in the function that contracts kill |
| Specificity | How many distinct mutation types contracts catch (not just one kind) |
| Boundary sensitivity | Whether contracts catch boundary mutations (off-by-one, boundary shift) |
| Redundancy | Whether multiple contract clauses catch the same mutants (diminishing returns) |
A "weak" contract typically has high reach but low specificity: it catches arithmetic mutations but misses boundary cases. The fix is usually adding a boundary-sensitive clause to the precondition or postcondition.
| Feature | Role |
|---|---|
in {} / out {} / post {} | Define the obligations |
invariant {} | Obligations on construction |
observe | Test-side oracle that can kill contract mutants |
--why | Explains why a contract mutant survived |
| Contract adequacy score | Measures obligation coverage |
| Integrity score | Contract adequacy contributes 20% weight |
| Page | Topic |
|---|---|
| Observability | Understand why survivors escaped |
| Oracle analysis | Check whether tests have strong oracles |
| Advanced overview | See how contracts fit the five-pillar model |