I have spent more than a little time on this problem and have
probably looked at more approaches to specification than most,
probably well over a 100. I would have to agree. Most of the very
formal methods such as VDL or those based on writing predicates in
the equivalent of first-order logic end up with very complex
predicates. Which of course means there is a higher probability of
errors in the predicates than in the code. (Something I pointed out
in a review for a course of the first PhD thesis (King's Program
Verifier) that attempted it. Much to the chagrin of the professor.)
Of course protocols are a much simpler problem that a specification
of a general program (finite state machine vs Turing machine), but
even so from what I have seen the same problems exist. As you say,
the best answer is good clean code for the parts that are part of the
protocol and only write requirements the parts that aren't. The hard
part is drawing that boundary. There is much that is specific to the
implementation that we often don't recognize. The more approaches
one can get, the better. Triangulation works well! ;-)
At 2:29 AM +0000 1/8/13, John Levine wrote:
> But some people feel we need a more formal specification language
that goes beyond "key point compliance" or "requirements definition",
and some are using 2119 words in that role and like it.
Having read specs like the Algol 68 report and ANSI X3.53-1976, the
PL/I standard that's largely written in VDL, I have an extremely low
opinion of specs that attempt to be very formal.
The problem is not unlike the one with the fad for proofs of program
correctness back in the 1970s and 1980s. Your formal thing ends up
being in effect a large chunk of software, which will have just as
many bugs as any other large chunk of software. The PL/I standard is
famous for that; to implement it you both need to be able to decode
the VDL and to know PL/I well enough to recognize the mistakes.
What we really need to strive for is clear writing, which is not the
same thing as formal writing. When you're writing clearly, the places
where you'd need 2119 stuff would be where you want to emphasize that
something that might seem optional or not a big deal is in fact
important and mandatory or important and forbidden.
R's,
John