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

固然传统断言可以增添对 Java 代码履行的查抄次数,但有很多查抄不能用它们来履行.补偿这一缺陷的办法是利用“时态逻辑”,它是一种用于描写程序状况若何随时间而更改的情势体系.在本文中,Eric Allen 将讨结论言,介绍时态逻辑并描写用于处理程序中时态逻辑断言的工具 （下一篇文章将查抄从前的错误情势和时态逻辑的利用程序）.

我们大家赞成对 Java 代码查抄得越多就越好,我们查抄了断言在测试新的和改良的编程中的用法.固然传统断言可以增添履行的查抄次数,但有很多查抄不能用它们来履行.

但是,有一个办法可以补偿断言留下的查抄缺口.那就是利用 时态逻辑.时态逻辑是用于描写程序状况若何随时间而更改的情势体系.让我们谈论一下断言及其特点,以及时态逻辑是若何合适查抄的.然后,我们将研究用于处理时态逻辑断言的工具.

断言及其特点

除了范例查抄和单元测试外,断言还供应了一种肯定各种特点能否在程序中得到保护的极好办法.

让我们快速浏览三种范例常见的断言特点（固然是常见的,但它们没有供应我们所需的完好范围）,将它们与可以用传统断言语言表示的程序特点的范例举行对比,并查抄多线程上下文所必须的,但不大概表示成通例断言的断言特点.我们还将供应一些代码示例.

常见的断言特点

传统上,断言特点分成下面三种范例:

代码块履行之前特点所持有的条件前断言.

代码块履行之后特点所持有的条件后断言.

代码块履行之前和 之后特点所持有的不变断言.

与这些典型情势的断言一样有效,它们不太会有我们但愿能在程序中持有的全部特点范围.让我们看一下典型的用断言表示的程序特点.

可表示为断言的程序特点

这只是可以用传统断言语言表示的程序特点范例的简短列表 ― 全部程序员都但愿在代码中包含的特点:

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

断言文档决不被未受权的代理程序拜候

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

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

安全性协议利用一次性特点（利用过一次的数字）生成器来确保事件未被用过.作为安全性中的简单概念,确保一旦生成特别一次性特点,就不再生成它,这一点很重要.另一个重要的安全性断言是安全文档决不被未受权的代理程序拜候.

在多线程代码中,我们但愿断言每个线程终究城市有运行机会.我们还但愿确保系统决不会使其本身陷入 死锁状况（即在两个或多个线程可以持续处理之前,它们正在彼此等候供应资源）.

　　以上是“诊断Java代码: Java编程中的断言和时态逻辑[Java编程]”的内容，如果你对以上该文章内容感兴趣，你可以看看七道奇为您推荐以下文章：