Re: using @inert with collection APIs

On Sep 26, 2008, at 18:10, Tyler Close wrote:
> On Fri, Sep 26, 2008 at 2:47 PM, Kevin Reid <[email protected]> wrote:
>> On Sep 24, 2008, at 16:45, Tyler Close wrote:
>>> 1. We were unable to use the standard iteration API, since it uses a
>>> mutable iterator object. So the following code would generate a
>>> verifier error:
>>>
>>>   Iterator<SomeMutable> i = someKeys.iterator();    // cannot hold
>>> return value in non-@inert variable
>>>
>>> and so would:
>>>
>>>   @inert Iterator<SomeMutable> i = someKeys.iterator();
>>>   i.next();    // cannot call non-@inert method on @inert reference.
>>
>> It seems to me that what you want to express here is
>>
>>  Iterator<@inert SomeMutable> i = someKeys.iterator();
>
> That's interesting, but not quite what is needed. We need to know that
> the iterator itself won't mutate the values in the map, not just that
> it won't let the caller mutate the returned values. For example, what
> if the Iterator.next() implementation was:
>
> T next() {
>    this.underlyingMap.get(0).sneakyModification();
>    T r = ...  // get next value.
>    return r;
> }

So let's say that you can only use the above declaration if the  
iterator class is audited to not do this -- i.e. to treat its  
parameter as inert, whether or not the caller does.

>> Whether something equivalent to this is possible in Java I don't  
>> know.
>
> Unfortunately, the syntax also doesn't support this expression.

How about something like @inert-in-type-parameter(0)  
Iterator<SomeMutable>?

-- 
Kevin Reid                            <http://homepage.mac.com/kpreid/>