诊断Java代码: Java编程中的断言和时态逻辑 - 编程入门网

诊断Java代码: Java编程中的断言和时态逻辑

虽然传统断言可以增加对 Java 代码执行的检查次数，但有许多检查不能用它们来执行。弥补这一缺陷的方法是使用“时态逻辑”，它是一种用于描述程序状态如何随时间而更改的形式体系。在本文中，Eric Allen 将讨论断言，介绍时态逻辑并描述用于处理程序中时态逻辑断言的工具 （下一篇文章将检查以前的错误模式和时态逻辑的应用程序）。

我们大家同意对 Java 代码检查得越多就越好，我们检查了断言在测试新的和改进的编程中的用法。虽然传统断言可以增加执行的检查次数，但有许多检查不能用它们来执行。

然而，有一个方法可以弥补断言留下的检查缺口。那就是使用 时态逻辑。时态逻辑是用于描述程序状态如何随时间而更改的形式体系。让我们讨论一下断言及其特性，以及时态逻辑是如何适合检查的。然后，我们将研究用于处理时态逻辑断言的工具。

断言及其特性

除了类型检查和单元测试外，断言还提供了一种确定各种特性是否在程序中得到维护的极好方法。

让我们快速浏览三种类型常见的断言特性（虽然是常见的，但它们没有提供我们所需的完整范围），将它们与可以用传统断言语言表示的程序特性的类型进行比较，并检查多线程上下文所必需的，但不可能表示成常规断言的断言特性。我们还将提供一些代码示例。

常见的断言特性

传统上，断言特性分成下面三种类型：

代码块执行之前特性所持有的条件前断言。

代码块执行之后特性所持有的条件后断言。

代码块执行之前和 之后特性所持有的不变断言。

与这些典型形式的断言一样有用，它们不太会有我们希望能在程序中持有的所有特性范围。让我们看一下典型的用断言表示的程序特性。

可表示为断言的程序特性

这只是可以用传统断言语言表示的程序特性类型的简短列表 ― 所有程序员都希望在代码中包含的特性：

确保任何一次性特性都仅生成一次

断言文档决不被未授权的代理程序访问

断言向每个线程提供运行机会

断言系统将决不会使其本身陷入死锁

安全性协议使用一次性特性（使用过一次的数字）生成器来确保事务未被用过。作为安全性中的简单概念，确保一旦生成特殊一次性特性，就不再生成它，这一点很重要。另一个重要的安全性断言是安全文档决不被未授权的代理程序访问。

在多线程代码中，我们希望断言每个线程最终都会有运行机会。我们还希望确保系统决不会使其本身陷入 死锁状态（即在两个或多个线程可以继续处理之前，它们正在彼此等待提供资源）。

诊断Java代码: Java编程中的断言和时态逻辑(2)

基本的非常规断言特性

下面是我们希望获得的（通常想要在多线程代码环境中获得的）两种非常有用的特性类型，不可能仅用常规断言来表示它们：

安全断言

生存断言

安全断言声明某些不合需要的系统状态将决不在任何环境下起作用。生存断言声明保证最终发生某些事件 ― 例如，给定的线程将最终被唤醒，而不是永远休眠。

时态逻辑可以帮助产生这些断言。

时态逻辑出现在何处

这样的断言超出普通断言语言的表示，但可以用形式体系和工具来表示这种语句。我们将这种形式体系称为 时态逻辑。

已定义的时态逻辑

时态逻辑是一种 模态逻辑，用于推理随时间而更改的特性。

请始终记住，有两种常规的时态逻辑：

把未来当作为事件的线性序列的模型

把未来当作为具有各种可能性的树型分叉的模型

在本文中，我们将只考虑把未来当作为事件的线性序列模型的时态逻辑。（“分叉树”逻辑非常酷，但它在计算上很难处理。）

通常，时态逻辑构建于一组更简单的原子（小单元）命题之上，如传统程序断言。于是，各种模态操作符都可以应用于这些原子断言以生成更

凌众科技专业提供服务器租用、服务器托管、企业邮局、虚拟主机等服务，公司网站：http://www.lingzhong.cn 为了给广大客户了解更多的技术信息，本技术文章收集来源于网络,凌众科技尊重文章作者的版权，如果有涉及你的版权有必要删除你的文章，请和我们联系。以上信息与文章正文是不可分割的一部分,如果您要转载本文章,请保留以上信息，谢谢!