验证 JML 中的基本集合操作答案

【问题标题】：Validate basic set operations in JML验证 JML 中的基本集合操作
【发布时间】：2019-10-03 17:41:25
【问题描述】：

在 JML 工具（如 OpenJML）中，不支持“\intersect \set_minus \set_union”等关键字的 JML 工具中，如何验证相交、联合和差异等基本集合操作？

我要对其进行验证的 Java 接口如下所示：

MySetInterface<S> intersect (MySetInterface<S> set)
MySetInterface<S> union (MySetInterface<S> set)
MySetInterface<S> difference (MySetInterface<S> set)

【问题讨论】：

标签： jml

【解决方案1】：

您必须找到这些操作的功能描述，就像在 JML 支持的理论中没有直接对应的所有方法一样。例如，两个集合并集的数学定义是“属于一个集合或另一个集合的所有对象的集合”。即，方法union可以大致指定为

/*@ public normal_behavior
  @ ensures this.containsAll(\old(this)) &&
  @         this.containsAll(\old(set)); */

对于其他方法也是如此，假设有一个纯containsAll 方法可用。否则，您可以使用量化表达式和纯 contains 方法。如果您没有这种纯查询方法，您将不得不像底层字段一样公开实现细节，这对于指定接口的意义不大。

这是否为您澄清了问题？

【讨论】：

你觉得@ ensures \result != null&&( \forall java.lang.Object e; ; \result .has(e) <==> this.has(e)||s2.has(e));eecs.ucf.edu/~leavens/JML-release/javadocs/org/jmlspecs/models/…
这也应该是一个明智的规范，因为你的接口有has 方法。当然，有不止一种方法可以做到这一点。为了判断哪个适用于您的特定情况，我必须查看您的完整源代码。可用的签名扩展了您的 Java 模型，没有您想象的那么多“通用”JML 运算符。