Lambda the Ultimate

"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.