Xref: utzoo comp.ai:5493 comp.edu:2893 comp.object:724
Path: utzoo!attcan!uunet!tut.cis.ohio-state.edu!cs.utexas.edu!usc!apple!voder!pyramid!athertn!joshua
From: joshua@athertn.Atherton.COM (Flame Bait)
Newsgroups: comp.ai,comp.edu,comp.object
Subject: Re: Reasons why you don't prove your programs are correct
Message-ID: <16479@joshua.athertn.Atherton.COM>
Date: 12 Jan 90 01:29:37 GMT
References: <25711@cup.portal.com> <1449@krafla.rhi.hi.is>
Reply-To: joshua@Atherton.COM (Flame Bait)
Organization: Atherton Technology, Sunnyvale, CA
Lines: 27

"Proving your programs are correct" seems to mean different things
to different people:

One group thinks it means that your program does exactly what your
spec says it should.

Another group thinks it means that you can put complex assertions
in your code and have the checker makes sure that these assertions
are always true.

The first sort of proof is obviously useless, the spec becomes the
program, and bugs in the spec become bugs in the program.  Also,
specifing most programs is impossible; and if you could, then you
could write a compiler for the specification language.

The second sort of group is more interesting.  It has these advantages:
    It is possible.
    It is not all or nothing (simple assertions can added now, and 
        complex ones added later on).
And these disadvantages:
    Doing it well requires specific skills, which need to be taught.
    It will never prove correctness; it only proves that some assertions
        are true. 
    There are still problems getting test input data.

Joshua Levy                          joshua@atherton.com  home:(415)968-3718
                        {decwrl|sun|hpda}!athertn!joshua  work:(408)734-9822