[Checkers] Need for multiple immutability parameters

Michael Ernst mernst at csail.mit.edu
Mon Jun 9 15:15:04 EDT 2008

Mahmood and others-

The Checker Framework paper says:

  In just two cases, the programmer would have liked multiple immutability
  parameters for an object.  The return value of \<Map.keySet> allows removal
  but disallows insertion.  The return value of \<Arrays.asList> is a mutable
  list with a fixed size; it allows changing elements but not insertion nor

I understand the second example (Arrays.asList).  Could you please explain
the first one (Map.keySet)?  I don't see how two parameters could
separately control removal and insertion in IGJ.



More information about the checkers mailing list