[comp.software-eng] Some misperceptions about program proof

hughes@tempest.Berkeley.EDU (Eric Hughes) (03/20/90)

It seems that there has been a lot of discussion about program proving
without a general understanding of what the whole process involves. I
do not claim that any individual misunderstands any individual point;
rather I offer this as clarification to the end of a useful
discussion.  Here then, are four misperceptions that whose explication
would be of benefit.

Misperception 1:  A program by itself is either correct or incorrect.

In my previous posting where I supplied a proof sketch to the posted
subroutine, I made this same point.  Correctness applies to a program
insofar as it has preconditions and postconditions attached to it.

The issue here is one of semantics.  A program, by itself, is just
syntax (at least, mostly syntax).  A statement of that the program
(and here I mean subroutine, loop, statement, etc.) does is not
contained as such within the statements of the program.  A signifer
of the intended semantics is often included in the name of the 
subroutine/variable/program, as sqrt(), to implement a square root
function, or insert_node_with_rebalancing().  But the name cannot
fully describe the semantics.  The semantics, at best, are contained
in the statement of the preconditions and postconditions.

Misperception 2:  The proof is developed after the code is written.

This can, of course, be done.  The method works best, however, if the
proof is written at the same time as the code.  Furthermore, it works
best when the proof guides the construction of the code.  It is often
said "a program and its proof"; I have begun to think of "a proof and
its program."

As Gries says in _The Science of Programming_, "Programming is a goal-
oriented activity."  In other words, you should have the postcondition
in mind before you start.

What the idea is (and it works; I do it) is to state first what you
want to do, and then to work backwards from the postcondition,
changing it as you go, working back to the precondition all the time.
This assumes you know what you want to do, of course, which is a much
harder thing than most people imagine.  One's mindset changes, as
typified by the question "What do I do next?" changing to "How do I
make this true?"

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

This misperception requires both the preceding two.  Such a compiler
would require that statements be alternated with assertions and that
all preconditions and postconditions be stated.  Furthermore, it would
require that all loop invariants be stated together with their bound
functions and guards.  It would also likely require the explicit
assertion of intermediate steps in the proof.  But I do think that
such a compiler could be written.  It would not be easy for any
current language I know of, because none of them are simple and
elegant enough, including C, or, possibly, especially C.  In any case,
only the program statements would be retained; there would be entirely
new syntax for describing the assertions and predicates.

As Hoare said: "I conclude that there are two ways of constructing a
software design: One way is to make it so simple that there are
_obviously_ no deficiences and the other way is to make it so
complicated that there are no _obvious_ deficiencies."

A further hurdle to such a compiler would be that it would itself
have to be proved correct in order for it to have any credibility.
This would require that for those sections of the code that are
automatically generated, the proof, as well, should be automatically
generated.  This is, I suspect, the least of the hurdles.

Misperception 4:  Writing a program and proof takes forever.

Forever is an awfully long time. :-) Currently, I admit, it does take
a long time to write a correct program.  A large part of that, though,
is that common constructions must be thought about over and over
again.  There simply has not been enough practice in writing correct
programs that the common, repeated features are well understood and
embedded in language design.  All the books on program correctness
(that I know of) deal with writing correct algorithms, not with
writing implementations of correct algorithms by writing correct
programs.  (This is, at least, basically true.  Gries does have a
small section about "Writing Programs in Other Languages", but it is
not a treatise on how to write whole software packages which are
correct.)  As common constructions are identified and named, it will
be much easier to think about program proofs, making it much faster
to write correct software.

Another hindrance is the lack of software tools.  A first step would
be a lint-like processor which takes a program whose proof is entirely
within comments (meaning no alteration to existing compilers) and
prints out a list of assertions which it cannot justify from the
program text.  Such a tool would not verify that a program was
correct, but it would allow correct programs to be written.  This tool
would also be able to check that the pre/post-conditions of a
subroutines definition match those used in its reference.

Misperception 5.  Program correctness will solve all your problems.

Oops, that's a dead horse. :-)

Eric Hughes
hughes@ocf.berkeley.edu

skrbec@cell.mot.COM (Brad Skrbec) (03/20/90)

hughes@tempest.Berkeley.EDU (Eric Hughes) writes:

><...>

>Misperception 1:  A program by itself is either correct or incorrect.
><...>
I agree that the preconditions and postconditions are what determine
whether a program or subroutine is correct or incorrect for the problem
domain.  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.

>Misperception 2:  The proof is developed after the code is written.

>This can, of course, be done.  The method works best, however, if the
>proof is written at the same time as the code.  Furthermore, it works
>best when the proof guides the construction of the code.  It is often
>said "a program and its proof"; I have begun to think of "a proof and
>its program."

The proof development can and often should accompany the development
of the code, but it probably shouldn't guide the goal of the code.
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.  We use an independent testing group, and they
are kept apart from the code designers and writers, so that they have
an unbiased view of what the code should do.  If the coders start
to work too closely with the testers, they tend toward similar false
assumptions, and errors go undetected until too late.
><...>

>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".  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).
Syntactically, I believe this is already done by strongly typed
compilers such as Ada and some others.

hughes@locusts.Berkeley.EDU (Eric Hughes) (03/21/90)

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