Re: Generalizing Types as Provable Invariants

[Dan Weinreb <address@hidden>]

   Date: Fri, 31 May 2002 15:17:30 -0700
   From: Waldemar Horwat <waldemar@acm.org>
   Precedence: bulk

   A static type system can be thought of as a small framework for 
   proving invariants about a program -- in a type-safe language, if a 
   variable is typed as an integer then I know that I can't get a string 
   out of it.  The compiler knows it too and doesn't let me modify the 
   program to violate that assumption.

   How much work has been done on generalizing the notion of a static 
   type system into a more complete framework for proving interesting 
   invariants about a program?  In essence, I'd like the source code of 
   a program to consist of two interweaved parts:

   1.  The actual code of the program
   2.  Machine-checkable proofs of assertions about the program

You might be interested in "Extended Static Checking for Java".
Some of the people involved were:

David L. Detlefs, K. Rustan M. Leino, Greg Nelson, and James B. Saxe.

See

 http://research.compaq.com/SRC/esc/

-- Dan