Testing

This file has no test in it. kavach test still finds its bug:

fn average(xs: [Int]) -> Int {
    let total = 0
    for x in xs {
        total += x
    }
    total / xs.len()
}

0 passed, 0 failedseed 7✗ average: panicked (division by zero)    stats.kav:6   total / xs.len()  smallest failing input: xs = []  How to fix (pick one):    1. Return an error. Change the signature to `-> Int ! SomeError` and `fail` when the value is bad.       Choose this if the value can come from users, files, the network or AI.    2. Forbid it. Add: require xs.len() != 0       Choose this if such a value here is always a bug in the calling code.    3. Use a default. Add: if xs.len() == 0 { return … }       Choose this if a default is a correct answer.  saved to tests/found/stats.kavf  (replayed on every run)1 functions   0 ✓   1 ✗   0 weakly testednothing checked by hand (no example, ensure, invariant or test) in:  stats.kav

It tried many lists, found the smallest one that crashes, [], and suggests three fixes, each with when to choose it. The failing case is saved and replayed on every later run.

A found case becomes an example

Found cases are saved in tests/found/, one file per module, each line one call. The files are generated: commit them, but never edit them. Once the bug is fixed, kavach test --keep turns each found case that now passes into an example on its function, so it becomes documentation:

fn average(xs: [Int]) -> Int
    require xs.len() <= 1000 and xs.all(x => x >= 0 and x <= 1_000_000)
{
    if xs.len() == 0 {
        return 0
    }
    let total = 0
    for x in xs {
        total += x
    }
    total / xs.len()
}

fn main() {
}

// Found by `kavach test` (spec 11.4). Generated: commit it, never edit it.
average([])

kept: example average([]) == 0

✓ average: example average([]) == 0
1 passed, 0 failed
seed 7
✓ average  200 cases
1 functions   1 ✓   0 ✗   0 weakly tested

• --keep wrote example average([]) == 0 into stats.kav, and the case left tests/found/.
• A case that still fails stays found, and --keep says why.

A case that can't happen any more

Add an invariant to a type after a case was saved, and the case may hold a value no program can build now. It is no case any more, so the run takes it out of its file and says so:

type Run {
    events: [Int]
    passed: Bool

    invariant passed == events.is_empty()
}

fn failed(runs: [Run]) -> Int
    ensure result == runs.count(r => not r.events.is_empty())
{
    runs.count(r => not r.passed)
}

fn main() {
}

// Found by `kavach test` (spec 11.4). Generated: commit it, never edit it.
failed([Run(events: [], passed: false)])

0 passed, 0 failed
seed 7
  dropped a saved case that breaks the invariant `Run: passed == events.is_empty()`: failed([Run(events: [], passed: false)])
✓ failed  200 cases
1 functions   1 ✓   0 ✗   0 weakly tested

Run(events: [], passed: false) breaks passed == events.is_empty(), so the case was dropped and the run went on with the rest.

What you write, what gets tested

• Types and invariants: valid values of every type, edge cases first.
• require and ensure: many inputs that meet the first, each result checked against the second.
• example lines: run as written.
• Capabilities: replaced by fakes, so tests never touch the real world.

What nothing checks yet

Generated tests try every function, but without an ensure or an example they can only check that it doesn't crash, not that its answer is right. So after its results, kavach test says where a person should look first:

/// The price with tax, in cents.
pub fn with_tax(cents: Int) -> Int
    require cents >= 0 and cents <= 1_000_000
    example with_tax(1_000) == 1_180
{
    cents + cents * 18 / 100
}

/// A short label for an order.
pub fn label(id: Int) -> String {
    "order {id}"
}

/// The invoice number for an order.
pub fn number(order: Int) -> String {
    "INV-{order}"
}

use orders.{with_tax, label}
use billing.invoice

fn main() {
    print("{label(7)}: {with_tax(1_000)}, {invoice.number(7)}")
}

✓ with_tax: example with_tax(1_000) == 1_180
1 passed, 0 failed
seed 7
✓ number  200 cases
✓ with_tax  200 cases
✓ label  200 cases
3 functions   3 ✓   0 ✗   2 weakly tested
weakly tested (no contract or example; only checked for panics):
  src/billing/invoice.kav:2   number
  src/orders.kav:10   label
nothing checked by hand (no example, ensure, invariant or test) in:
  src/billing/invoice.kav

• Weakly tested lists each function with no ensure or example: label and number. A require limits the inputs but checks no answer, so it doesn't count.
• Nothing checked by hand lists each module with no example, ensure, invariant or test at all, in the file or in its test file beside it. orders.kav has an example, so only invoice.kav is listed.
• An example line, or an invoice.test.kav beside it, takes a module off the list.