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

时态逻辑使用三个（或四个，取决于模型）常见的模态操作符。

典型的模态操作符

通常，下列模态操作符可用于时态逻辑：

Always

Sometime

Until

Next （特殊情况）

当应用于断言时， Always 确保断言在整个程序执行的剩余部分继续保持。

从意义上说，操作符 Sometime 与 Always 是亲戚，但弱得多。当应用于断言时， Sometime 规定一定要在程序执行的今后时间内存在某些断言可以起作用的时间点。

Until 应用于两个断言，它规定一旦第一个断言停止作用，此后，第二个断言就必须保持有效。

当时间可以是由一系列不连续步骤（比如，程序执行期间）组成的模型时，您有时候会看到 Next 操作符被添加到这个著名的列表中。当 Next应用于断言时，它规定断言在“下一个”步骤中保持有效。当然，仅当我们将时间分割成不连续步骤时，这才有意义。

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

清单 1 显示了一些时态逻辑断言示例：

清单 1. 样本时态逻辑断言

Always x != 0 Sometime x == 0 {x == y} implies {Next {x == y + 1}} {x == y} Until {y == 0} {x == 0} implies {Next {Always {x != 0}}} // x is zero only once Sometime {! this.isInterrupted()} // this thread is not interrupted forever

下面是两个断言它们从不死锁的线程的示例断言。（注：布尔方法 isWaitingOn 用于检查一个线程是否被另一个线程执行的任务挂起。）

清单 2. 说明多线程的样本

Always {x.isWaitingOn(y) implies {! y.isWaitingOn(x)}}

可以扩展时态逻辑。

扩展语言

我们还可以扩展时态逻辑的语言以包括数据库中值集合的量词。例如，我们可以检查断言是否始终对表中的所有值保持有效或者至少对表中的一个值保持有效。

有了这种级别的表示，我们可以构成非常强大的安全和安全性断言。例如，考虑显式代理对象可以请求访问各种文档的环境。我们可以组成清除可以查看各种文档的代理的断言。

下列断言保证没有一个代理可以查看文档，直到他让明确可以有权这样做：

清单 3. 说明数据库安全性的样本

ForAll agents in AgentPool 　 {ForAll document in TopSecretDocumentPool 　　 {{! agent.canView(document)} Until {agent.hasClearanceFor(document)}}}

如何检查时态逻辑？

现在，您可能会提出异议：“喔！我可以 讲所有这些事情真是太棒了，但我无法检查我所讲的是否正确，那么问题在哪里呢?!”

对此我要说的是：有专门检查这些类型的断言的工具。在数字电路中，在构建芯片之前，先静态地验证这类断言。

在软件中，我们 静态检查这种断言的能力是微不足道的，但存在用于检查这些断言在程序的特殊运行（例如，单元测试的运行）期间是否保持有效的品质工具。这样的断言可以帮助您将单元测试提升到很高的程度；每个时态逻辑断言都可以与无数的传统断言对应（并且只是在传统断言完全可以用来表示断言的情况下）。

Time Rover Inc. 的 Temporal Rover 是一种用于处理 Java 程序中时态逻辑断言并根据断言生成有效 Java 代码的工具。（请参阅 参考资料。）该公司还提供用于数据库表的工具 DBRover。

Temporal Rover 包括所有时态操作符以及为讨论过去发生的事件而设计的其它操作符。DBRover 可以以数据库中值量化断言。不幸的是，这些工具不是免费的，但它们提供了 30 天的免费试用版本。

与 JUnit 中的断言相似，Temporal Rover/DBRover 断言为程序员提供了在断言失败时打印诊断消息的选项。实际上，Temporal Rover

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