I am new to this JSR305 group.
I am working on defect detection techniques applied to several
programming environments, espacialy on underflow, overflow, DIV/0,
null checking, return value checking etc..
As in restricted languages (ADA for ex), it would be valuable both for
tools and for developpers to be able to specify the authorized values
for functions, arguments, variables.
For example a simple instruction like * on floats leads to an overflow
when both factors are over sqrt(Float.MAX_VALUE).
As a matter of fact up to now, there is no way to detect
"automatically" that this declaration (in java.lang.StrictMath.java) :
public static native double cos(double a);
is in fact a value from -1.0 to 1.0, or NaN, mostly because native
declarations cannot be analyzed.
Adding annotation like for example public static native
@LegalIntervals {NaN;[-1.0, 1.0]} double cos(double a); would help
static analysis tools to detect that
float a;
float b = a*cos(a);
can never overflow
See
http://d.cr.free.fr/ for lots of tricky examples extracted from
Sun jdk6 packages.
This JSR305 sems to be closed now, may be for the future !!
Thanks for your attention.