[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: Generalizing Types as Provable Invariants
Date: Fri, 31 May 2002 15:17:30 -0700
From: Waldemar Horwat <firstname.lastname@example.org>
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.