[Checkers] Type Declaration Qualifiers

Mahmood Ali mahmood at MIT.EDU
Sat Aug 23 23:51:45 EDT 2008


It seems to me that the Interning type system differ from the  
immutability (IGJ and Javari) type systems in their use of annotations  
on type declaration.

For a given type declaration 'class @Interned Foo { ... }', the  
Interning checker assumes that 'Foo' and '@Interned Foo' are  
equivalent.  In other words, every use of Foo is actually '@Interned  

In IGJ (and Javari), for a declaration like 'class @Mutable Foo  
{ ... }', the IGJ checker assumes that the use needs to be a supertype  
of '@Mutable Foo'.  In other words, every use of 'Foo' needs to be of  
type '@Mutable Foo' or '@ReadOnly Foo'.  The old syntax of IGJ permits  
both uses by declaring Foo as 'class Foo<I extends Mutable>  
{ ... }' (cannot have readonly I) or 'class Foo<I super Mutable>  
{...}' (either readonly or mutable not immutable).  Javari operates  
like this too, but without immutable, so it's a bit less relevant there.

Any suggestions to clarify this difference?  Change the way we think  
about it in IGJ and Javari?  How should one express that a type cannot  
be Immutable?


More information about the checkers mailing list