虽然传统断言可以增加对 Java 代码执行的检查次数，但有许多检查不能用它们来执行。弥补这一缺陷的方法是使用“时态逻辑”，它是一种用于描述程序状态如何随时间而更改的形式体系。在本文中，Eric Allen 将讨论断言，介绍时态逻辑并描述用于处理程序中时态逻辑断言的工具。
我们大家同意对 Java 代码检查得越多就越好，我们检查了断言在测试新的和改进的编程中的用法。虽然传统断言可以增加执行的检查次数，但有许多检查不能用它们来执行。
然而，有一个方法可以弥补断言留下的检查缺口。那就是使用 时态逻辑。时态逻辑是用于描述程序状态如何随时间而更改的形式体系。让我们讨论一下断言及其特性，以及时态逻辑是如何适合检查的。然后，我们将研究用于处理时态逻辑断言的工具。
断言及其特性
除了类型检查和单元测试外，断言还提供了一种确定各种特性是否在程序中得到维护的极好方法。
让我们快速浏览三种类型常见的断言特性（虽然是常见的，但它们没有提供我们所需的完整范围），将它们与可以用传统断言语言表示的程序特性的类型进行比较，并检查多线程上下文所必需的，但不可能表示成常规断言的断言特性。我们还将提供一些代码示例。
常见的断言特性
传统上，断言特性分成下面三种类型：
?代码块执行 之前特性所持有的条件前断言。
?代码块执行 之后特性所持有的条件后断言。
?代码块执行 之前和 之后特性所持有的不变断言。
与这些典型形式的断言一样有用，它们不太会有我们希望能在程序中持有的所有特性范围。让我们看一下典型的用断言表示的程序特性。
可表示为断言的程序特性
这只是可以用传统断言语言表示的程序特性类型的简短列表 ― 所有程序员都希望在代码中包含的特性：
?确保任何一次性特性都仅生成一次
?断言文档决不被未授权的代理程序访问
?断言向每个线程提供运行机会
?断言系统将决不会使其本身陷入死锁
安全性协议使用一次性特性（使用过一次的数字）生成器来确保事务未被用过。作为安全性中的简单概念，确保一旦生成特殊一次性特性，就不再生成它，这一点很重要。另一个重要的安全性断言是安全文档决不被未授权的代理程序访问。
在多线程代码中，我们希望断言每个线程最终都会有运行机会。我们还希望确保系统决不会使其本身陷入 死锁状态（即在两个或多个线程可以继续处理之前，它们正在彼此等待提供资源）。
基本的非常规断言特性
下面是我们希望获得的（通常想要在多线程代码环境中获得的）两种非常有用的特性类型，不可能仅用常规断言来表示它们：
?安全断言
?生存断言
安全断言声明某些不合需要的系统状态将决不在任何环境下起作用。生存断言声明保证最终发生某些事件 ― 例如，给定的线程将最终被唤醒，而不是永远休眠。
时态逻辑可以帮助产生这些断言。
时态逻辑出现在何处
这样的断言超出普通断言语言的表示，但可以用形式体系和工具来表示这种语句。我们将这种形式体系称为 时态逻辑。
已定义的时态逻辑
时态逻辑是一种 模态逻辑，用于推理随时间而更改的特性。
请始终记住，有两种常规的时态逻辑：
?把未来当作为事件的线性序列的模型
?把未来当作为具有各种可能性的树型分叉的模型
在本文中，我们将只考虑把未来当作为事件的线性序列模型的时态逻辑。（“分叉树”逻辑非常酷，但它在计算上很难处理。）
通常，时态逻辑构建于一组更简单的原子（小单元）命题之上，如传统程序断言。于是，各种模态操作符都可以应用于这些原子断言以生成更复杂的断言。传统的布尔逻辑操作符（如 与(and) 或 或(or) ）可应用于这些断言以生成甚至更复杂的断言。新生成的断言仍可以生成更复杂的断言，并且可以无限地生成下去。
时态逻辑使用三个（或四个，取决于模型）常见的模态操作符。
典型的模态操作符
通常，下列模态操作符可用于时态逻辑：
?Always
?Sometime
?Until
?Next （特殊情况）
当应用于断言时， Always 确保断言在整个程序执行的剩余部分继续保持。
从意义上说，操作符 Sometime 与 Always 是亲戚，但弱得多。当应用于断言时， Sometime 规定一定要在程序执行的今后时间内存在某些断言可以起作用的时间点。
Until 应用于两个断言，它规定一旦第一个断言停止作用，此后，第二个断言就必须保持有效。
当时间可以是由一系列不连续步骤（比如，程序执行期间）组成的模型时，您有时候会看到 Next 操作符被添加到这个着名的列表中。当 Next应用于断言时，它规定断言在“下一个”步骤中保持有效。当然，仅当我们将时间分割成不连续步骤时，这才有意义。
清单 1 显示了一些时态逻辑断言示例：
清单 1. 样本时态逻辑断言
Always x != 0
Sometime x == 0
{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 进行编译可以使断言免受任何影响）。
结束语
这类时态逻辑可以帮助您将单元测试提升到更高的程度，因为每个时态逻辑断言都可以与许多传统断言对应。这意味着这些断言是如此强大，以致可以有力地帮助消除本专栏文章中讨论的许多典型的错误模式。
责任编辑：小草
