{x == y} implies {Next {x == y + 1}}
{x == y} Until {y == 0}
{x == 0} implies {Next {Always {x != 0}}} // x is zero only once
Sometime {! this.isInterrupted()} // this thread is not interrupted forever
下面是两个断言它们从不死锁的线程的示例断言。（注：布尔方法 isWaitingOn 用于检查一个线程是否被另一个线程执行的任务挂起。）
清单 2. 说明多线程的样本
Always {x.isWaitingOn(y) implies {! y.isWaitingOn(x)}}
可以扩展时态逻辑。
扩展语言
我们还可以扩展时态逻辑的语言以包括数据库中值集合的量词。例如，我们可以检查断言是否始终对表中的所有值保持有效或者至少对表中的一个值保持有效。
有了这种级别的表示，我们可以构成非常强大的安全和安全性断言。例如，考虑显式代理对象可以请求访问各种文档的环境。我们可以组成清除可以查看各种文档的代理的断言。
下列断言保证没有一个代理可以查看文档，直到他让明确可以有权这样做：
清单 3. 说明数据库安全性的样本
ForAll agents in AgentPool
{ForAll document in TopSecretDocumentPool
{{! agent.canView(document)} Until {agent.hasClearanceFor(document)}}}
如何检查时态逻辑？
现在，您可能会提出异议：“喔！我可以 讲所有这些事情真是太棒了，但我无法检查我所讲的是否正确，那么问题在哪里呢?!”
对此我要说的是：有专门检查这些类型的断言的工具。在数字电路中，在构建芯片之前，先静态地验证这类断言。
在软件中，我们静态检查这种断言的能力是微不足道的，但存在用于检查这些断言在程序的特殊运行（例如，单元测试的运行）期间是否保持有效的品质工具。这样的断言可以帮助您将单元测试提升到很高的程度；每个时态逻辑断言都可以与无数的传统断言对应（并且只是在传统断言完全可以用来表示断言的情况下）。
Time Rover Inc. 的 Temporal Rover 是一种用于处理 Java 程序中时态逻辑断言并根据断言生成有效 Java 代码的工具。该公司还提供用于数据库表的工具 DBRover。
Temporal Rover 包括所有时态操作符以及为讨论过去发生的事件而设计的其它操作符。DBRover 可以以数据库中值量化断言。不幸的是，这些工具不是免费的，但它们提供了 30 天的免费试用版本。
与 JUnit 中的断言相似，Temporal Rover/DBRover 断言为程序员提供了在断言失败时打印诊断消息的选项。实际上，Temporal Rover 断言的语法与我在上面示例中使用的语法相同，其中，模态操作符采用的断言用花括号括起。然后，这些断言被传递到具有下列语法的 TRAssert 函数（Temporal Rover Assert）：
/* TRAssert{<assertion> => <output string>}
＜output string＞是在断言无法保持有效时显示的。这样， TRAssert 语句就可以嵌入到有效的 Java 程序，并且这些程序仍可以不用 Temporal Rover 进行编译（当然，不用 Temporal Rover 进行编译可以使断言免受任何影响）。
结束语
这类时态逻辑可以帮助您将单元测试提升到更高的程度，因为每个时态逻辑断言都可以与许多传统断言对应。这意味着这些断言是如此强大，以致可以有力地帮助消除本专栏文章中讨论的许多典型的错误模式。
