Contracts: example
● Intermediate3 min
example shows one real call and its expected result. kavach test runs every one.
fn double(n: Int) -> Int
require n >= 0 and n < 1_000_000
ensure result >= n
example double(21) == 42
{
n * 2
}The program ran and printed:
kavach run contracts.kav
✓ double: example double(21) == 421 passed, 0 failedseed 7✓ double 200 cases1 functions 1 ✓ 0 ✗ 0 weakly tested
An example is documentation that can't go out of date: editors show it on hover, and a wrong one fails the tests. Examples are left out of the program you ship. A method's examples are run too.
An example sees the clock the generated tests do: 2026-01-01 00:00 UTC, and frozen. So an example that reads the clock gives the same result on any day:
use std.time
/// Days left in a 30-day trial that began at `started` (ms since 1970).
fn days_left(started: Int) -> Int
require started >= 0
example days_left(1_767_225_600_000) == 30
example days_left(1_766_016_000_000) == 16
{
30 - (time.now_ms() - started) / 86_400_000
}
fn main() {
print(days_left(time.now_ms()))
}The program ran and printed:
kavach run example-clock.kav
✓ days_left: example days_left(1_767_225_600_000) == 30✓ days_left: example days_left(1_766_016_000_000) == 162 passed, 0 failedseed 7✓ days_left 200 cases1 functions 1 ✓ 0 ✗ 0 weakly tested