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

孤线程错误模式

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

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

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

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

臆想实现错误模式

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

例如，考虑我喜欢的接口示例： 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”最终将得到满足。此外，该技术也可用作出错诊断工具。

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

下一次，我们还将讨论更多用来改进您代码健壮性的方法。尤其是，我们将研究一些激动人心的新工具，以通过研究 JUnit 测试套件，这些新工具能够 自动地检测有意放置在您代码上的断言。

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