[JSR308] A little prototype experience...

[Arnout Engelen]

Neal Gafter wrote:

> On 5/5/07, *Perry James* <perry.dsrg at gmail.com 
> <mailto:perry.dsrg at gmail.com>> wrote:
>
>     Runtime checks should be emitted to throw a cast exception if null
>     is ever cast to non-null.  This would prevent a reference declared
>     to be non-null from ever becoming null
>
Alternatively, instead of emitting runtime checks, another way to go 
could be to allow/require the programmer to write code like:

void method1 (@Nullable String s) {
  if (s != null) {
    // the tool can infer statically that 's' is non-null at this point
    method2(s)
  }
}
void method2(@NonNull String s) { ... }

(of course, this /is/ a runtime check, but explicitly written down by 
the programmer instead of somehow generated)

> Unless it is a field (static or instance), in which case it starts out 
> as null no matter how it is declared.

Indeed there are a lot of interesting design choices when building a 
tool that leverages those annotations: if I remember correctly ESC/Java2 
and Spec# resolve this specific case by defining the semantics of their 
'nonnullability' of fields as something like 'only non-null assignments 
are allowed to this field, and we guarantee that something will have 
been assigned to it after any constructor for this object has finished'. 
Of course, this opens up an entire following (interesting) can of worms*.

I do think, however, that we're drifting off-topic here: the main point 
is that we can imagine (several different kinds of) useful tools being 
developed that make use of such annotations.


Arnout

* e.g. http://citeseer.ist.psu.edu/fahndrich03*declaring*.html


-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.csail.mit.edu/pipermail/jsr308/attachments/20070505/7c2cd8a1/attachment.htm