Generics

Lex Spoon lex at cc.gatech.edu
Mon Sep 29 14:47:39 UTC 2003


"Richard A. O'Keefe" <ok at cs.otago.ac.nz> wrote:
> ESC/Java (the Extended Static Checker for Java; there is also an earlier
> version for Modula-3) *can* solve the "these two integers must sum to
> less than 5 at all times" style of correlations.  ESC/Java is, and is
> intended to be, somewhere between a type checker and a program verifier.


Additionally, the functional languages guys do a LOT along these lines. 
Anyone interested in this should search for "proof carrying code".

Note, though, that these systems are rarely automatic.  The more you
want to know statically, the more, in general, the programmer must help
out.

-Lex



More information about the Squeak-dev mailing list