Developer Tools
vcontract
Preconditions, postconditions and invariants, checked every time the code runs.
Released v1.0.0 · 2026-09-28use "stdlib/contract.ven"Design by contract checks, precondition, postcondition and invariant, enforced at the moment a function actually runs rather than proved ahead of time. A violated contract raises a real, catchable error through the same mechanism the assertion package already uses. It makes no claim beyond that: it checks the calls that really happen, and proves nothing about calls that never run.
print contract_violation_text("precondition", "divisor must not be zero")Reference (6 functions)
API reference
contract_violation_text(kind, message)
Formats one contract violation as a raisable Text error.
contract_violation_text("precondition", "divisor must not be zero")requires(predicate, message)
Builds a precondition decorator that checks predicate before every call.
wrap requires(make(a, b) give b != 0, "divisor must not be zero")
make divide(a, b)
give a / b
divide(10, 2)ensures(predicate, message)
Builds a postcondition decorator that checks predicate after every call.
wrap ensures(make(result, a, b) give result >= a, "result must not shrink below a")
make add_positive(a, b)
give a + b
add_positive(3, 4)invariant(predicate, message)
Builds a decorator that checks a shape invariant after a method runs.
behavior Account
wrap invariant(make(self) give self.balance >= 0, "balance can't go negative")
make withdraw(self, amount)
self.balance = self.balance - amount
give self.balance
acct.withdraw(40)check_invariant(instance, predicate, message)
Runs one invariant check against instance right now, raising if it fails.
check_invariant(valid_acct, make(self) give self.balance >= 0, "balance can't go negative")checked_constructor(build_fn, predicate, message)
Builds a constructor wrapper that checks an invariant right after construction.
new_account = checked_constructor(make(*a, **k) give Account(*a, **k), make(self) give self.balance >= 0, "balance can't go negative")
new_account("Bob", 50)