Validate basic set operations in JML

Question

How do I verify basic set operations such as intersect, union and difference in JML tool like OpenJML in which keywords like "\intersect \set_minus \set_union" are not supported?

The Java interfaces on which I want to do validation on looks like this:

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

Answer 1

You would have to find a functional description for these operations, as for all methods that don't have a direct correspondence in the JML-supported theories. The mathematical definition of the union of two sets, for example, is "the set of all objects that are members of either the one or the other set". I.e., the method union could be specified roughly as

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

and similarly for the other methods, assuming that there is a pure containsAll method available. Otherwise, you could use quantified expressions and a pure contains method. If you don't have such pure query methods, you would have to expose implementation details like an underlying field, which would make less sense for specifying an interface.

Does this clarify the problem for you?