jbn@glacier.STANFORD.EDU (John B. Nagle) (02/16/89)
Well, Parnas-type formal specifications aren't it. We used SRI's
SPECIAL language extensively in the Kernalized Secure Operating System
effort (1978-1982), and as it turns out, the specifications for an
interesting system are only a factor of 2 to 4 smaller than the code
itself. Worse, they are less comprehensible. Parnas has backed off
from his original idea that specs should have meaningless variable
names so that people would be compelled to follow the math, but even
with useful variable names, formal specs are still very hard to read.
Also, since you can't run them, there's no way to test them. Structured
walkthroughs help, but are very expensive and still only find some of the
errors.
The fundamental problem with formal specifications is that if behavior
is well enough specified that the outputs for a given sequence of inputs
are uniquely determined, the specification has essentially the same
information content as the program. Any so-called "implementation detail"
that can affect the output in any way must be formalized in the specification.
This leads to large specifications for systems with complex behavior.
What a formal spec turns out to be is a sort of inefficient program
to do the job. Given this, it would make more sense to have a means of
writing simple but inefficient programs to get the desired behavior and then
constructing more efficient programs with provably identical behavior.
John Nagle