Re: Verifying a compiler

wlohmann@informatik.uni-rostock.de (Wolfgang Lohmann)
30 Jun 2000 00:59:42 -0400

          From comp.compilers

Related articles
[2 earlier articles]
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: wlohmann@informatik.uni-rostock.de (Wolfgang Lohmann)
Newsgroups: comp.compilers
Date: 30 Jun 2000 00:59:42 -0400
Organization: University of Rostock
References: 00-06-056 00-06-081 00-06-088 00-06-099
Keywords: testing

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


Post a followup to this message

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