Checks and examples

Tests in RCE are part of the program, not a separate file. A program whose tests fail is not accepted at all.

check

You have already seen check: a bool expression that must be true. The checker evaluates every check while it checks the program.

intent and example

An intent says in words what a piece of code is for, and holds the tests that pin it down:

intent "a counter that never goes below zero"
    example Inc, Inc, Dec -> 1
    example Dec -> refused: Underflow

state Counter
    n: u64 = 0

event Inc
event Dec

error Underflow

step Counter on Inc -> n + 1
step Counter on Dec -> try n.checked_sub(1) else Underflow

The parts after the intent (state, event, step) are the subject of the next chapter. For now, read the two examples:

• example Inc, Inc, Dec -> 1 means: start from the initial state, apply the events Inc, Inc, Dec, and the counter must then be 1.
• example Dec -> refused: Underflow means: applying Dec to a fresh counter must be refused with the error Underflow.

rce test reports how many examples and checks each file has:

$ rce test counter.rce
ok counter.rce (2 examples, 0 checks)
1 passed, 0 failed
exit status: 0

A failing example is a refused program

Change the expected value and the program is refused:

intent "a counter"
    example Inc, Inc -> 3

state Counter
    n: u64 = 0

event Inc

step Counter on Inc -> n + 1

$ rce check wrong_example.rce
REFUSED wrong_example.rce: line 2: W-INT-1 example does not hold: final value is 2, expected 3
exit status: 1

This is the admission rule W-INT-1: every check and every example must hold for the program to be admitted. rce test and rce check give the same verdict; rce test also counts the cases.

What an example compares

When the program has one state with one field, the value after -> is compared with that field. Otherwise the part after -> must be a bool expression over the final state, such as light == Yellow or items == ["jam"] and adds == 2. Chapter 10 has an example of the second kind.

What you learned

• check and example are tests that live in the program.
• A program whose tests fail is refused (rule W-INT-1).
• rce test runs the same checks as rce check and counts them.