Crispin wrote: >> Proving that all array accesses are within bounds would seem to be Turing undecidable. Either you are not proving what you way you are proving, or your programs are not full Turing machines.
Proof: <insert diagonalization argument here :> Issue: Some people may regard diagonalized programs are a contrivance, and are only interested in correctness proofs for real programs (for some value of "real"). << The diagonalization argument shows quite nicely they you cannot write a program that, for any arbitrary input program, can say whether or not it has any array bounds problem. Which is why we haven't wasted our time trying to write such a program. Instead, we have produced a tool-supported method that lets us produce programs (including programs that solve complex problems) that are proven - subject to correctness of tool chain and processor - not to have array bounds problems (or many other sorts of problem), for arbitrary inputs. >> Crispin's rebuttal: Suppose I want to prove that your program checker does not have any illegal array references ... << I don't see what you are getting at here. Our proof engine is large and complex; but because of the way we have built it, the proofs that array indices are in bounds are not particularly difficult. Of course, you would need to use a different proof engine - or at least an independent proof checker - to produce reasonable "proof" of the correctness of the prover itself. Despite this, running the tool on itself does provide a lot of value, because proof failures have shown up a number of problems with the tool. Some of these problems would be very hard to detect by testing. The input space for a program of this type is so large so that testing can only exercise a small fraction of that space (actually, an infinitesimal fraction). David Crocker, Escher Technologies Ltd. Consultancy, contracting and tools for dependable software development www.eschertech.com
