[Checkers] feedback on JavaOne talk

[Michael Ernst]

Brent-

Thanks for your interest in pluggable type-checking.  It sounds like you
and I have similar interests in using tools to improve software quality.
No one approach is a panacea, but it can help a lot!

> From just the JavaOne slides, I am actually finding it difficult to get an
> accurate picture of this new technology.  Do you have a more formal paper or
> website that gives more details?

Yes, talk slides tend to be telegraphic and not so useful after the fact.
You also missed the demos where much of the information was conveyed.  You
can see a video of a dry run at http://www.vimeo.com/4368251 .

More documentation including tool manuals and academic papers appears at
the website http://pag.csail.mit.edu/jsr308/.  It already answers some but
not all of your questions.  (I don't mind replying, but you could have
saved yourself some effort and avoided the delay!)

> Is this annotation stuff for sure going into jdk 7?

It's as certain as such things can be.  For example, this weekend Sun
integrated our code into its main OpenJDK Mercurial repository.

> Here is one practical example of my confusion.  On p. 5/29 of your talk, you
> mention immutable Dates.  ...  can you use @Immutable
> to effectively make a custom Date type that cannot be mutated?

Yes, that is exactly what slide 5 is showing.  You don't have to write any
more code than is shown on the slide.

> Does the
> effect only work with Java code that is compiled with the same type checker? 

Yes.  And I agree it is unfortunate.  But is no such thing as an absolute
guarantee in Java:  you can already use reflection to change the value of a
String object, for example.  (Java's flexibility comes at a price.)

> ... because
> Date is potentially mutable, there are all kinds of encapsulation issues
> here.  You could take the approach of always cloning incoming and outgoing
> Dates to ensure no tampering, but that lowers performance which is the whole
> point of using caching in the first place.  The approach that I ended up
> taking was to use a Date subclass which throws UnsupportedOperationException
> whenever a mutating method is called.

We've used our checkers to find representation exposure errors (that would
permit tampering), and to guarantee that they don't happen.  You can use
the checkers either to verify that the copying is correct, or to verify
that sharing without copying is safe.  The latter does require you to run
the checker on client code.  Best of all, the guarantee is a static one
rather than causing a crash at some unspecified point in the future.

> Here is another question: can you concatenate a bunch of type checks together?
>   As in, instead of something verbose like
>     javac -processor NullnessChecker  -processor ImmutableChecker -processor
> ...
> can you do
>     javac -processor MyFaveCheckers
> where MyFaveCheckers has been configured to do all the checks that you want?

Not at the moment.  We plan to support that in version 0.9.5 of the Checker
Framework (scheduled for July).  In the meanwhile, you can define a shell
alias or put it in an ant/make build file.

> Finally, how does your approach compare with JML?

JML is more ambitious.  A programmer can write a JML specification that
describes arbitrary facts about program behavior.  Then, the programmer can
use formal reasoning or a theorem-proving tool to verify that the code
meets the specification.

The JML toolset is relatively immature.  For instance, if your code uses
generics or other features of Java 5, then you cannot use JML.

Our pluggable type-checkers are aimed at being practical, which of
necessity means that they attack a limited set of problems.

> I am sure that your technology must be extensible so that people can write
> their own checkers.

Yes.  The documentation at the above website (& included in the download)
describes how.  The most relevant section is
http://groups.csail.mit.edu/pag/jsr308/current/checkers-manual.html#writing-a-checker

> 1) tons of numeric checks: is a byte/short/int/long/float/double positive/
> negative/notNegative/notPositive?
>     is a float/double not NaN or infinite?
> 
> 2) Strings: the usual check for me is not only is the String not null, but it
> also must be not empty and must not be all whitespace
> 
> 3) tons of other type specific checks (e.g. that a File arg is not only
> non-null, but that it exists in the file system and that it is either a normal
> file say).

The nullness checker already appears in our distribution.  You can write
the others yourself -- with more effort the more elaborate you want the
checks to be, for instance in how many different expressions are statically
determined to be positive.  The problem is undecidable in its full
generality.

> My current solution for all the general checks that I want to do is a custom
> class of mine called Check. ...  The major
> advantage of a library approach like this is that it always works regardless
> of what compiler is used and what client uses it, since the checks are
> embedded in the code.  But it has many weaknesses too:
> 
> a) it imposes a (usually small) runtime execution overhead
> 
> b) I suspect that other static analysis tools would find it harder to work
> with
> 
> c) it does not lead to any automatic javadoc generation of contracts (does
> your approach?)

In my view, despite its limitations, use of such a class marks you as a
careful and thoughtful programmer who cares about correctness.  And the
benefit of working regardless of the compiler and the silent is a big one.
I would add a fourth limitation to your list:

d) you only learn about a bug at run time -- during testing if you are
lucky, in the field if you are not.

Of course, a run time exception about a broken contract is much better than
a silent error, or a confusing exception later in the execution.  But
static checking is ever better, when practical.  Pluggable type-checking
makes it practical in more situations.  That includes some but not all of
the checks in your Check.java file.

To answer your question about Javadoc:  type annotations will appear in
Javadoc.  This support does not yet exist, but will be implemented for one
of our July releases.  (Unfortunately, the javadoc tool does not share any
code with the javac tool, so it requires some re-implementation.)

                    -Mike