Path: utzoo!attcan!uunet!lll-winken!brutus.cs.uiuc.edu!usc!zaphod.mps.ohio-state.edu!uakari.primate.wisc.edu!ames!pasteur!agate!agate!hughes
From: hughes@locusts.Berkeley.EDU (Eric Hughes)
Newsgroups: comp.software-eng
Subject: Re: Some misperceptions about program proof
Message-ID: <HUGHES.90Mar20085846@locusts.Berkeley.EDU>
Date: 20 Mar 90 16:58:46 GMT
References: <HUGHES.90Mar19095708@tempest.Berkeley.EDU> <1751@teal4.UUCP>
Sender: usenet@agate.berkeley.edu (USENET Administrator;;;;ZU44)
Organization: ucb
Lines: 139
In-reply-to: skrbec@cell.mot.COM's message of 20 Mar 90 15:02:09 GMT

In article <1751@teal4.UUCP> skrbec@cell.mot.COM (Brad Skrbec) writes:
>hughes@tempest.Berkeley.EDU (Eric Hughes) writes:

>However, if the results of a subroutine don't apply to the 
>pre- and postconditions, is the subroutine incorrect, or is it being
>incorrectly used?  If I use a Sine subroutine where I need a Cosine
>result, the Sine routine isn't incorrect, only inapplicable.

It is incorrect, because no proof can be exhibited (since none exists)
which asserts that the answer is a cosine if the calculated value
is a sine.

For example, the following program is incorrect, because one cannot
demonstrate that y is in fact the cosine of x after execution of the
program.  This does not mean that the code statements don't do
anything, simply that they have not been demonstrated (with a proof or
proof sketch) that they do in fact do something.  You can, however,
compile the program (with a regular C compiler) and exhibit (with a
program execution) behavior.

{ true }
y = sin( x )
{ y == cos( x ) }


>The proof development can and often should accompany the development
>of the code, but it probably shouldn't guide the goal of the code.

I disagree.  It is my own coding experience, that if you do let the
proof guide the code, it is much easier to construct programs that
work, let alone be correct.  More below.

>If the proof contains misconceptions, then they are automatically
>carried over to the code, and now you have not one source of false
>information, but two.

If the proof contains a logic flaw, then this does in fact happen; I
cannot deny this, and in a hand checked proof system, this will always
be a problem, that one can only be sure about the correctness of the
program to the extent that you are sure about your abilities at
logical manipulation.

However, in a machine checked system (assuming, for the sake of
argument, that the machine checker is correct and bug-free) the only
possible misconceptions are those in the preconditions and
postconditions, exactly those predicates which are supplied by the
programmer.  You will get a correct program, but you may not do what
you think it should do or want it to do.  This is what Dijkstra refers
to as "the pleasantness problem."  However, the virtue of good design,
per Hoare, whom I quoted earlier, is that a complicated specification
should be simple enough that there are "_obviously_ no deficiences."

Here is a small example to illustrate the pleasantness problem.

{{ true }}
switch( a ) {
    case 1 :
        if ( doremi( x ) )
            break ;
    case 2 :
}
{{ true }}

The postcondition is true, so the program is correct, because every
program that halts satisfies the true postcondition.  But does this
program do anything useful?  No.

>  If the coders start
>to work too closely with the testers, they tend toward similar false
>assumptions, and errors go undetected until too late.

No argument here.  Making sure that others think a formal spec means
the same thing to them as it means to you is definitely a good idea.
This is one part of a solution to the pleasantness problem.

>>Misperception 3:  Writing a compiler which only compiles correct
>>programs is impossible.

>This may be a false perception, but I doubt that you'll disprove
>it any time soon.  Again, this all depends on what you consider
>"correct".

I alluded to this earlier.  One of the very hardest things to prove a
compiler correct is to write down just exactly what it really does.
One could, for example, construct the "strongest postcondition", from
a true precondition, of, say GCC, but I doubt that it would be
readable or understandable.  (The strongest postcondition is technical
term, which means loosely in this context "a formal specification of
what the program really does.")  I would love to see it as a goal of
the computer science community to be able to state in both simple and
elegant language the right kinds of formal specifications for complex
programs such as compilers, operating systems, and editors.  (Such
language may be large, but that by itself doesn't prevent it from
being simple.)

>  Semantically, I think that current technology won't
>allow this (We have tried AI verification programs that take
>a week to do what one could do manually in a couple of hours).

When you mention AI in this context, it makes me wonder what type
of verification system you were using.  An AI system that tries
to come up with, say, loop invariants is bound to fail at its
goal, because the general problem is equivalent to the halting
problem.  (That is, by the way, the reason for a bound function;
one _must_ prove that every loop halts.)  What such a compiler
really needs is a way to verify that the invariants supplied by
the programmer are valid.  What we need is a proof checker, not
a proof constructor.

Now I don't know what kind of verification system you were using,
so this argument may not apply to you.  It is, however, of
vital importance in using correctness as a useful tool.

In the proof I posted earlier, one of the invariants was something
like "n' = s' + n * b^u."  Only people can come up with those kinds of
invariants effectively.  The problem with automatic generation is
fundamental.  True sentences are recursively enumerable, but not
decidable.  In other words, if you have a postcondition to a program,
and that postcondition is provable from the program and precondition,
then you eventually can automatically generate a proof of that
postcondition.  But if that postcondition is not provable, then you
may never find a disproof, i.e. the constructor may never halt.

>Syntactically, I believe this is already done by strongly typed
>compilers such as Ada and some others.

Strong typing (or, more correctly, robust handling of the
interpretation and representation of concrete and abstract types) is
one necessary element of a correct compiler.  But it does a fairly
small amount of the real work of proving a program correct, even if in
practice strong typing is extremely useful.  Abstractly, strong typing
verifies that all the terms of the program and proof are well-formed,
that is, that the arguments are of the proper domain with respect to
the functions.  However, it is also a manifestation _only_ of
well-formedness, but since one can only speak of correctness with
respect to well-formed formulas, it is a necessary aspect.

Eric Hughes
hughes@ocf.berkeley.edu