Contracts and tests

contracts/main.xo

struct Account { id: Int, balance: Int } invariant balance >= 0

enum TxErr { Insufficient } derive Display

fn withdraw(a: Account, amount: Int) -> Account ! TxErr
  requires amount > 0
  requires a.balance >= amount else TxErr.Insufficient
  ensures result.balance == a.balance - amount
{
  a with {balance: a.balance - amount}
}

fn main(os: Os) {
  let a = Account{id: 1, balance: 50}
  match withdraw(a, 80) {
    Ok(b) => os.stdio.println("left ${b.balance}")
    Err(Insufficient) => os.stdio.println("insufficient funds")
  }
}

test "withdraw lowers the balance" {
  let b = withdraw(Account{id: 1, balance: 50}, 20)?
  expect(b.balance) == 30
}

test "reverse twice" for xs: List[Int] {
  expect(xs.reverse().reverse()) == xs
}

Output:

insufficient funds

requires amount > 0 faults when violated: passing a negative amount is a bug in the caller. requires ... else TxErr.Insufficient returns an error instead: running out of money is an expected outcome.
ensures checks the result; invariant is checked whenever an Account is built or changed.
test "name" { ... } blocks live next to the code. expect(x) == y prints both sides when it fails.
test "reverse twice" for xs: List[Int] is a property test over generated lists.
xo test also fuzzes every function that has contracts, with inputs that satisfy its requires. That is why this module reports three passing tests for two test blocks. A failure found this way is shrunk and saved as a regression test.

Docs

Tour

Reference

Contracts and tests