验证JML中的基本集合操作

Question

如何在OpenJML这样的JML工具中验证基本的集合操作，比如intersect、union和difference，在这些工具中不支持"\intersect \set_minus \set_union“这样的关键字？

我想在其上进行验证的Java接口如下所示：

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

Answer 1

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

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

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

这是否为您澄清了问题？