Contracts and Tests

A contract says what a function needs and what it promises. You write it once, and SSPUR uses it four ways: it checks it at run time, turns it into property tests, tries to prove it, and drops runtime checks it has proved.

pre, post and where

fn find_slot(sorted: List[Int], x: Int, lo: Int, hi: Int) -> Int
  pre 0 <= lo and lo <= hi and hi <= sorted.len
  post r >= lo and r <= hi
= if lo >= hi then lo else do
  m = (lo + hi) / 2
  if sorted[m] < x then find_slot(sorted, x, m + 1, hi) else find_slot(sorted, x, lo, m)

pre is what callers must guarantee about the arguments.
post is what the function guarantees. r is the result.
where on a parameter, field or type alias is a condition on one value, with _ for the value (Everyday Types).

All three are checked whenever the function runs, and a violation stops the program with the clause that failed. Contracts must be pure.

Tests and examples

test name = expr is a named Bool expression. ex lines on a function are examples that run as tests:

fn slot(sorted: List[Int], x: Int) -> Int
  ex slot([1, 3, 5], 4) == 2
  ex slot([], 7) == 0
= find_slot(sorted, x, 0, sorted.len)

test slot_front = slot([10, 20], 5) == 0
test slot_back = slot([10, 20], 25) == 2

$ sspur test contracts.ssp
4 passed, 0 failed

A failing test prints the values it compared (FAIL bad: left 7, right 8), in sspur test and in sspur edit --test, so you rarely need to add logging.

Fuzzing

Here is a function with a plausible contract and a bug in it:

fn average(total: Int, n: Int where _ > 0) -> Int
  post r * n <= total
= total / n

sspur fuzz generates arguments that satisfy every pre and where, runs each function, and checks post on every result. It shrinks a failing input to a small one:

$ sspur fuzz contracts.ssp
FAIL  average(-1, 2): contract violated: post r * n <= total in average (r = 0)
ok    find_slot (36 cases, 3964 discarded)
ok    slot (200 cases, 0 discarded)

Int division truncates toward zero, so for a negative total the average is too large. “Discarded” counts generated inputs that didn’t meet pre. sspur fuzz --differential also compares native code against the interpreter on every input.

Proving

sspur verify hands the contracts to Z3 and tries to prove each clause for every input. Calls are checked against the callee’s contract, not its body, so pre is proved at each call site, including the recursive ones:

$ sspur verify contracts.ssp
fn find_slot
  pre 0 <= lo and lo <= hi and hi <= sorted.len proved: at 3 call sites
  post r >= lo and r <= hi                     proved
fn average
  n where _ > 0                                no callers
  post r * n <= total                          counterexample: average(total = -1, n = 2): contract violated: post r * n <= total in average (r = 0)
2 proved, 1 counterexample, 0 unknown; 8 of 8 runtime checks proved safe

Each clause is proved, a counterexample (with concrete inputs, confirmed by running them), or unknown. Native code leaves out every check Z3 proved can’t fail, so contracts like pre lo <= hi and post r >= lo make code faster rather than slower. Fix average by declaring total: Int where _ >= 0 and both tools pass.

verify needs z3 on the PATH.

Filling holes from the tests

A ? or ?name in an expression is a typed hole. The checker reports its type, and when the program has no errors it also searches for expressions that fit: small combinations of the values in scope, fields, constructors, your functions and the everyday methods of lists, strings and options. Each candidate runs against the tests and examples that reach the hole and against fuzzed inputs of the function, so the contracts get a say too:

type Line = {sku: Str, qty: Int where _ > 0, price: Int where _ >= 0}

fn subtotal(lines: List[Line]) -> Int
  post r >= 0
= ?subtotal

test none = subtotal([]) == 0
test two = subtotal([Line{sku: "a", qty: 2, price: 5}, Line{sku: "b", qty: 3, price: 4}]) == 22

$ sspur fill holes.ssp
?subtotal: lines.map(_.qty * _.price).sum (passes 2 tests, post)

sspur check lists up to three passing candidates under each hole; when others pass the same checks, the evidence ends with N others also fit, which means a test that tells them apart is missing. --json gives each one as a fill op you can apply. sspur fill --apply writes the best one in. A candidate never uses an effect the function doesn’t declare. The search is small and has a time budget (400 ms a hole in check), so a long expression won’t be found; write the part you know and leave a smaller hole.

Suggested contracts

sspur suggest works the other way round. It runs each function on the arguments its tests pass and on fuzzed ones, then proposes the post clauses that held on every run and a pre that rules out the inputs it trapped on:

fn mean(xs: List[Int]) -> Int
= xs.sum / xs.len

fn keep(xs: List[Int], n: Int) -> List[Int]
= xs.take(n)

$ sspur suggest holes.ssp
keep
  post r.len <= xs.len  // proved
mean
  pre xs.len > 0  // traps on 1 of 175 inputs without it

A clause Z3 proves says proved; the rest only held on the runs, so read them before you keep them. Nothing changes until you pass --apply.

Next: Generics and Traits.

Keyboard shortcuts