0

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

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

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

1 回答 1

1

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

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

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

这是否为您澄清了问题？

于 2019-10-04T08:08:42.423 回答