Newsgroups: comp.lang.misc
Path: utzoo!utgpu!watserv1!watmath!tolstoy.waterloo.edu!mhcoffin
From: mhcoffin@tolstoy.waterloo.edu (Michael Coffin)
Subject: Re: Formal definitions (Re: ada-c++ productivity)
Message-ID: <1991Apr11.214018.19443@watmath.waterloo.edu>
Sender: news@watmath.waterloo.edu (News Owner)
Organization: University of Waterloo
References: <1755@optima.cs.arizona.edu>
Date: Thu, 11 Apr 1991 21:40:18 GMT
Lines: 76

In article <1755@optima.cs.arizona.edu> gudeman@cs.arizona.edu (David Gudeman) writes:

>(1) given that you already think the program is correct by the rules
>of its own notation, why does it increase your confidence just because
>you have another "program" in another notation that says the first one
>is correct?
>
>(2) Is the mathematical notation more reliable in some sense?  If so,
>how?
>
>(3) Is formalism (proof of correctness) more reliable than experience
>(testing)?  If so, how?
>
>I would answer that yes, proofs of correctness do increase the
>confidence in a program, but not because of (2) or (3), to which I
>would answer "no".  There is another reason that proofs of correctness
>are useful that I think Mike knows but hasn't expressed clearly.
>Hint: what is the main way to acheive fault tolerance?

I assume you mean that proofs are a just a form of redundancy---a way
to "write the program twice".  There's something to that, but it
isn't the whole story.  Programming languages, at least imperative
languages, are constructed from statements, which say "do this, then
this, etc.".  They don't say "achieve this goal", which is really the
purpose of running a program.  A proof connects these two ideas; it's
a way of verifying that executing a sequence of statements achieves
a particular goal.  

Here's an analogy to illustrate the difference (off the top of my
head, so let's not push this too far).  Suppose I'm telling you how to
get to my house.  A strictly imperative program looks like

    go two blocks north,
    turn left,
    go straight 4.1 miles,
    turn left,
    then right at the second corner.

Proving a program is like adding landmarks to the program and then
showing that the actions get from one landmark to the next:

    { you are at your house }
    go two blocks north,
    { there's a McDonalds on your right }
    turn left,
    { you are now on Main St. and Limberlost}
    go straight 4.1 miles,
    { You will see a blue house on the corner }
    turn left,
    { You are at the corner of Birch Ave. and Main }
    then right at the second corner.
    { You're in my driveway; look for my grey Mazda }

Besides giving you more confidence while you're driving, the proof has
the property that it abstracts away detail.  If you make it to Birch
Ave. and Main, you're in good shape regardless of the twists and turns
it took to get there.  But more importantly, notice that the original
program doesn't say anything about what each step accomplishes, or
even what the program as a whole accomplishes.  In the original
program, it's difficult to see if "go straight 4.1 miles" is right
without trying the entire route; there's no mention of what "go
straight 4.1 miles" ought to *do*. That's all informally
(mis)understood.  In the proven program, that statement can be checked
in isolation: it ought to get you from Main and Limberlost to a corner
with a blue house.

As far as your last question goes, I don't know if proofs are more
reliable than testing for sequential programs.  For concurrent
programs, where nondeterminism can cause a program to run for weeks
and then suddenly fail, I would guess that proofs are far more
reliable. 

Michael Coffin				mhcoffin@watmsg.waterloo.edu
Dept. of Computer Science		office: (519) 885-1211
University of Waterloo			home:   (519) 725-5516
Waterloo, Ontario, Canada N2L 3G1