Bad precondition in java.util.HashSet.HashSet(Collection<? extends E> c)

[psybers]

I believe this spec is wrong:

Specs/specs/java/util/HashSet.jml

Line 11 in f34f232

//@ ensures size() == c.size();

Since the collection c can be of any type, it might have duplicates. The resulting set would thus have a smaller size.

Perhaps a spec of:

    //@   ensures c instanceof Set ==> (size() == c.size());
    //@   ensures !(c instanceof Set) ==> (size() <= c.size());