Google Groups Home Help | Sign in
Reasons why you don't prove your programs are correct
There are currently too many topics in this group that display first. To make this topic appear first, remove this option from another topic.
There was an error processing your request. Please try again.
flag
  Messages 1 - 25 of 64 - Collapse all   Newer >
The group you are posting to is a Usenet group. Messages posted to this group will make your email address visible to anyone on the Internet.
Your reply message has not been sent.
Your post was successful
"Steve" Stevenson  
View profile
 More options Jan 8 1990, 9:31 am
Newsgroups: sci.philosophy.tech, sci.physics, talk.philosophy.misc, comp.software-eng
From: st...@hubcap.clemson.edu ("Steve" Stevenson)
Date: 8 Jan 90 14:31:08 GMT
Local: Mon, Jan 8 1990 9:31 am
Subject: Reasons why you don't prove your programs are correct

I'm trying to discover the real reason why people do not prove their programs
are correct. I would like to collect those reasons --- even those snappy
one liners that we all use as excuses.

Please forward your comments ( short flames ok) to me by E-mail.  I'll post
the replies if there is sufficient interest. Thanks.

Steve (really "D. E.") Stevenson           st...@hubcap.clemson.edu
Department of Computer Science,            (803)656-5880.mabell
Clemson University, Clemson, SC 29634-1906
--
Steve (really "D. E.") Stevenson           st...@hubcap.clemson.edu
Department of Computer Science,            (803)656-5880.mabell
Clemson University, Clemson, SC 29634-1906


    Reply to author    Forward  
You must Sign in before you can post messages.
To post a message you must first join this group.
Please update your nickname on the subscription settings page before posting.
You do not have the permission required to post.
Dave Decot  
View profile
 More options Jan 18 1990, 4:30 pm
Newsgroups: comp.software-eng
From: de...@hpisod2.HP.COM (Dave Decot)
Date: 18 Jan 90 21:30:11 GMT
Local: Thurs, Jan 18 1990 4:30 pm
Subject: Re: Reasons why you don't prove your programs are correct
Here's three of my reasons why programs aren't proved correct.
(Sorry I was unable to reach you by email.)

Theorem provers are too slow and expensive.

Programmers are too lazy to write assertions and invariants, especially
for complex code (which if they weren't lazy wouldn't be so complex).

Efficient compilers for programming languages that support automatic
verification are not widely available.

Dave


    Reply to author    Forward  
You must Sign in before you can post messages.
To post a message you must first join this group.
Please update your nickname on the subscription settings page before posting.
You do not have the permission required to post.
Flame Bait  
View profile
 More options Jan 20 1990, 6:30 am
Newsgroups: comp.software-eng
From: jos...@athertn.Atherton.COM (Flame Bait)
Date: 19 Jan 90 18:16:55 GMT
Local: Fri, Jan 19 1990 1:16 pm
Subject: Re: Reasons why you don't prove your programs are correct

In article <16520...@hpisod2.HP.COM> de...@hpisod2.HP.COM (Dave Decot) writes:
>Theorem provers are too slow and expensive.

Theorem provers might be slow and expensive, but program provers are
not available at any seed or price.  Indeed it is doubtful that such
programs can be written at all.  (See the CACM article entitled "
Program Verification: The Very Idea".  I can no longer remember the
exact CACM it was in, sorry.  My best guess would be Sept. 1986 or 1989.)

>Programmers are too lazy to write assertions and invariants, especially
>for complex code (which if they weren't lazy wouldn't be so complex).

As was discussed in another new group (comp.ai or comp.object), assertions
have little to do with proving a program correct.  The best they can
do is prove that the assertions are met.  While this is a good thing,
it does not PROVE anything.  How do you prove that the assertions assert
anything useful?

Blaming the programmers is a cheap shot.  If that were the only problem,
then some programs would be proven correct, the fact almost no commercial
or military programs have ever been proven correct suggests that the
technology is not available.  Remeber that assertions are not nearly
enough.

Dave Decot makes it sound like there is a choice.  You can choose to
prove your program correct, or not prove it correct, but this is false.
With current technology you can not prove a (real-world) program correct.

Joshua Levy
--------                Quote: "If you haven't ported your program, it's not
Addresses:                      a portable program.  No exceptions."  
jos...@atherton.com          
{decwrl|sun|hpda}!athertn!joshua    work:(408)734-9822    home:(415)968-3718


    Reply to author    Forward  
You must Sign in before you can post messages.
To post a message you must first join this group.
Please update your nickname on the subscription settings page before posting.
You do not have the permission required to post.
Geoff Clemm  
View profile
 More options Jan 20 1990, 11:47 am
Newsgroups: comp.software-eng
From: ge...@tom.harvard.edu (Geoff Clemm)
Date: 20 Jan 90 04:30:40 GMT
Local: Fri, Jan 19 1990 11:30 pm
Subject: Re: Reasons why you don't prove your programs are correct

In article <16...@joshua.athertn.Atherton.COM> jos...@athertn.Atherton.COM (Flame Bait) writes:

   Theorem provers might be slow and expensive, but program provers are
   not available at any seed or price.  Indeed it is doubtful that such
   programs can be written at all.  (See the CACM article entitled "
   Program Verification: The Very Idea".  I can no longer remember the
   exact CACM it was in, sorry.  My best guess would be Sept. 1986 or 1989.)

This article is only of interest because of the resulting CACM Flame-Fest
that ensued.  The article itself merely makes the obvious statement that
a program-proof is wrt some set of axioms about the behaviour of the hardware
that the program runs on.  The article's author then concludes that you "cannot
prove programs correct" because the hardware may not satisfy the axioms.
Personally, I would be very happy with a program that would only malfunction
if the hardware adds 1+1 and comes up with 3.

What the author (and apparently the poster) fails to realize is that the
purpose of a program proof in the real world is to increase your confidence
that the program will do what you want it to do.  Sure, some academics with
axes to grind (and grants to obtain, and tenure to achieve) indulge in some
faulty advertising, but anyone seriously working in the area is aware that
a proven program can still fail to do what the user wants it to do.

Of course the hardware axioms could
be unsatisfied, the proof itself could be faulty, a faulty compiler could be
used, etc., but that does not eliminate the fact that a program proof
increases your confidence that the program does what you want it to do.

   As was discussed in another new group (comp.ai or comp.object), assertions
   have little to do with proving a program correct.  The best they can
   do is prove that the assertions are met.  While this is a good thing,
   it does not PROVE anything.  How do you prove that the assertions assert
   anything useful?

This comment applies to any technique that can be used to increase your
confidence in a program, and is totally pointless.  To repeat, the point of
a program proof is to increase your confidence that the program does what
you want.  Neither it, nor any other technique will guarantee it.  Sometimes
testing is better, sometimes code walkthroughs, usually a combination of
all the various techniques is best.

Geoff Clemm


    Reply to author    Forward  
You must Sign in before you can post messages.
To post a message you must first join this group.
Please update your nickname on the subscription settings page before posting.
You do not have the permission required to post.
Charlie Martin  
View profile
 More options Jan 21 1990, 10:47 am
Newsgroups: comp.software-eng
From: c...@romeo.cs.duke.edu (Charlie Martin)
Date: 20 Jan 90 20:11:42 GMT
Local: Sat, Jan 20 1990 3:11 pm
Subject: Re: Reasons why you don't prove your programs are correct
I resisted answering this for a long time, except by mail, but now I
just can't resist any longer.

I can't answer the question "why I don't prove my programs correct"
because I do.  All the time.  As a matter of course.  Almost without
exception.

As a practical matter, the issues Fetzer raised in his diatribe passing
falsely as a technical article can be largely ignored, both from the
standpoint of engineering and mathematically.  You simply must know
where to draw the line.  You assert a semantics for whatever you can't
prove, assume that as part of your theorey, and proceed.  when you
realize your code, you firewall the parts which are assumed but unproven
with assertions that are executed at run time, and ensure that the
semantics you assumed are the semantics you got.  Thus as a matter of
engineering, Fetzer's Dilemma -- which we might state as "how can
mathematics which is deductive apply to the real world, about which we
can only gather data and validate hypotheses?" -- can be (almost)
ignored.  All the issues raised are issues that apply equally to other
pure vs. applied mathematics dichotomies; all must be handled by the
(implicit or explicit) assumtion that our physical models are a
sufficiently good approximation of the "unspeakable" real world.

But, in fact, these issues had been examined at some length in the
formal methods community.  Had Dr Fetzer been conversant with the
literature, he would have known it; had the reviewers been
appropriately chosen, they would have called him on it.  The fact that
Dr Fetzer's article was published without appropriate examination of
the literature is failure on the part of CACM which I think is very
hard to excuse.

*On the other hand*, Fetzer's Dilemma does expose an unfortunate
tendency in some parts of the formal methods community that we might
term "Hoare's Folly."  Tony Hoare has said in print that proven
programs remove the need to debug *and to test*.  For the reasons that
Fetzer described, this is clearly untrue.  You don't know the way the
apple tastes until you taste the apple.  The program as a mathematical
construct can be proven; the realized program as a physical construct
-- a sequence of executable operations in a physical memory and their
execution in a physical processor -- can AND MUST be tested.

It is a myth that programs must be verified by theorem provers to be
proven.  Hand proofs can be done; in several small experiments I have
seen very large improvements in quality as measured by number of
defects seen per thousand lines of code (I know, I know, but propose a
better measure and I'll use it.)  These are only slightly better than
pure anechdotes; I am currently looking for research funding to perform
experiments which would more strongly confirm the hypothesis.

It is a fact that many of the clients or customers for very highly
trusted programs require verification using a mechanical prover or
proof checker.  I am willing to work with one when it is required, but
there is as yet little evidence that they provide more certainty than
hand proofs, and hand proofs are lots cheaper.  I can't help but think
that the use of theorem provers in this context is often a case of the
old myth that if it's been blessed by a machine, it is somehow ennobled
and incapable of error.

(I'm not claiming that theorem provers are useless, either.  There are
contexts in which they can be very useful.  There is ongoing research
which will help to delimit these contexts.  We need to know more about
it.)

Program proving isn't a panacea: among other things, a proof doesn'
t tell us a damned thing about the suitability of the requirements to
the user's needs.  I don't see how formal methods can help much with
that question, but there is a lot of "requirements engineering"
literature that I should read before I have an informed opinion.

Pant, pant.

These are, of course, only my opinions.  They are not necessarily held
by Duke University, the Department of Computer Science, or any of my
consulting clients, and would probably be bitterly contested by some
subset of the above.
Charlie Martin (c...@cs.duke.edu,mcnc!duke!crm)


    Reply to author    Forward  
You must Sign in before you can post messages.
To post a message you must first join this group.
Please update your nickname on the subscription settings page before posting.
You do not have the permission required to post.
P A Tsahageas  
View profile
 More options Jan 21 1990, 12:16 pm
Newsgroups: comp.software-eng
From: zmac...@tsun5.doc.ic.ac.uk.doc.ic.ac.uk (P A Tsahageas)
Date: 21 Jan 90 17:16:10 GMT
Local: Sun, Jan 21 1990 12:16 pm
Subject: Re: Reasons why you don't prove your programs are correct

In article <16...@joshua.athertn.Atherton.COM> jos...@athertn.Atherton.COM (Flame Bait) writes:

   Theorem provers might be slow and expensive, but program provers are
   not available at any seed or price.  Indeed it is doubtful that such
   programs can be written at all.  (See the CACM article entitled "
   Program Verification: The Very Idea".  I can no longer remember the
   exact CACM it was in, sorry.  My best guess would be Sept. 1986 or 1989.)

Could someone post the exact reference, please ?

Periklis Tsahageas
Software Eng. IV
Imperial College, London


    Reply to author    Forward  
You must Sign in before you can post messages.
To post a message you must first join this group.
Please update your nickname on the subscription settings page before posting.
You do not have the permission required to post.
merriman  
View profile
 More options Jan 21 1990, 4:51 pm
Newsgroups: comp.software-eng
From: merri...@ccavax.camb.com
Date: 21 Jan 90 21:51:49 GMT
Local: Sun, Jan 21 1990 4:51 pm
Subject: Re: Reasons why you don't prove your programs are correct
In article <16...@joshua.athertn.Atherton.COM>,
    jos...@athertn.Atherton.COM (Flame Bait) writes:

> With current technology you can not prove a (real-world) program correct.

In my corner of the real world, most programs consist mainly of operating
system and other outside vendor supplied subsystem calls glued together with
rather trivial computations. It seems to me that it is futile to attempt to
prove my programs correct if the low level operations (from my point of view)
are not rigorously defined (let alone proven to be correct themselves).

    Reply to author    Forward  
You must Sign in before you can post messages.
To post a message you must first join this group.
Please update your nickname on the subscription settings page before posting.
You do not have the permission required to post.
Discussion subject changed to "references for how to prove (was Re: Reasons why you don't prove your programs are correct)" by John Kimball
John Kimball  
View profile
 More options Jan 22 1990, 10:26 am
Newsgroups: comp.software-eng
From: jkimb...@SRC.Honeywell.COM (John Kimball)
Date: 22 Jan 90 15:26:41 GMT
Local: Mon, Jan 22 1990 10:26 am
Subject: references for how to prove (was Re: Reasons why you don't prove your programs are correct)
You folks who do use program-proving regularly:  what reading material
would you advise for someone who'd like to start using it regularly?

Thanks . . .
                                                John Kimball

Domain: jkimb...@src.honeywell.com        Honeywell Systems and Research Center
        postmas...@src.honeywell.com      Computer Sciences/Software Technology
uucp: <any-smart-host>!srcsip!jkimball    3660 Technology Drive, MN65-2100
voice: 612/782-7343  fax: 612/782-7438    Minneapolis, MN  55418-1006


    Reply to author    Forward  
You must Sign in before you can post messages.
To post a message you must first join this group.
Please update your nickname on the subscription settings page before posting.
You do not have the permission required to post.
Discussion subject changed to "CACM (was Re: Reasons why you don't prove your programs are correct)" by Frank A. Adrian
Frank A. Adrian  
View profile
 More options Jan 22 1990, 10:27 am
Newsgroups: comp.software-eng, comp.misc
From: fra...@mentor.com (Frank A. Adrian)
Date: 22 Jan 90 15:27:17 GMT
Local: Mon, Jan 22 1990 10:27 am
Subject: CACM (was Re: Reasons why you don't prove your programs are correct)

In article <16...@duke.cs.duke.edu> c...@romeo.UUCP (Charlie Martin) writes:
>But, in fact, these issues had been examined at some length in the
>formal methods community.  Had Dr Fetzer been conversant with the
>literature, he would have known it; had the reviewers been
>appropriately chosen, they would have called him on it.  The fact that
>Dr Fetzer's article was published without appropriate examination of
>the literature is failure on the part of CACM which I think is very
>hard to excuse.

Well, I don't excuse it.  Has anyone noticed the dumbing down of CACM in
order to try to get a broader membership?  Long gone are the days when
you could find mainly articles like "On the Probability Distribution of
the Values of Binary Trees", "Application of Game Tree Searching Techniques
to Sequential Pattern Recognition", and "Complex Interval Arithmetic" (these
titles taken from random from CACM, Vol. 14, No. 2, Feb. '71 - and, BTW, the
sixties issues were even better).

Instead we get whole issues devoted to "Computers and Society", which although
an important subject, is not one which can be very usefully applied to most
Comp. Sci. professionals (although we build the tools, we often have little
say in usage policy).  The inclusion of more "practicum" articles rather than
research is another sign of decline.  And the final nail in the coffin
has been the recent inclusion of a Personal Computing column. Any "technical"
magazine which allows one of these rotten apples into its pages has never stayed
"technical" long.  I don't know if it's because the editorial policy has
shifted before the column appears or if it's just some sort of karmic influence.
However, I still believe that before long we will be seeing articles on "How I
Used Lotus 1-2-3 to do a Least-Squares Analysis" or others of its ilk (after
all, we do have to increase membership, eh?).

All in all, I wish that I could drop the $30 charge for CACM and keep my
membership for Computing Surveys, ToPLAS, SIGArch, SIGPLAN, etc.  However,
ACM will not allow me to do this.  It is becoming more and more obvious to
me that CACM is becoming more of an embarrassment than a flagship publication.
Maybe it's just that I'm grumpy today.  Has anyone else noticed this, or am I
just getting continually more grouchy as the years go along?
--

Frank A. Adrian
Mentor Graphics, Inc.
fra...@mntgfx.com


    Reply to author    Forward  
You must Sign in before you can post messages.
To post a message you must first join this group.
Please update your nickname on the subscription settings page before posting.
You do not have the permission required to post.
Discussion subject changed to "references for how to prove (was Re: Reasons why you don't prove your programs are correct)" by Mark Runyan
Mark Runyan  
View profile
 More options Jan 22 1990, 5:50 pm
Newsgroups: comp.software-eng
From: run...@hpirs.HP.COM (Mark Runyan)
Date: 22 Jan 90 22:50:45 GMT
Local: Mon, Jan 22 1990 5:50 pm
Subject: Re: references for how to prove (was Re: Reasons why you don't prove your programs are correct)

>/ c...@romeo.cs.duke.edu (Charlie Martin) / 12:11 pm  Jan 20, 1990 /
>I can't answer the question "why I don't prove my programs correct"
>because I do.  All the time.  As a matter of course.  Almost without
>exception.

I've been trying to follow this string, remembering those days in college
when the instructor indicated that program proof of correctness was
possible, but intractable.  Now someone claims to do it.  Apparently,
often.  

o- Do you use a program or tool to do it?  
o- How complex a program are we talking about?
o- If a tool is used, how would I go about acquiring it?  If a tool isn't
    used, what literature (books, articles, or pamphlets) is available to
    the "engineer in the field"?

And, if this posting makes me sound ignorant or ill-informed, please
be kind in your flames...

Mark Runyan


    Reply to author    Forward  
You must Sign in before you can post messages.
To post a message you must first join this group.
Please update your nickname on the subscription settings page before posting.
You do not have the permission required to post.
Discussion subject changed to "Have *YOU* ever written a program which COULDN'T be proven correct?" by Marshall Cline
Marshall Cline  
View profile
 More options Jan 23 1990, 4:56 pm
Newsgroups: comp.software-eng
From: cl...@cheetah.ece.clarkson.edu (Marshall Cline)
Date: 23 Jan 90 21:56:08 GMT
Local: Tues, Jan 23 1990 4:56 pm </