Qualifies assertions with modal
Always, Sometime, Until, Next.
"In the case of digital circuits, assertions like these
are statically verified before the chip is built...
In the case of software, our ability to statically check such assertions
is paltry, but quality tools exist for checking that these assertions hold
during particular runs of the program (such as, say, the runs of your unit tests).
Assertions like these can help you to leverage unit testing to a much greater
degree; each temporal logic assertion can correspond to countless traditional
assertions (and that's just in cases where traditional assertions could be
used to express the assertion at all."
Unfortunately only commercial software is currently available to do these checks.
The next article in the series
"Preventing common bugs with temporal logic assertions"
puts the modal operators to use on different types of bugs.
Posted to OOP by jon fernquest on 8/30/02; 3:50:07 AM