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

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

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.)

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

   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

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)

   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

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

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).

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

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

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

SCENARIO: you're working for MicroS*ft on their new whiz bang C++
compiler (I don't even know if they *have* a C++ compiler :-).  You
work hard at your assignment (the parser, for example).  You tell your
boss that you think it works, but you have discovered that your code
is in the class of undecidable programs, being transformed from
Godel's famous 1931 example.

You think your boss will be pleased?  I doubt it!

Indeed, I doubt *ANYONE* on the entire net has *EVER* written a
real-life program which couldn't in theory be verified.  We all (well,
except for a few of those who posted earlier) know that finding a
decision procedure for the predicate calculus (called the
"Entscheidungsproblem" and "Hilbert's Program" in various places) is
impossible, and therefore the halting problem and program verification
are undecidable.

But this is a *theoretical* concern which *rarely* impacts our practical
"here's a program, boss" world.

The fact of the matter is that program verification is *hard*.  It's
limitation in everyday life is that it's *hard*, not that it's undecidable.

Furthermore it *is* semi-decidable.  Ie: there exist procedures which
will always detect that correct programs *are* correct.  The problem
is that no *algorithm* can exist for this, since somewhere out there
there exist programs which will defy proof (or perhaps they are false
but they defy finding a counter-example).

So don't think you can't find *anything* via program verification.
It's just that you can't find *everything*.

Marshall Cline
--
=========================================================================== ====
Marshall Cline/ECE Department/Clarkson University/Potsdam NY 13676/315-268-3868
 cl...@sun.soe.clarkson.edu, bitnet: BH0W@CLUTX, uunet!clutx.clarkson.edu!bh0w
  Career search in progress: ECE faculty. Research oriented. Will send vitae.
=========================================================================== ====

In article <CLINE.90Jan23165...@cheetah.ece.clarkson.edu> cl...@sun.soe.clarkson.edu (Marshall Cline) writes:

There does not seem to be much recognition by anyone in any of the
groups which are discussing this subject that there is a difference
between *UNDECIDABILITY* and *INCOMPLETENESS*.  (Sorry, this isn't
meant to be a flame, I just don't want to sound like I'm picking on you
in particular, Marshall.)  The fact that the halting problem is
undecidable does not mean that we cannot prove whether or not a program
halts.  What it does mean is that there is no algorithm which will come
up with the answer.  The impact of this is that there can be no program
which will take specification and implementation as inputs and decide
whether the implementation is correct.  However, this does not mean
that there is no proof of correctness.  It certainly does not mean that
there is no proof checker.  In other words, there can be a machine
which will take specification, implementation and `proof' of
correctness and decide whether the `proof' really is a proof.

Insomuch as a verification relies on `theorems' for which there is no
known proof, I for one would much prefer to know that the theorem is
taken as an axiom.  It is not beyond the state of the art to have a
verification theory which is complete whenever the theory of the
underlying data types is complete (i.e. the things you want to
manipulate in the program).  This is the best we could hope for.  It
means, for instance, that we do not know a proof that

  IF ((n>2) AND (a>0) AND (b>0) AND (c>0) AND
      ((a^n) + (b^n) = (c^n)) THEN p ELSE q

is equivalent to q under the assumptions that a, b, c and n are all
integers and we have some way of evaluating the equality correctly.
On the other hand, anything which cannot be proved can be reduced to a
statement in the theory of some of the data types which cannot be
proved.  I think most programmers would shy away from depending on such
theorems for correctness without some explicit recognition of the fact.

                                                        Geoff Barrett

In article <1...@gould.doc.ic.ac.uk> zmac...@doc.ic.ac.uk (P A Tsahageas) writes:

Fetzer, James H.  "Program Verification:  The Very Idea."
Communications of the ACM, Volume 31, Number 9 (September 1988), pp. 1048-1063.

Hope this helps.

chris...
--
c...@tove.umd.edu    Computer Science Dept, U. Maryland at College Park
                    4122 A.V.W.  301-454-8711   <standard disclaimers>

From fra...@mentor.com (Frank A. Adrian):

   As a publication which is directed to ALL MEMBERS, CACM must publish
   material which is relevant to its audience.  Those who want narrowly
   targeted technical material should read the more specialized technical
   journals.  CACM, which once seemed to feature more Greek letters than
   ASCII characters, has now become a (relatively) lively and readable
   publication.  Given that CACM's audience includes both researchers
   and practitioners, it would seem that a judicious mixture of research
   and practicum would be most appropriate.  Research results need to be
   communicated to practitioners in a readable form, and practical
   considerations should help to guide researchers in their search
   for things which will be of significant benefit to society.  CACM
   serves to prevent either community from becoming too absorbed in
   itself, and facilitates communication within the computer science
   community.

   As described above, there may well be good reasons for this policy.

   Let's hope so.

   Bill Wolfe, wtwo...@hubcap.clemson.edu

From article <15992.25b9e...@ccavax.camb.com>, by merri...@ccavax.camb.com:

True, but for safty critical systems there is verified hardare out there.
The viper chip.
Also safty critical stuff tends to be small and embeded(no os).
There are folk working on verified os's.

In article <1990Jan22.152717.7...@mentor.com> fra...@mntgfx.UUCP
`                          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.

The approach that you criticize is similar to that of the IEEE societies
(e.g., the Computer and Communications Societies) and their 1) general
purpose magazines and 2) special purpose transactions.  What would you
propose that the ACM do differently?  I certainly prefer the ability to
select the technical areas that I pay for by joining SIGs and
subscribing to transactions.

The trend that you have noticed in publications is paralleled in
conferences.  While the NCC has fallen on hard times, conferences with a
narrower focus (e.g., CSCW, HCI, OOPSLA and TRI-Ada) are flourishing.  I
think these trends are symptoms of growth in both scope and depth in the
CS/IS/SE field(s).  Some realignment of ACM publications (baseline 1971)
was necessary.  I would hope that our (the ACM) publications board would
welcome suggestions on how to better serve the growing and diverse
interests of our fellow members.
--
/s/ George   vmail: 703/883-6029
email:  mitch...@community-chest.mitre.org    [alt: gmitc...@mitre.arpa]
snail:  GB Mitchell, MITRE, MS Z676, 7525 Colshire Dr, McLean, VA  22102

I hate stepping in sticky piles of whatever...

Note the term I used, "proof of correctness"...

There is a difference (perhaps only in *my* mind) between using the
predicate calculus proof of correctness and program verification.  If
we call code inspections and regression testing "proofs", then, I do
prove my programs.  I was under the mistaken expression that someone
was using an automated proof assistant.  My apologies to netters for
stepping into an argument where I didn't share the same understanding
of the terms.

Mark Runyan

How about:
 - Careful review by researchers in the field, so that something like
   Fetzer paper doesn't happen again
 - "targeted" issues that explore topics in depth with research
   papers and in-depth survey papers, such as IEEE Computer does
 - A detailed goal for CACM -- right now it seems to try to be
    - a technical magazine
    - a club news journal
    - a practitioner's magazine ("the new Dr. Dobbs")
   and it ends up not doing any of these very well

Acutally, at this point ACM has managed to alienate large portions of
its research audience, and recovery is going to be difficult.  That's a
pity since it used to be a flagship publication, useful to researchers
and practitioners alike.  Right now, there really isn't enough meaningful
content to be useful to many people.
                                Tim

In article <1990Jan22.152717.7...@mentor.com>, fra...@mentor.com (Frank A. Adrian) writes:

        I guess it depends upon what role you think the "flagship" publication
of the ACM should fulfil. I believe that generalist articles create a
common ground of interest. The SIG publications contain enough technical
literature without filling up CACM as well.
        I think we have to acknowledge that CS profesionals play a very
important role in society and issues such as database matching, organizational
impact of IT, computer based elections etc. should be the concern of these
people. I'm always reminded of people like Oppenheimer who have had an enormous
effect on the kind of world/societies we live in. Frankly, I'd rather read
about his pre and post reactions to the Manhattan project or something like
that then another paper on "how I made a bigger bang", important though
that might be.
        I guess its a sense of balance that we should pursue. I certainly
don't agree that CACM has been "dumbed down" by being more generalist. If
anything, many of the problems raised in the CACM generalist pieces are
more difficult to solve than the papers which describe a problem with say,
data structures and "How I did something clever with B-Trees" to solve it.
The latter is probably more relevant to our daily work, but we need a
perspective beyond this as well ? :-)
        Cheers.

__  _______________________W_(Not Drowning...Waving!)___________________________
Perry Morrison  Ph.D
SNAIL: Maths, Stats and Computing Science, UNE, Armidale, 2351, Australia.
per...@neumann.une.oz    or pmorr...@gara.une.oz          Ph:067 73 2302

I just don't understand this trashing of Fetzer or the cricisms of CACM.

With regard to the former.  While some of you may be involved in
projects with verified code; most of us are forced to use UNIX, VMS,
MSDOS, CMS, ORACLE, USENET, TCP/IP and other *useful* systems which
are most definitely *not* verified.  The compilers are not verified. The
hardware is not verified.  And we are writing software for use
by human beings whose behavior must be included in the model of the
system we might attempt to verify.  Now, this is not to say that the real
world of "software engineering" would not be improved by "proven"
programs, nor even to say that systems *cannot* be proven correct.  But
there is a difference between mathematical models of computation and
practical implementations of computing systems (just as there is a
difference between theoretical and applied mathematics).  Whether
Fetzer's arguments are correct or not, the questions raised are
important for the practicing programmer.

Now, ACM is not just for grad students and researchers.  There are
various archival journals (e.g. JACM) published by ACM which are
not "dumb."  For the professional practitioner there are many real
societal issues that are rightfully addressed in CACM.  Personally,
I would prefer more "Programming Pearls" and "Literate Programming"
type content and less Greek gobbledegook; however, those of you
fortunate enough not to have to get working systems out the door
in the next 3 months might have other preferences. And that's okay.

--
        Brad Sherman (b...@alfa.berkeley.edu)

   I just don't understand this trashing of Fetzer or the cricisms of CACM.

   With regard to the former.  ... Whether
   Fetzer's arguments are correct or not, the questions raised are
   important for the practicing programmer.

That is exactly the point.  The questions are important.  The problem with
the CACM is that the article was a travesty.  The arguments ranged from
trivial to misleading (at least they were not actually false).  There was
a recent posting in this news group that was of far higher quality. Back in
the 60's, CACM would have published an article that accurately portrayed
the current state of program proving, and detailed a new result in the
area, understandable by a non-expert that was willing to work at the article.

Perhaps it is not CACM's fault ... perhaps (shudder) those are the best
articles that are being submitted.  The problem is that IEEE Computer is
doing a much better job, and THAT indicates that it may well be something
wrong with CACM.

Geoff Clemm

No one has said this yet, though James Adcock and Joshua Levy have
alluded to it:

   ***************************************************************
   **** For a large class of programs, "correct" is UNDEFINED. ***
   ***************************************************************

In general, the big, real-world programs that we spend big bucks to
create, things like telephone systems, air traffic control, SDI, 1-2-3,
and "unix" don't support the abstraction of "correct."  Their
specifications are partly on paper, but mostly exist as concepts of
greater or lesser exactness in the minds of a large number of people.
Obviously, these concepts are not identical from one person to another.

When a program functions in ways that most of those people decide agrees
with their concepts, it is said to be "working;" when it functions in
way that most decide disagrees, it is said to be "wrong."  (When there is
no majority opinion either way, it is "unfinished.")

I'm afraid that belief that we will someday be able to prove our
largest, most important programs correct has become one of my tests of
native intelligence, along with belief in astrology and support of the
flag-burning amendment.

                 -- Bob <Mu...@MITRE.ORG>, linus!munck.UUCP
                 -- MS Z676, MITRE Corporation, McLean, VA 22120
                 -- 703/883-6688

I just gave a talk on myths of verification, and this was one of the
ones I mentioned.  It was true in a sense, a long time ago, when
Floyd-style proofs were the only ones that could be done.  It is no
longer true now, in the sense that proof of program texts or notations
that are semanitcally reasonably well behaved can be done.  It is still
true in the sense that there are classes of programs and programming
languages which are so badly behaved that it's hard to prove anything
about them.  Ada and C are both in this class.  Interprocess
communication tends to be difficult, asynchrony is hard (but the
technology is catching up, see e.g. some of Leslie Lamport's work.)

The basic trick comes down to this:

(1) describe your specification as formally as you can.  Things like Z
specifications are very handy, but a little mathhematical maturity and
some thought can lead to a document in mathematical prose which encodes
most of the hard parts in a crisp way.  (And recognize that there will
be requirements which are not amenable to formality:  "the system will
be built in a well-structed fashion"; "the human interface will be easy
to use and consistent." You have to pay lip service to them, because
saying "this is crap" will get you talked about at annual reviews, but
you should generally try to do a good job and challenge them to show you
didn't meet it if pressed.)

(2) describe your program first in a notation that is well-behaved, and
for which the semantics are simple.  I use Dijkstra's notation ("the
programming calculus") because it is the first one I used, I'm
comfortable with it, and I find the reasoning rules intuitive.  But use
the _Science of Programming_ [Gries] to get a start with it, not
Dijkstra's book.

(3) complex programs, espeically programs that depend on the system in
which they are embedded (e.g., window programs), will have things that
you can't prove, but must assume.  This need not stop you.  You must
first try to understand those things formally; second, state them
formally in the semantic formalism you are using.  I would, for example,
try to state the weakest-precondition specification for a window routine
using informal arguments.  Third, when you write your program, make sure
that you TEST, yes test, the program with particular attention to the
things you couldn't prove.

As an aside, this does NOT mean that there is no "proof" because the
proof depends on components that are unproveable; it does not.  What
you are doing is introducing new axioms into your theory; these axioms
are statements about the semantics of the operations which you can't
prove.  As in any usual deductive system, either these statements are
theorems or they are not.  If they are theorems (i.e., the unproven
chunks do behave as specified) then you're in fat city.  If not, you
will have a defect there, so long as the defect in the underlying stuff
is exercised by what you write.  Conveniently, most of these things are
also things which are extremely well tested, so you have good evidence
to believe that it will work.  This is very much like the way
mathematics has been done in history: Euclid's axioms are formal
statements of things that were observed to be true in many cases.  The
formal system derives results that always correspond to reality on
Earth so long as the scale is limited.  But when you get outside of the
range that Euclid could observe, or the limits of classical Greek
measuring instruments, you observe the axioms do not correspond to
truth in the large.  

As another aside, there is a sort of competing body of work on the IBM
Software Clean Room.  I don't have references right at hand, but they
should be easily found.  They use a notation that I consider exceedingly
ugly, but they get good results in their hoard-of-programmers
environment.  I don't personally think their methods are completely
workable for smaller groups, or groups with less formal structure, which
also describes the kind of group I like to work in.

(4) Code the program in any convenient language.  I use C or C++ almost
exclusively.  This coding is translation from the design notation to an
executable notation; you should argue for each translation that the
semantics of the executable match what you describe in the design.  This
is easier than it sounds, but you have to be careful about places where
the language is wierd.  One that I've run into recently is that there
are cases where a[i] is NOT the same as *(a+i), in all compilers I can
test with.

Not regularly, although I have done so.  It is much harder using tools
to do the proofs, in general.

I've done programs up to about 10K source lines of C.  The IBM Clean
Room people have done several bigger ones with many programmers working
together.

isn't used, what literature (books, articles, or pamphlets) is
available to the "engineer in the field"?

As I said above, I like Science of Programming by Gries.  I have a book
called _Program Derivation_ by Geoff Dromey (Addison Wesley 1989) which
looks pretty good, but I haven't had time to read it closely.  I hope
someday to write The Ultimate Book On Proof In Software Engineering, but
I wouldn't hold my breath if I were you.  Therea re a number of other
books that other may recommed, which I like more or less well.

Charlie Martin (c...@cs.duke.edu,mcnc!duke!crm)

In article <CLINE.90Jan23165...@cheetah.ece.clarkson.edu> cl...@sun.soe.clarkson.edu (Marshall Cline) writes:

In real programs, the whole halting problem (and the stronger
equivalence problem) do not apply, because all real realizations of
program are finite state machines; both of these are decidable for
finite state machines.

If someone wants to claim they are NOT finite state machines, I want to
see your machine with infinite memory registers.

Charlie Martin (c...@cs.duke.edu,mcnc!duke!crm)

That simply isn't true.  Fetzer's argument is precisely that program
proofs are flawed on the face, that no proof can ever give insight or
certainty to the behavior of a real program on a real machine, because
of the distinction between the mathematical model and the physical
world.

But one can argue on the same basis that euclidian geometry has no use
and gives no insight, because the same distinction between mathematical
model and physical world exists; worse, Euclid's axioms for plane
geometry can be demonstrated false in the real world.  Thus it is
useless and morally wrong for surveyors to learn euclidiam plane
geometry, because the real world doesn't fit the model.

Furthermore, the questions raised -- while they are real and significant
questions, and must be considered, and while there clearly are people
who needed the reminder -- have been explored in the verification
literature.  They form the basis of at least three research efforts I
know about (the CL Inc Trusted Stack, the Odyssey hardware verficication
efforts, and the UK verified hardware/software stuff).  Fetzer's paper
did not explore that existing research, and further used very old
publications exclusively.  Fetzer came up with a real issue but made no
contribution other than filling a number of pages, because this
literature was not reviewed.  It was an extremely poor showing on the
part of CACM; my personal opinion is that the editors involved should
resign.

Charlie Martin (c...@cs.duke.edu,mcnc!duke!crm)