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
