Formulas #

Formulas and temporal operators may sound scary, but fear not — they are essentially ways of expressing “conditions over time”. Here are some quick facts about formulas and temporal operators:

• Temporal operators return formulas.
• Every property in Bombadil is a formula (of the Formula type).
• A temporal operator is a function that takes some subformula and evaluates it over time.
• Different temporal operators evaluate their subformulas in different ways.
• Bombadil evaluates formulas against a sequence of states to check if they hold true.

Temporal operator types include always, as discussed in the example in Extractors above, and also eventually and next. Here’s an informal¹ description of how they work:

• always(x) holds if x holds in this and every future state
• next(x) holds if x holds in the next state
• eventually(x) holds if x holds in this or any future state

They accept subformulas as arguments. You’ll notice in the example with always above, the argument was a thunk. This still works, because the operators automatically convert thunks into formulas. In fact, there’s an operator for doing that explicitly, called now:

always(now(() => title.current !== ""))

You normally don’t have to use the now operator, unless you want to use logical connectives at the formula level. They are defined as methods on formulas:

• x.and(y) holds if x holds and y holds
• x.or(y) holds if x holds or y holds
• x.implies(y) holds if x doesn’t hold or y holds

There’s also negation, both as a function and as a method on formulas, i.e. not(x) and x.not().

The now operator is useful when expressing single-state preconditions. The following property checks that pressing a button shows a spinner that is eventually hidden again:

const buttonPressed = extract(() => ...);
const spinnerVisible = extract(() => ...);

now(() => buttonPressed.current).implies(
    now(() => spinnerVisible.current)
        .and(eventually(() => !spinnerVisible.current))
)

You can build more advanced formulas, and even include nested temporal operators, but the basics are often powerful enough. See the examples at the bottom for more inspiration.