诊断Java代码: 将时态逻辑用于错误模式 - 编程入门网

根据这个示例演示，类型检查器可以成为功能极强大的重构工具。但请考虑一下这种世界末日般的情景：新客户机程序员可能牢记着构造二叉树叶的旧的做法，并尝试通过构造 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.

诊断Java代码: 将时态逻辑用于错误模式(3)

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 Clean

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