🚀 go-pugleaf

joshua@athertn.Atherton.COM (Flame Bait) writes:

| kers@hplb.hpl.hp.com (Kers) [that's me] writes:
|  >I'll also think that the remark "specifying most programs is impossible" is
|   >wrong. "bloody difficult, especially after the fact" is the predicate that
|   >springs to mind.
|
|   No problem.  Specifiy the following programs, in a machine readable
|   format useful to a program verifier.  These should be commerical products,
|   so they must look good and feel good so that people want to use them:

Let me admit that I don't have a verifier to hand, so the machine-readability
of any specification I might supply is a little beside the point. (There are
any number of specification languages one might use, with varying degrees of
accessibilility and surface-level checking.)

Let me also admit that "look good" and "feel good" are things I have no idea
how to specify. Can we agree that much of the program behaviour is independent
of the look-and-feel?

[Lest this should seem a cop-out, there's no reason why one shouldn't specify
the "look" in a formal fashion. It's just that "looking good" would have to be
a property that was asserted about particular - eg - screen layouts; it can't 
be derived from mathematics. I just happen to think that this isn't a
particularly important problem *for verification* - it's part of the harder
problem of whether the specification is *appropriate* to the problem at hand.
Discussion encouraged.]

|       A rule based expert system shell.
|	   Remember to specify input and output for an window based system.

What makes the I/O for a window system harder than for a terminal?

|       A source code control facility like SCCS or RCS
|	   If you use system calls you must have some way of proving that
|	   they do what your spec says they do.

No, *I* don't.

I hope *someone* has; one day I'd like there to be a formal proof that they
*do* do what they're supposed to. The behaviour of system calls is given, like
the behaviour of "+"; the correctness of the program is relative to the
correctness of the system calls.

In fact, I can state the correctness of the program in just those relative
terms; *if* these system calls S1 ... Sn have meanings M1 ... Mn, then the
program is correct (has the specified behaviour). You can then examine my
assumptions about the system and decide whether they are justified.

|       <Put most any real world program here>
|
|   My last example points out a current problem with proving program correct.
|   They must only use libraries which have been proven correct, must run on 
|   an operating system which has been proven correct, and must use hardware
|   which is proven correct.  All of this is impossible right now.

True, but ... it depends what you're trying to accomplish. I agree that if we
demand complete proofs - in the sense that the proof extends all the way to
the bedrock - we can't do it [ever - see [*1]]. If we're happy to prove things
relative to some set of base assumptions (system calls behave this way, and if
they don't it's the system call that's broken, not the program) we can practice
separation of concerns.

|   I'm serious about this challenge.  I hold that these program can not
|   be specified in any kind of useful way, and that the set of programs 

How much specification is enough? How little would help? In the case of the
expert system shell, surely a specification of the inference engine (and a
proof that the code satisfied it) would be useful, even if the I/O was on 
shaky ground. After all, if the system misbehaved, you could concentrate your
efforts away from the engine.

|   which can be proven correct is so small as to be uninteresting.

Before I disagree any more I think we ought to decide just what limits we're
prepared (or not) to place on specifications and proofs. For example, do you
think that specifying a "real world program" is *in principle* impossible; if
so, why? Or just that it cannot be done *now*? Do you think that working on
verification is a complete waste of time, or just that some of its proponents
are hypemasters? Would proofs of components strike you as an improvement over
no proofs at all, or do you want the whole cat in the bag?

-- Footnoties follow ----------------------------------------------------------

[*1] You can't prove hardware correct; its behaviour is physics. You can only
prove it relative to your assumptions about the physics of electrons in
semiconductors (or whatever). 

Similarly, you can't prove that an expert system is "correct", if by that you
mean that it gives genuinely "expert" answers. But you could show that it will
give answers that are derivable (in whatever sense is appropriate) from its
rulebase. Proving that the rulebase has some correspondance with reality is
*not* program verification.







--

Regards, Kers.
"If anything anyone lacks, they'll find it all ready in stacks."