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

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

[peteclose]

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. "

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

[Tucker Taft]

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. "

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

[Warren W. Gay VE3WWG]

Tucker Taft wrote:
> 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.

It was also pointed out in a paper I recently read, that all Java 
methods are dynamic (virtual). This also eliminates some compile 
time (static) checking that otherwise could have been performed.
-- 
Warren W. Gay VE3WWG
http://members.home.net/ve3wwg