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,start
X-Google-Attributes: gid103376,public
X-Google-ArrivalTime: 2001-08-16 13:22:15 PST
Path: 
 archiver1.google.com!newsfeed.google.com!newsfeed.stanford.edu!pln-w!spln!dex!extra.newsguy.com!newsp.newsguy.com!drn
From: peteclose@- <peteclose_member@newsguy.com>
Newsgroups: comp.lang.ada
Subject: is Java getting close to Ada strong type checking with this tool?
Date: 16 Aug 2001 13:01:25 -0700
Organization: Newsguy News Service [http://newsguy.com]
Message-ID: <9lh8ql05og@drn.newsguy.com>
NNTP-Posting-Host: p-385.newsdawg.com
X-Newsreader: Direct Read News v2.80
Xref: archiver1.google.com comp.lang.ada:12009
Date: 2001-08-16T13:01:25-07:00
List-Id: <comp.lang.ada>

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