Have immutable flag to allow for returning unmodifiable collections in java.util.Collections

[slyubomirsky]

This might require some careful thought. From what I understand, there are plans to rework OpenJML collections on a larger scale, so perhaps this is not so disruptive a change.

I wonder if a better (less coupled and cluttered) approach would be to simply have model classes implementing List, Collection, etc., that throw UnsupportedOperationExceptions and have the spec for Collections.unmodifiableList, unmodifiableSet, etc., return those.

[slyubomirsky]

Appears there are a number of issues with actually trying to use the unmodifiable collecitons I was hoping to specify: in HashMap, JML complains of a catastrophic internal error related to the quantifiers (which don't seem very different from those in other files) and also complains of contradictory invariants (i don't know which are in contradiction). Any advice for working around these or getting to the bottom of it?

[davidcok]

Steven,

1. Guard all declarations and uses of isImmutable with //-RAC@ (and any other model or ghost fields)
2. I would expect isImmutable to be a model field, not ghost.
3. Usual style is to list either ghost or model as the first modifier in declarations.

[slyubomirsky]

Done as suggested. I don't think I've missed any more places where there should be a -RAC but I'll give it another check soon

[RustanLeino]

The previous Map.jml file (and quite possibly also other collection types) had an invariant

public invariant content.owner == this;

This restricts a Map from being used by more than one client. For immutable maps, one would like to allow sharing. For this reason, the invariant ought to be updated to:

public invariant isImmutable || content.owner == this;

Rustan

[leavens]

Hi Rustan, and all, That sounds right to me; thanks, Rustan! Regards, Gary T. Leavens 437D Harris Center (Bldg. 116) Computer Science, University of Central Florida 4000 Central Florida Blvd., Orlando, FL 32816-2362 USA http://www.cs.ucf.edu/~leavens phone: +1-407-823-4758 [email protected]

…

On Thu, Sep 6, 2018 at 1:56 PM Rustan Leino ***@***.***> wrote: The previous Map.jml file (and quite possibly also other collection types) had an invariant public invariant content.owner == this; This restricts a Map from being used by more than one client. For immutable maps, one would like to allow sharing. For this reason, the invariant ought to be updated to: public invariant isImmutable || content.owner == this; Rustan — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#8 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/ALu2vTtSGmHeRNaabiyP-YZURQDwzaRHks5uYWHegaJpZM4WAv0R> .

[RustanLeino]

I'm sorry, I spoke too hastily when I mentioned the isImmutable disjunct of the Map class invariant above. That invariant says that the content is owned by the Map, not that the Map belongs to someone. I was confused by a bug in OpenJML, where my suggestion here happened to step around the bug. For more details, see OpenJML/OpenJML#651.