Keyboard shortcuts

Press or to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

The test atom — ox test

A test is a named imperative block, run top-to-bottom against a fresh store. Its name is a string literal; its body is the mutate-body statement set (let / insert / update / delete / for / require and declared mutation/fn calls — mutate, RFD 0015) plus the assert statement:

test "accountBalance derives the posted amount per account" {
    let cash = insert Account { name: "Cash" };
    let rev  = insert Account { name: "Revenue" };
    let e    = insert Entry { memo: "sale 1" };
    postPair(cash, rev, cash, rev, e, 100.50);
    assert accountBalance(cash) == 100.50;   // reads the derived value
    assert accountBalance(rev) == -100.50;
}

An assert mirrors require exactly, with one difference: a failed require aborts the body; a failed assert records a pass/fail outcome and execution continues. true is a PASS, false a FAIL, and an evaluation error (an unbound reference, a non-boolean result, a missing field, a value not derivable in the current state) is an ERROR (the test errors; it never panics). Setup and assertions interleave naturally, so there is no separate fixture block.

Asserting over the deductive plane. A condition that names a derived predicate or a declared pub queryaccountBalance(cash), or the nav-method form x.active_leases() — is evaluated against the reasoner’s materialized extent at the fixpoint of the current committed state, the same read path ox query / ox derive and the for x in <derive> snapshot use. A keyed call (accountBalance(cash)) selects the row whose leading columns match the argument and returns its head-carried value; with no matching row the assert ERRORs (the value is not derivable), and an ambiguous match is a loud error too. Scalar comparisons, field access, arithmetic, and aggregates evaluate as in a require guard. This is the point of testing a reasoning system: an assert checks what the rules derive, not just what was stored.

Asserting derivability — assert [not] derivable F(args). The value-read assert above answers what value a keyed derive carries; the derivability form answers whether a fact holds at all — membership and, crucially, non-derivability. assert derivable F(a, …) passes when a row whose leading columns equal the resolved args is in F’s materialized extent; assert not derivable F(a, …) is its negation. The predicate F resolves the same way the value-read assert and for x in <derive> do — a derive head, a declared pub query, or a base rel. The predicate slot accepts a qualified path (assert derivable students::adult(p), assert not derivable pkg::accounts::adult(p)), resolved by the same ::-suffix matching the rest of the runtime uses: a bare leaf resolves when it is unambiguous, and qualifying disambiguates a name carried by two heads in different modules — that case stays a loud ERROR for the bare form, naming every candidate, so qualification is the way to pick one. Partial args test prefix membership (derivable amtOf(acme) over amtOf(account, money) = “some row has account == acme”); zero args test extent non-emptiness (derivable F()). A predicate that names nothing is a loud ERROR, not a silent outcome. derivable is a contextual keyword — recognized only in leading position after assert / assert not, so it stays usable as an ordinary identifier everywhere else.

The outcome is world-honest and four-valued: the read consults the matching tuple’s truth value — the definite extent, the head’s well-founded-undefined companion, and the explicit refutation extent (pub not_fact) — and only a tuple absent from all three falls to the predicate’s world assumption (World assumptions (CWA / OWA)):

truth of the asserted tupleassert derivable Fassert not derivable F
is — a matching row is present, unrefutedPASSFAIL
not — explicitly refuted, no positive supportFAILPASS
can — a well-founded-undefined standoffINCONCLUSIVEINCONCLUSIVE
both — asserted and refuted (a native contradiction)PASSFAIL
absent, F is closed-world (absence ⇒ not)FAILPASS
absent, F is open-world (absence ⇒ unknown)INCONCLUSIVEINCONCLUSIVE

The can row is the load-bearing case on the deductive plane. An atom the well-founded semantics leaves undefined (a recursion-through-negation standoff, truth values) is neither definitely true nor definitely false — so neither polarity is assertable: a definitely-false atom and an undefined one must never be conflated at this surface, and assert not derivable over an undefined atom is a distinct, loud INCONCLUSIVE, never a silent pass. The teaching detail names the value and the exact-pinning vehicle — a scenario expect row { tuple = [ … ], truth = "Can" } (Scenario harness — ox run-scenario), which pins the third truth value where the polarity form cannot. The both row is the opposite discipline: an overdetermined atom is not unknown — positive support exists, so derivable passes and not derivable fails, the detail naming both. The not row reads an explicit refutation as definite-false under either world assumption: a refutation is present evidence, not open-world absence. The per-tuple classification joins the extents exactly as federation’s information-join does (truth values, can ⊕ not = not): an explicitly refuted standoff is not — the refutation supersedes the undefined companion (and it is not both: a standoff supplies no definite positive support). When a partial-args (prefix) assertion matches several rows, an unrefuted positive match keeps the assertion at plain is (a contradictory sibling row does not mask definite support), and a refutation decides the prefix claim only as far as it reaches: a full-arity refutation refutes exactly the asserted tuple (definite not under either world), while under an open-world predicate a refutation of one tuple beneath a partial prefix leaves the remainder unknown — assert not derivable F(prefix) stays INCONCLUSIVE, the detail naming the near-miss (under a closed world the remainder’s absence is already definite, so the prefix decides).

The open-world absent row is the same soundness case it always was. Under the open-world assumption absence of evidence is not evidence of absence: a missing row is unknown, not false, so closed-world non-derivability is not assertable and must never silently pass. The runner reports a distinct, loud INCONCLUSIVE carrying a teaching detail that names the open-world cause and the two ways forward (assert a positive outcome instead, or mark the concept #[world(closed)] if it should be closed). This composes with the world-honest negation-as-failure of the rule engine: a derivability assert reads the same world each negated atom does.

Asserting rejection — assert rejects [( Pkg::Code )] { … }. Argon is a constraint language; a model’s most important property is which writes its where-invariants and check delta-guards turn away. The two forms above assert positive outcomes — the negative-enforcement half is assert rejects { <mutate-body-stmts> }, which asserts that the block’s write is refused by a write-path guard. The block admits the full mutate-body statement set (insert / insert iof / update / delete / mutation calls); it runs against an isolated copy of the test world, so it commits nothing back regardless of outcome. An optional code pin assert rejects(Pkg::Code) { … } requires the rejection to carry that exact diagnostic code. Like derivable, rejects is a contextual keyword — recognized only in leading position after assert — so it stays usable as an ordinary identifier elsewhere.

The outcome is three-valued, and the guard-vs-non-guard distinction is load-bearing:

block outcomeassert rejectsassert rejects(Code)
a write-path guard refuses the writePASSPASS iff the rejection carries Code, else FAIL (wrong reason)
the block commits with no rejectionFAIL (the write was accepted)FAIL (the write was accepted)
a non-guard error (unbound var, type error, unevaluable)ERRORERROR

A guard rejection is a genuine constraint refusal on the write path — a where-invariant violation (OE0668), a check delta-guard refusal (which is also how a group axiom — disjoint / complete / partition — surfaces, carrying the check’s own Pkg::Code), an insert iof onto a defined (iff) concept (OE0211), a write onto an abstract or fixed-introduced type (OE0233 / OE0234), a construction-completeness refusal (OE0207 / OE1014), a property write to an unclassified individual (OE0238), a relation write over a non-existent endpoint or past a declared cardinality (OE0232 / OE1341), or a typed-slot write whose individual is classified under a concept a declared disjoint / partition group makes disjoint from the slot’s declared concept — refused on both slot planes, a relation endpoint (OE1428) and a concept-typed field (OE1435), because classifying that individual under the slot’s concept would itself violate the group, so the write can never be satisfied in this state or any later one (Group axioms). Only these satisfy rejects.

The declared-disjointness pair is admitted at its write-time codes only. The same disjointness is also refused one plane earlier, at elaboration, wherever the written value’s concept is statically known — the annotated-parameter spelling, where a mutation parameter’s declared concept already contradicts the slot’s (OE1426 endpoints, OE1434 fields). Those build-plane refusals are not observable through rejects at all, and no widening of this set could make them so: they refuse at ox check, so the package produces no artifact and the test run never happens. A reader who spells the disjoint write with an annotated parameter and expects a passing rejection test gets a compile error instead — the fix is to write the block over a value whose conflicting classification is only knowable at write time (an individual bound by an earlier insert in the test body, as the runtime codes above describe), or to pin the build-plane refusal the way every other ox check refusal is pinned, as a refusal fixture rather than a test. A non-guard error — a typo, an unbound reference, a type error, an unevaluable term, a stray require failure — is reported as a loud ERROR, never counted as a rejection: a broken test must never masquerade as a passing rejection test. An accepted write is a FAIL (and is rolled back, like any other block outcome, so it does not pollute the rest of the test). Use the positive forms to test that a legal write is accepted.

Isolation. Each test runs against its own fresh store seeded with the package’s declared facts (the same fresh-store-per-run discipline as the scenario harness, Scenario harness — ox run-scenario). No test sees another’s writes, so tests are order-independent. Within one test, the body’s writes are flushed and the read-model maintained before each assert, so an assert observes every earlier write — including the derived facts they entail (read-your-writes over the committed + deductive state).

Discovery + running. ox test runs every test from two sources, unioned: (1) any test declaration in a mod-reachable module (e.g. tests/mod.ar reached by mod tests;), and (2) every *.ar anywhere under <pkg>/tests/, which ox test auto-discovers (recursive, any depth — a nested tests/sub/foo.ar is discovered too, so no test under tests/ silently fails to run — filename-sorted) and elaborates as part of the package, so each sees the package’s full vocabulary. This mirrors how ox run-scenario auto-discovers scenarios/*.toml: a test placed in the reserved tests/ directory runs without mod-wiring. A tests/ file that is also mod-reachable is folded exactly once (its tests never double-run). A discovered tests/foo.ar references package items by their package-absolute path (pkg::…). This discovery is test-mode only: ox build / ox check and the shipped .oxbin never include tests/*.ar — tests do not ship. Tests are inert at query / serve time; only ox test enumerates and runs them:

ox test <pkg>                 # build the package (+ tests/), run every test, report
ox test <pkg> --filter NAME   # run only tests whose name/path contains NAME

A tests/*.ar with a parse or resolve error fails loudly (ox test aborts with the diagnostic), never a silent skip; a package with genuinely no tests anywhere prints “no tests found” and exits 0.

ox test builds the package (so the run reflects current source), runs every discovered test, and prints a PASS / FAIL / ERROR / INCONCLUSIVE line per test — a failed or inconclusive assertion shows its rendered source text and why it could not pass — followed by an N passed, M failed, K errored, I inconclusive summary. A test’s rollup status takes the strongest of its assertions in the precedence Error > Fail > Inconclusive > Pass. It exits non-zero if any test fails, errors, or is inconclusive (a test you cannot decide is not green), so ox test doubles as a CI-usable gate (like ox run-scenario).

Assertion forms. Three forms are admitted. The value/boolean form is assert <bool-expr>; — scalar comparisons (==, !=, <, <=, >, >=), field access on bound entities (x.field, chained x.a.b), arithmetic on those, the aggregate/comprehension forms, and the deductive-plane reads above (a derived-predicate / pub query keyed call, and the nav-method x.method() form). The derivability form is assert [not] derivable F(args); with the world-honest four-valued semantics above. The rejection form is assert rejects [( Pkg::Code )] { <mutate-body-stmts> } — the negative-enforcement half above. All three are test-only: a stray assert (any form) in a mutate / fn body lowers to an unsupported form and ox check / ox build refuse it up front with OE1318 (the runtime also rejects it, as defense-in-depth) — it is never a silent no-op.

Only the three assert forms above are admitted; anything else is a loud refusal, never a silent pass.