[Checkers] Q about Mutability

Mahmood Ali MAHMOOD at MIT.EDU
Wed Nov 26 22:33:09 EST 2008

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 {

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.


More information about the checkers mailing list