\set<Object>

[davidcok]

The type of `\lockset' and the type of the set comprehension expression are both sets of Objects. But we do not have such a type defined in the standard as yet. Likely we will in the future, along with other such types. (I need it now at least to write the RMv2 sections on those expressions). Maybe it is time to define it now.

I envision the following.

• a built-in primitive (value-based) type \set<> or alternatively org.jmlspecs.lang.set<> (which? both?)
• with one type parameter (just reference types or JML built-in types as well?)
• equality of elements using ==
• a constructor that creates such a set, e.g. \set<T>(o,oo,ooo,...), for type parameter T (perhaps with type inference for T so one can write a singleton set as \set(o))
• \set<T>() is the empty set
• operations set equality and inequality: ==, !=
• operations + (union), - (difference), * intersection (\disjoint ?)
• • subset, subset or equal: < <=
• operator \in for membership (using == on reference objects)
• implicit iteration with for (T o: set-value) {} is permitted
• quantification with \in (e.g. \forall T t; t \in set-value; ...
• has a .size() member and possibly a .stream() member
• as this is a value type, assignment is (conceptually) by copying. Thus set<T> is a subtype of set<U> iff Tis a subtype of U

By the way, would we be better to choose | and & for union and intersection?

Eventually, I expect also \map, \seq (variable length), \array (fixed length), maybe \multiset

[leavens]

• I like the idea of a built-in primitive (value-based) type instead of an actual Java object type (although the RAC might need the latter).
• We should only allow reference types.
• Equality using == is good for object identity.
• The constructor to create such a set is a good idea.
• The constructor to create an empty set is also good.
• If we compare value types uniformly using == and != for equality, then those are fine. But these would need to be implemented in RAC using .equals.
• Using +, -, and * for union, difference, and intersection, and < and <= for proper subset and subset are also good.
• Using \in for membership based on == is sensible.
• I don't see how a value type would be used in Java code to do iteration, but it could be used in quantifiers.
• .size() is fine, but I don't see the use of .stream()
• The subtyping rule given is fine (since there is no mutation).

[davidcok]

stream() is used in Java to convert collections to streams, for functional programming. If you do functional programming in Java you use a lot of streams and filters etc. on them. Having stream on \set removes to need to implement other syntax for applying lambda functions to them. That also lets you act on \sets (and collections) in specifications because you don't need statements. E.g. writing c.stream().anyMatch(o->p(o))

By org.jmlspecs.lang.set<> I still meant a primitive, value-based built-in type. But perhaps the distinction is clearer with the backslash. Of course, RAC will need some actual Java class to implement the value based \set, just as it does for other JML types.

As for only allowing reference types, I expect users will want (as will I), e.g. \set of \bigint or \set of \real or even \set of \set of T. I'm OK with disallowing \set of int or \set of short.

You would not use a value type in Java code, but you might use a Java for statement iterating over a \set in a model program or a model method

[mattulbrich]

I pretty much agree with the proposal. I have longed for this extension for a while. (It also fits neatly into the existing infrastructure in KeY.)

I also think that the type argument should be covariant.

.stream() would not have top priority for us and I would assume that we would leave it unimplemented at first.

.size() is problematic since this implies that all sets are finite. It might be sensible to have the set of even \bigints e.g. That would not be possible. I do not necessarily advertise the concept, but Dafny has two types set and iset with the latter allowing infinite sets.

\seq is implemented in KeY, so we do have some experience there to share. \map is implemented too, but has been used rarely.

[davidcok]

In all my specification I have not needed an infinite set -- have you in KeY, other than examples created to demonstrate the concept?

I'm happy to have \set be just finite sets, and worry about infinite sets later.

[wadoon]

a built-in primitive (value-based) type \set<> or alternatively org.jmlspecs.lang.set<> (which? both?)

I see logical types, like \set, as primitive values. They should not be treated like Java classes to avoid complexities. Especially, they should be immutable.

equality of elements using == operator \in for membership (using == on reference objects)

I would not always go for ==, only if the type is generated in the sense of CASL. In general, it depends on the types. Free generated data types requires a predicate for equality. For generated data types (not free), their equality follows from the term structure. Note, that there is a third option between == (symbolical equivalence) and .equals (equivalence by a Java method)---a defined logical predicate.

In general, I would suggest we build our data types on top of an established ADT definition. Especially, logical types, \set etc., does not need to work like the corresponding Java types (with all their quirks).

operations + (union), - (difference), * intersection (\disjoint ?) I current implemented operating overloading in KeY, and I used

• + and | for union
• - for difference
• & for intersection
• a^b could be (a|b)-(a&b)
• a<b is subset and a<=b is subseteq

has a .size() member and possibly a .stream() member

I would avoid using methods on the logical type in favor for a functional style.

Thus set is a subtype of set iff T is a subtype of U

[wadoon]

@davidcok

In all my specification I have not needed an infinite set -- have you in KeY, other than examples created to demonstrate the concept?

Here is an example for \map

We coupled \map to a Java interface, and an implementation of this interface. This gave us nice mathematical types for the specification and verification in the caller class.

[davidcok]

I likely was too terse. By == and != for any primitive \set type I mean a mathematical (structural) equality, not anything imagined from Java. Two \sets are equal if they contain the same (i.e. ==) members. The same would be true of a recursive datatype

[leavens]

I am fine with using == and != to mean mathematical equality of value types (both for sets and in general).

It was David Cok that made the remark about infinite sets (not me), but I agree that it makes sense to support infinite values for specification purposes (e.g., the set of all primes can be useful), but we need to be careful how we specify them to allow for runtime assertion checking. I see the point that Mattias is making about .size() not being well-defined for infinite sets, so perhaps that needs a precondition.

In general, I would prefer the method-like notation or operators (+, -, *) for operations on such mathematical values.