虽然传统断言可以增加对 Java 代码执行的检查次数，但有许多检查不能用它们来执行。弥补这一缺陷的方法是使用“时态逻辑”，它是一种用于描述程序状态如何随时间而更改的形式体系。在本文中，Eric Allen 将讨论断言，介绍时态逻辑并描述用于处理程序中时态逻辑断言的工具 （下一篇文章将检查以前的错误模式和时态逻辑的应用程序）。
我们大家同意对 Java 代码检查得越多就越好，我们检查了断言在测试新的和改进的编程中的用法。虽然传统断言可以增加执行的检查次数，但有许多检查不能用它们来执行。
然而，有一个方法可以弥补断言留下的检查缺口。那就是使用 时态逻辑。时态逻辑是用于描述程序状态如何随时间而更改的形式体系。让我们讨论一下断言及其特性，以及时态逻辑是如何适合检查的。然后，我们将研究用于处理时态逻辑断言的工具。
断言及其特性
除了类型检查和单元测试外，断言还提供了一种确定各种特性是否在程序中得到维护的极好方法。
让我们快速浏览三种类型常见的断言特性（虽然是常见的，但它们没有提供我们所需的完整范围），将它们与可以用传统断言语言表示的程序特性的类型进行比较，并检查多线程上下文所必需的，但不可能表示成常规断言的断言特性。我们还将提供一些代码示例。
常见的断言特性
传统上，断言特性分成下面三种类型：
代码块执行之前特性所持有的条件前断言。
代码块执行之后特性所持有的条件后断言。
代码块执行之前和 之后特性所持有的不变断言。
与这些典型形式的断言一样有用，它们不太会有我们希望能在程序中持有的所有特性范围。让我们看一下典型的用断言表示的程序特性。
可表示为断言的程序特性
这只是可以用传统断言语言表示的程序特性类型的简短列表 ― 所有程序员都希望在代码中包含的特性：
确保任何一次性特性都仅生成一次
断言文档决不被未授权的代理程序访问
断言向每个线程提供运行机会
断言系统将决不会使其本身陷入死锁
安全性协议使用一次性特性（使用过一次的数字）生成器来确保事务未被用过。作为安全性中的简单概念，确保一旦生成特殊一次性特性，就不再生成它，这一点很重要。另一个重要的安全性断言是安全文档决不被未授权的代理程序访问。
在多线程代码中，我们希望断言每个线程最终都会有运行机会。我们还希望确保系统决不会使其本身陷入 死锁状态（即在两个或多个线程可以继续处理之前，它们正在彼此等待提供资源）。