Module testing 

test and property blocks — docs/21-tests-in-beck-and-proof.md §21.2 and §21.3, checked.

This module holds the checked shape of a test. The runner is elsewhere (beck-rt), because running one means driving the same Roles the runtime drives; what belongs here is the part that is a language feature: a clause is typed against the program’s own Event, Command and state types, and an assertion about placement is answered from the compiler’s own data without running anything.

Why a test is clauses rather than statements

§21.2: “A test names a log, an input, and an expectation. The log is the state, because state is a fold — there is no fixture, no factory and no setUp.” Each of the three is a clause, so the checker knows which is which: given is a list[Event] and goes through the real apply_event, when is a Command and goes through the real validate. A test therefore cannot construct a state the program could not reach, which is the property a factory cannot offer.

The row of a test is empty, and that is checked

§21.2’s open question — “Do test blocks have effect rows? They must not” — is settled here as an error, B0700. An expression inside a test performs nothing: a test that could perform net.out is a test that fails when somebody else’s server is down. The subject’s effects are a different matter, and §21.3’s answer is that they are stubbed — see Clause::Stub and the auto-stubbing in the runner.

Structs

Bindings

The three names a test’s expectations may use. They are plain data — a folded state, the events a command produced, and the result of the last one — so every backend can hold them.

TestDef

A checked test or property block.

Enums

Clause

Count

Expectation

Functions

is_auto_stubbable

Which effect atoms a stub can stand in for.

is_stubbable

Whether an atom may be named in a stub clause at all.

performs_itself

Does a definition perform an atom, as opposed to inheriting it from something it calls?