Java开发网 - 诊断 Java 代码：将时态逻辑用于错误模式

Java开发网

您没有登录

» Java开发网 » 技术文章库

打印话题 寄给朋友 订阅主题

作者

诊断 Java 代码：将时态逻辑用于错误模式

palatum

CJSDN高级会员

发贴: 451
积分: 80

于 2002-12-03 17:58

诊断 Java 代码：将时态逻辑用于错误模式

用时态逻辑断言防止常见错误
级别：初级

Eric E. Allen（eallen@cs.rice.edu）
博士研究生，Java 编程语言小组，莱斯大学（Rice University）
2002 年 11 月

时态逻辑（temporal logic）是一种用来描述程序状态如何随时间而更改的形式体系。本文是 Eric Allen 关于时态逻辑和断言的第二篇专栏文章，他讨论了如何通过使用时态逻辑断言防止几种最常见的错误模式。请单击文章顶部或底部的讨论参与本文的论坛，与作者和其他读者分享您关于本文的想法。
尽管传统的断言可以增加对 Java 代码所作的检查次数，但仅用它们，还是有许多检查无法完成。处理这种情况的方法之一就是使用时态逻辑。请回忆上个月的文章“Assertions and temporal logic in Java programming”，时态逻辑有助于提供比程序中的方法更有力的断言，从而有助于增强用其它方式难以正式表达的不变量。

我们不必费力搜寻去发现有助于防止我们程序出错的许多有用的不变量。实际上，可以通过使用此类时态逻辑断言来加大我们消除一些最常见错误模式的力度。在本文中，我们将研究一些错误模式，使用时态逻辑能会对它们产生最积极的影响。我们将把下列错误模式用作示例：

悬挂复合（Dangling Composite）。当您的软件抛出空指针异常时这个错误发生，因为递归数据类型的错误表示，所以这是个难以诊断的问题。

破坏者数据（Saboteur Data）。这种错误在已存储的数据不能满足某些句法或语义约束时发生；此时软件会因为代码操纵的数据中的错误而不是编码中的错误而崩溃。

Split Cleaner。当资源的获取和释放按方法边界一分为二，允许某些控制流不释放它们本该释放的资源，其表现形式为泄漏或过早地释放它们时，这种错误发生。

孤线程（Orphaned Thread）。当主线程抛出异常而剩余线程继续运行，并等待更多输入到该队列时，这种错误发生；这种错误可能导致程序冻结。

臆想实现。当您“实现”了接口，但实际上没有满足其预期的语义时，这种错误发生。
悬挂复合错误模式
悬挂复合错误模式包括递归数据类型的错误表示、将一些类型的基本情况表示为空值而非单独的类。这样做会导致难以诊断的 NullPointerException。

例如，假定您创建了下列“讨厌的”数据类型来表示二叉树：

清单 1. 一些非常糟糕的树
public class Tree {
public int value;
public Tree left;
public Tree right;

// Leaves are represented as Trees
// with null branches.
public Tree(int _value) {
this.value = _value;
this.left = null;
this.right = null;
}

public Tree(int _value, Tree _left, Tree _right) {
this.value = _value;
this.left = _left;
this.right = _right;
}
}

大家注意，除了作为糟糕的示例，请不要将这个代码用于任何其它用途！

这段代码造成了悬挂复合。二叉树叶子被表示为左右分支都是空值的 Tree。如果我们尝试向下递归这样的树，可能很容易引发 NullPointerException。

防止这种错误模式的最佳方法是：将数据类型的表示重构为 Composite 类层次结构（请在参考资料一节参阅关于这个主题的文章）。假定您恰好已经完成了这样的重构，如下所示：

清单 2. 更好的、已重构的树
abstract class Tree {
public int value;

public Tree(int _value) {
this.value = _value;
}
}

class Leaf extends Tree {

private Leaf(int _value) {
super(_value);
}
}

class Branch extends Tree {
public Tree left;
public Tree right;

public Branch(int _value, Tree _left, Tree _right) {
super(_value);
this.left = _left;
this.right = _right;
}
}

您希望确保其余代码（或任何外部客户机代码）都不会再构造任何旧的悬挂复合：您如何做到这一点呢？

很容易：做一次彻底的编译。如果您试图构造 Tree 类的实例，就会得到编译器错误。而且因为 Tree 是抽象的，所以当您试图编译新程序时，来自类型检查器的错误将通知您每个应该重构的构造位置。此外，left 和 right 字段被移到 Branches 类这一事实意味着：Tree 类中每条设置这些字段的值的语句也都会引起类型检查错误。

根据这个示例演示，类型检查器可以成为功能极强大的重构工具。但请考虑一下这种世界末日般的情景：新客户机程序员可能牢记着构造二叉树叶的旧的做法，并尝试通过构造 Branch 类的新实例来构造新叶子，因此给左右分支都传递空值。那么，使用时态逻辑，您可以在该字段上设置“Always”断言，它将断言该字段永远不接收空值：

Always{left != null}
Always{right != null}

当然，我们也可以用在字段上放置类似的普通断言的方法重构代码。但是这个过程要麻烦得多。具体来说，我们必须使该字段成为私有的（private），添加一个 setter ，并把代码中设置该字段的地方重构为调用写方法（setter）（我们可以在执行这个操作时利用类型检查器，就象上个示例中一样）。然后，我们可以在该写方法（setter）上放一个普通断言，声明所设置的值不能为空。

因此，在本例中，您可以根本不用时态逻辑断言就能完成任务，但会困难得多。让我们研究一些其它的错误模式，对于这些模式时态逻辑能向我们提供了更大的好处。

破坏者数据错误模式
破坏者数据错误模式在已存储的数据不能满足某些句法或语义约束时发生。此类数据会长期休眠，然后在访问时被激发。

防止这种错误模式的最佳方法是：在将数据放置到长期存储器之前，对它执行足够的检查。但假定您维护一个具有多个客户机的数据库，其中有些客户机不受您控制，所有客户机都有写访问权。您如何防止插入不合适的数据呢？

保护措施的第一级是为所有数据库访问（以仲裁器 (Mediator) 形式）提供单个控制点。但是，您还是有可能不能防止恶意（或只是无心的）客户机突破您的抽象层并通过另外的路径输入数据。

有助于快速诊断此类问题的方法之一是在数据库上放置时态断言。这些时态断言可以将希望保存的句法和语义不变量声明为“Always”断言：

ForAll x in Employees . Always{Age >= 0}
ForAll x,y in Employees . Always{isMarried(x,y) implies isMarried{y,x}}
etc.

Split Cleaner 错误模式
Split Cleaner 错误模式资源的获取和释放按方法边界一分为二，允许某些控制流不释放它们本该释放的资源时发生。

处理这种错误模式的最佳方法是重构。但如果代码库很大并且写得很糟糕，就很难确保已经全面跟踪了所有可能的执行路径。

在那种情况下，Split Cleaner 错误模式会转换成另一种形式：我们将尝试多次释放资源，而不是一味地不释放资源。

我们可以做的、有助于把我们从这种可悲的重构尝试中解脱出来的事情是：在最初获取该资源的方法中放置一条时态断言，以达到这样的效果，如果资源已被释放，那么除非它再次被获取，否则不会被再次释放。

例如，考虑下列用于打开和关闭文件的糟糕得惊人代码。

import java.io.*;

class ReaderMaker {

String name;

public ReaderMaker(String _name) {
this.name = _name;
}

FileReader getReader() {
return new FileReader(this.name);
}
...
}

class Client1 {
...
void doSomeWork(ReaderMaker maker) {
FileReader reader = maker.getReader();
...
reader.close();
}
}

当我们完成了对 FileReaders 的使用时，谁负责关闭它？很明显是客户机。这是 Split Cleaner 的典型情况。当用不同的方法负责获得和释放资源这两种行为时，就很容易取得资源却永不释放。

首先，时态逻辑断言对于诊断此类错误也是有用的。例如，如果我们怀疑一个 Split Cleaner，那么，可以在获取资源的方法上放置一个断言：如果获取了资源，则最终要释放它。然后，如果程序执行没有满足断言而终止，将用错误消息通知我们。理想情况下，所有资源获取行为都将首先包括这个断言，因此一出现 Split Cleaner 就会尽快通知我们。

孤线程错误模式
孤线程错误模式在多线程程序中某些线程等待已终止的线程时发生。

时态逻辑可以有助于诊断此类错误。在每个放置了“wait”以等待其它线程应答的实例中，我们都可以插入一个断言以使等待最终得到满足。如果它永远得不到应答，当程序终止时，我们将得到一条说明情况的错误消息：

Always{wait() implies {Sometime{notify()}}}

臆想实现错误模式
时态逻辑断言最直接的应用是在接口上添加可执行文档，从而在一旦违反这些断言时就立即捕捉接口的臆想实现。

例如，考虑我喜欢的接口示例：Stack。我们可以向这个接口添加非常强有力的断言，以表达如下所示的意思：

// Once push(x) occurs, top() will return x until a push or a pop occurs.
Always{push(x) implies {{top() == x} until {push(y) || pop()}}

// If the stack is empty, there should be no pops until a push occurs.
Always{isEmpty() implies {{! pop()} until {push(x)}}}

// (if we have a length operation) If the length is n, and a push occurs,
// then next step, the length will be n+1.
Always{{length == n && push(x)} implies {Next{length == n + 1}}}

您明白其意义了吧。

接口中的时态逻辑断言不但比散文（prose）精确得多，而且，实际上在运行时它们是强制执行的（如果我们运行的代码包含断言检查手段的话）。

把松散的思路串起来
正如我们在本文和前一篇专栏文章中所看到的，因为每个时态逻辑断言可以对应多个传统断言，所以时态逻辑断言可以辅助您更有力地进行单元测试，因此它们的功能是很强大的。

在本文中，我们展示了如何用时态逻辑断言对付下列错误模式：

悬挂复合。在字段上使用用比较简单的“Always”断言来声明该字段永远不使用空值。

破坏者数据。在数据库上使用“Always”断言来声明希望在数据库中保存的句法和语义不变量。

Split Cleaner。在最初获取资源的方法中使用时态断言来声明：如果该资源已被释放，那么直到它再次被获取，才会被再次释放。此处也可以使用时态断言作为出错诊断工具。

孤线程。使用时态断言来声明：无论何处，只要在线程上放置了等待其它线程应答的“wait”，则“wait”最终将得到满足。此外，该技术也可用作出错诊断工具。

臆想实现。将时态断言用作接口上附加的可执行文档，以便在违反断言时立即捕捉接口的臆想实现。

话题树型展开

人气	标题	作者	字数	发贴时间
8785	诊断 Java 代码：将时态逻辑用于错误模式	palatum	5598	2002-12-03 17:58

已读帖子

新的帖子

被删除的帖子