Code Analysis

I'm working on a plugin that does almost just this, using editor warning
inspections and annotations just like you said (as well as source code transformation
right before compilation, to enforce the preconditions at runtime). I'll
post on the plugins forum when it's usable, it might not be for a while because
I'm pretty busy. I do not plan to make the plugin automatically detect preconditions,
the user has to do it himself or herself.

-Keith

I've been thinking about what would really make me go 'Wow!' in an
IDE.
IDEA has made me go 'wow' several times with refactorings, live
templates, and smart completion.
Inspections are also amazing. I read somewhere that Dave Griffiths
is working on global inspections. I can't wait.
Here something I've been thinking of:

Code Analysis
IDEA could analyze methods for effects, side-effects, calculate
pre-conditions and post-conditions. It could use this information
to verify that pre- and post-conditions are not violated.
An example:

 { return p.x; }]]>

IDEA could detect that p cannot be null. This
piece of information
could be encoded using an annotation, like this:

 getX(@not_null Point p)
> { return p.x; }]]>

IDEA would of course provide the option to
automatically hide these
annotations.
IDEA could also calculate if parameters passed are modified,
e.g.:

 { p.x = 0; }]]>

The same thing should be done with return values.
Let's say I have
this code:

 Point getPoint();
> }
> class Test implements PointSource {
> Point getPoint()
> { return Moon.isFull ? new Point(10, 10) : null; }
> int getX(@not_null Point p)
> { return p.x; }
> void method(PointSource ps)
> {
> Point p = ps.getPoint();
> int x = getX(p);
> }
> }]]>

This would tell me that getX requires its parameter to be not
null, and p
may be null. This is fixed by annotating the getPoint call in the
PointSource
interface to not return null. This requirement is, of course,
inherited by the
implementation of getPoint in the Test class. That requirement will
generate
a warning since Test.getPoint may produce a null return value.
The updated and fixed code would look like this:

 PointSource {
> @not_null Point getPoint();
> }
> class Test implements PointSource {
> public static Point BAD_POINT = new Point(-1, -1);
> @not_null Point getPoint()
> { return Moon.isFull ? new Point(10, 10) : BAD_POINT; }
> int getX(@not_null Point p)
> { return p.x; }
> void method(PointSource ps)
> {
> Point p = ps.getPoint();
> int x = getX(p);
> }
> }]]>

This would make me go 'Wow!'
/Mikael

That sounds very interesting. I'm looking forward to it.

/Mikael