Re: Verifying a compiler

wlohmann@informatik.uni-rostock.de (Wolfgang Lohmann) writes:


> Verification is, informally speaking, mathematically prooving of
> correctness with respect to a specification. Testing can not
> prove the absence of errors (exception : trivial cases), only
> their existence. Therefore, you are looking for a validation
> suite ;-).


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.


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
shouldn't think that formal proofs are somehow above and beyond the
more mundane things like "validation suites". Formal specs can have
bugs, too.


- Bob

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