At 3:55 PM -0700 7/10/04, Crispin Cowan wrote:

> However, I think I do see a gap between these extremes. You could have
> a formal specification that can be mechanically transformed into a
> *checker* program that verifies that a solution is correct, but cannot
> actually generate a correct solution.

Isn't that pretty much what the SPARK Inspector does ?
-- 
Larry Kilgallen


Reply via email to