|
0 |
Some Notes on Proving Programs Correct
|
|
1 |
======================================
|
|
2 |
|
|
3 |
* status: under construction
|
|
4 |
|
|
5 |
There's a certain confusion I sometimes see in software
|
|
6 |
developers when the topic of program proving comes up.
|
|
7 |
|
|
8 |
Maybe you start talking about showing that some algorithm
|
|
9 |
is correct, or proving that some program is safe. They
|
|
10 |
respond in a way where it's apparent (after, perhaps,
|
|
11 |
some laboured clarification) that they're taking this to
|
|
12 |
mean that the program can somehow be correct, or safe, in
|
|
13 |
some _absolute_ sense — as if you could take all the
|
|
14 |
programs in the universe and divide them objectively into
|
|
15 |
two buckets, one containing all the correct programs, and
|
|
16 |
the other containing all the incorrect programs.
|
|
17 |
|
|
18 |
But this isn't the case at all. In order to have a proof
|
|
19 |
that a program is correct, you first need to have a
|
|
20 |
definition of "correct". You have to say what it means when you
|
|
21 |
declare, "This program is correct, but this other one isn't."
|
|
22 |
|
|
23 |
There is, in fact, no single definition of "correct"
|
|
24 |
(or "safe").
|
|
25 |
|
|
26 |
To put it another way, you can only really ever prove that a
|
|
27 |
program has a certain property or properties, and "correct"
|
|
28 |
is just a shorthand for a bundle of properties that a program
|
|
29 |
must have if it can be said to fulfill its requirements.
|
|
30 |
|
|
31 |
When no requirements are given, literally every program
|
|
32 |
is correct. "Vacuously correct", you might say.
|
|
33 |
[(Footnote 1)](#footnote-1)
|
|
34 |
|
|
35 |
But typically, some requirements are imposed, and further,
|
|
36 |
all too often many of those requirements are tacit — everyone
|
|
37 |
involved assumes them, and no one discusses them. And perhaps
|
|
38 |
it's this that leads some people to believe that a program can be
|
|
39 |
"correct" in some abstract, absolute sense.
|
|
40 |
|
|
41 |
At any rate, I think it's useful, in these situations,
|
|
42 |
to just forget about words like "correct" or "safe",
|
|
43 |
and concentrate on the specific properties of the program
|
|
44 |
that you want to prove:
|
|
45 |
|
|
46 |
* Does it always terminate, in a finite number of steps,
|
|
47 |
on all inputs?
|
|
48 |
* Does it ever terminate prematurely, on any input?
|
|
49 |
* Does it ever perform an operation, the result of which
|
|
50 |
is not defined?
|
|
51 |
* Does it ever write to a memory location outside a
|
|
52 |
certain fixed set of memory locations?
|
|
53 |
|
|
54 |
...and so forth.
|
|
55 |
|
|
56 |
A particular kind of property that is worth mentioning, both because
|
|
57 |
it is hard to avoid using the word "correct" when stating it, and
|
|
58 |
because the implications of proving it can be a little disconcerting,
|
|
59 |
are properties like:
|
|
60 |
|
|
61 |
* Does the program correctly compute the factorial function?
|
|
62 |
|
|
63 |
It can be disconcerting because, in order to show
|
|
64 |
that a program computes factorial, you have to have a
|
|
65 |
definition of what it means to compute factorial in the
|
|
66 |
first place.
|
|
67 |
|
|
68 |
But how do you know you have the right definition? You don't.
|
|
69 |
|
|
70 |
Further, a proof like this often has a form where it shows,
|
|
71 |
step by step, that the program computes just what the definition
|
|
72 |
defines. It looks very similar to a proof that two programs
|
|
73 |
compute the same thing. And that can be very unsatisfying
|
|
74 |
if you were expecting it to tell you something about the
|
|
75 |
result or what it means.
|
|
76 |
|
|
77 |
Footnotes
|
|
78 |
---------
|
|
79 |
|
|
80 |
##### Footnote 1
|
|
81 |
|
|
82 |
There's a similar situation with generative art. If you're coding
|
|
83 |
a generator but you make a mistake and the result is unexpectedly
|
|
84 |
more pleasing than what you originally intended it to do, is it
|
|
85 |
really fair to call that a "bug"?
|