[JSR308] Type refinement for immutability

[Michael Ernst]

James-

> Is there anyone that has had some practical experience with using type
> refinement to handle immutability?

The Checker Framework that is distributed at the JSR 308 website, contains
two checkers for immutability type qualifiers (that is, refinement types).
Here are the relevant sections of the manual:

  http://groups.csail.mit.edu/pag/jsr308/current/checkers-manual.html#igj-checker
  http://groups.csail.mit.edu/pag/jsr308/current/checkers-manual.html#javari-checker

Those manual sections cite publications about the type systems.  The
checkers have been run on programs of up to 100,000 lines of code.  Here
are direct links to the papers.

  http://www.cs.washington.edu/homes/mernst/pubs/immutability-generics-fse2007-abstract.html
  http://www.cs.washington.edu/homes/mernst/pubs/ref-immutability-oopsla2005-abstract.html
  http://www.cs.washington.edu/homes/mernst/pubs/ref-immutability-oopsla2004-abstract.html
  http://www.cs.washington.edu/homes/mernst/pubs/infer-refimmutability-ecoop2008-abstract.html

                    -Mike