Re: is Java getting close to Ada strong type checking with this tool?

[Tucker Taft <stt@avercom.net>]

The key difference is that programmers can't communicate
as much in Java as they can in Ada.  For example, all arrays
in Java are indexed by integers 0..length-1.  There are many
applications where this is not the natural index type for the
array.  Arrays are essentially like functions, and the index
type should be strongly typed, just like the parameters to a function.
Not all functions are presumed to take an integer parameter
ranging from 0..N-1!

Perhaps even more glaringly is that Java doesn't have enumeration
types, nor any user-defined scalar types (not even user-defined names
for the predefined scalar types).  That means that a parameter type is
often simply "int" when in fact the only legal values are much more
restricted, and correspond roughly to an enumeration.  There really
is no reasonable excuse for having omitted enumeration types from
Java (I have read the "official" rationale about lack of extensibility
and it is extremely weak in my view).

Unfortunately, there is no way for an enhanced static checker to
overcome some of these limitations.  There simply isn't enough
information.

On the other hand, I am a very big fan of enhanced static checking,
and I think it should be an important area of focus for programming
language research.

-Tucker Taft  stt@avercom.net

"peteclose@-" wrote:

> http://research.compaq.com/SRC/esc/
>
> "The Compaq Extended Static Checker for Java (ESC/Java), developed at the Compaq
> Systems Research Center (SRC), is a programming tool for finding errors in Java
> programs.  ESC/Java detects, at compile time, common programming errors that
> ordinarily are not detected until run time, and sometimes not even then; for
> example, null dereference errors, array bounds errors, type cast errors, and
> race conditions.
>
> ESC/Java uses program verification technology, but feels to a programmer more
> like a type checker.  By using an underlying automatic theorem prover, ESC/Java
> is more semantically thorough than decidable static analysis techniques.  At the
> same time, because it tries to detect certain kinds of errors only, and not
> prove the program's correctness, the technique is more automatic than full
> functional program verification. "