Re: Verifying a compiler

Robert A Duff <world!bobduff@uunet.uu.net>
27 Jun 2000 00:55:45 -0400

          From comp.compilers

Related articles
Verifying a compiler scarroll@csrd.uiuc.edu (Steven Carroll) (2000-06-14)
Re: Verifying a compiler mlross@jf.intel.com (2000-06-20)
Re: Verifying a compiler t.hutt@worldnet.att.net (Taylor Hutt) (2000-06-20)
Re: Verifying a compiler wlohmann@informatik.uni-rostock.de (2000-06-22)
Re: Verifying a compiler david@somers.lu (David Somers) (2000-06-22)
Re: Verifying a compiler echristo@cygnus.com (Eric Christopher) (2000-06-27)
Re: Verifying a compiler world!bobduff@uunet.uu.net (Robert A Duff) (2000-06-27)
Re: Verifying a compiler iainf@news.kororaa.com (Iain A F Fleming) (2000-06-30)
Re: Verifying a compiler wlohmann@informatik.uni-rostock.de (2000-06-30)
Re: Verifying a compiler joachim.dot.durchholz@halstenbach.com (Joachim Durchholz) (2000-07-04)
| List of all articles for this month |
From: Robert A Duff <world!bobduff@uunet.uu.net>
Newsgroups: comp.compilers
Date: 27 Jun 2000 00:55:45 -0400
Organization: The World Public Access UNIX, Brookline, MA
References: 00-06-056 00-06-081 00-06-088
Keywords: testing

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


Post a followup to this message

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