[Checkers] Q about Mutability

[Mahmood Ali]

Greetings Mike,

I was wondering if the Javari paper address the following issue of  
"indirect mutable references" (I cannot find a better name).  This  
occurs when a readonly has a mutable alias to the receiver and then  
the method is used to modify the receiver.  Here is an example:

class MyClass {
   int field;

   @Mutable MyClass ref;

   // method that create a mutable reference to itself
   void mutableMethod() @Mutable {
     ref = this;
   }

   // modifies self through a mutable reference
   void readOnlyMethod() @ReadOnly {
     ref.d.time++;
   }
}

Personally, I don't find anything invalid here.  This behavior is  
equivalent to the user marking all fields @Mutable.  Type-systems  
cannot capture all of the user intent.

Regards,
Mahmood