Formulas¶
A requirement's formula is its logic, from which its circuit is built. It is checked as you type it: the names it reads, with their types, or the mistake and where it is.
Operators¶
From the loosest to the tightest:
| Operator | Meaning |
|---|---|
init -> x |
init at the first step, x after |
a => b |
implies: false only when a holds and b does not |
a or b, a xor b |
or, exclusive or |
a and b |
and |
not a |
negation |
a = b, a <> b, a < b, a <= b, a > b, a >= b |
comparisons |
a + b, a - b |
sum, difference |
a * b |
product |
-a |
negation |
-> and => group to the right: a => b => c is a => (b => c). A
comparison does not chain: write (0 < x) and (x < 10), not 0 < x < 10.
Parentheses group as usual. A chain of one operator (a or b or c) is one
gate with several inputs.
Time¶
| Expression | Meaning |
|---|---|
pre(x, k) |
x k steps before, k from 1 to 100 |
next(x, k) |
x k steps after, k from 1 to 10 |
init -> x |
init at the first step, then x |
x can be any formula. Before the first step, every signal is false, or 0:
pre(x, 1) at the first step is x computed from those values;
init -> pre(x, 1) starts from init instead.
A circuit cannot read the future: a formula whose nexts reach N steps
ahead is built late by N steps. Its Out block at step s is the
requirement at step s − N, and its MC/DC decision counts from step N.
Choice¶
if c then a else b: a when c holds, b otherwise; a and b of one
type. It becomes a Switch.
Names, numbers and types¶
- A name (letters, digits and
_, not starting with a digit) is a signal: an input of the circuit. It is a boolean, unless the table's Signals declare it with another type. - A number (
5,0.5) takes the type of what it is compared or computed with. trueandfalseare the boolean constants.- Keywords may be in capitals:
AND,PRE,IF.
The keywords (and, or, xor, not, if, then, else, pre,
next, true, false) are not names.