[Checkers] Need for multiple immutability parameters

[Michael Ernst]

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
  removal.

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.

                     Thanks,

                    -Mike