Re: Verifying a compiler

Robert A Duff (world!bobduff@uunet.uu.net) wrote:


: Hmm. The proponents of "verification" are fond of pointing this out
: (that testing doesn't prove the absense of errors). What they often
: forget to mention is that verification is *also* not a proof of
: absense of errors -- the program still might not do what we want it
: to. In fact, there is no known technique for being 100.0% certain of
: the absense of errors in a computer program, and I suspect there never
: will be.


Of course, verification can only prove absence of errors with respect
to the specification, which might itself contain errors. Errors
contained in the specification by mistake have to be assumed to be
correct program behaviour for the verification process, which is of
course not what we want.


: Sorry to get up on a High Horse there. ;-) I just think we should use
: whatever techniques are available -- writing formal specs, proving
: programs with respect to formal specs, testing, reviews, etc. We


I totally agree.


: shouldn't think that formal proofs are somehow above and beyond the
: more mundane things like "validation suites". Formal specs can have
: bugs, too.


Yes. And even verification proofs can contain errors ;-). One could
argue those proofs to be done automatically, but even those programs
can contain bugs... and sooner or later we might arrive at
philosophical considerations about truth. ;-)


I did not want to make any proposition, whether one of these methods
are better or worse. Just to make clear the distinction.


Regards, Wolf

Return to the comp.compilers page.
Search the comp.compilers archives again.