From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: 103376,8a49f460b1976768 X-Google-Attributes: gid103376,public X-Google-ArrivalTime: 2001-08-17 02:54:44 PST Path: archiver1.google.com!newsfeed.google.com!newsfeed.stanford.edu!bloom-beacon.mit.edu!nycmny1-snh1.gtei.net!cambridge1-snf1.gtei.net!news.gtei.net!inmet!not-for-mail From: Tucker Taft Newsgroups: comp.lang.ada Subject: Re: is Java getting close to Ada strong type checking with this tool? Date: Fri, 17 Aug 2001 05:55:41 -0400 Organization: AverStar Message-ID: <3B7CEA1C.18D8AE77@avercom.net> References: <9lh8ql05og@drn.newsguy.com> NNTP-Posting-Host: 209.6.249.6 Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii; x-mac-type="54455854"; x-mac-creator="4D4F5353" Content-Transfer-Encoding: 7bit X-Trace: inmet2.burl.averstar.com 998042053 23194 209.6.249.6 (17 Aug 2001 09:54:13 GMT) X-Complaints-To: usenet@inmet2.burl.averstar.com NNTP-Posting-Date: 17 Aug 2001 09:54:13 GMT To: "peteclose@-" X-Mailer: Mozilla 4.75C-CCK-MCD {C-UDP; EBM-APPLE} (Macintosh; U; PPC) X-Accept-Language: en Xref: archiver1.google.com comp.lang.ada:12038 Date: 2001-08-17T09:54:13+00:00 List-Id: 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. "