Re: I'm struggling with 2219 language again

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

 



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



[Index of Archives]     [IETF Annoucements]     [IETF]     [IP Storage]     [Yosemite News]     [Linux SCTP]     [Linux Newbies]     [Fedora Users]