Contracts

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.

What it does

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.

What it outputs

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

How to use it

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.

How to interpret the results

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

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:

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.

How contracts interact with other features

What to do next