Well, even if you choose your formalism first and then use that to
guide the development and specification of the protocols, the
challenge still stands. The operative word in your description is
"portions." Does the technique cover enough of the protocol to be
useful and does it wind up adding or saving time, work, errors, etc?
Steve
Steve Crocker
steve@xxxxxxxxxxxx
On Nov 17, 2005, at 11:56 AM, Hallam-Baker, Phillip wrote:
There is a way, develop a highly targetted formalism for the specific
problem.
This is hard to apply to existing specs because they tend to be
inconsistent. If you are required to apply a formalism you have to be
much more consistent in your design approach.
I did this for the finite state portions of FTP, NNTP and SMTP in 1993
when I was working on HTTP. With HTTP at the time there was not a
lot of
state.
-----Original Message-----
From: Steve Crocker [mailto:steve@xxxxxxxxxxxx]
Sent: Thursday, November 17, 2005 11:28 AM
To: Hallam-Baker, Phillip
Cc: Steve Crocker; Masataka Ohta; Yaakov Stein;
ietf@xxxxxxxx; Stewart Bryant
Subject: Re: Diagrams (Was RFCs should be distributed in XML)
Phillip,
I spent a large fraction of my professional life in pursuit
of this alluring and seemingly simple goal. Here's a small
challenge: Take
*any* IETF protocol and write down the formal specification.
Never mind the proof of correctness; that can come later.
(And with it an extended discussion of the underlying logical
system, the formal system for representing the protocol
specification, and the proof system you have in mind for
carrying out the proof.) Of course, the formal specification
will have to be readable and understandable to the general
population, and there will have to ready agreement that
it does embody the desired properties. Pick something simple.
Perhaps IP? Feel free to leave out messy details like
performance issues if you wish. Just something simple and
instructive to make your point. And in light of the other
issues being discussed, don't feel constrained to use ASCII.
Use any notation and tools you like.
Steve
Steve Crocker
steve@xxxxxxxxxxxx
On Nov 17, 2005, at 10:09 AM, Hallam-Baker, Phillip wrote:
If we want to enforce simpler, more accurate design the
best way to do
this would be to require a formal proof of correctness before
accepting a specification.
Requiring people to use 1960s technology is not a way to achieve
simplicity.
-----Original Message-----
From: ietf-bounces@xxxxxxxx [mailto:ietf-bounces@xxxxxxxx]
On Behalf
Of Masataka Ohta
Sent: Thursday, November 17, 2005 8:30 AM
To: Yaakov Stein
Cc: ietf@xxxxxxxx; Stewart Bryant
Subject: Re: Diagrams (Was RFCs should be distributed in XML)
Yaakov Stein wrote:
It's good that protocols needing more than 72 ASCII
characters are
forbidden.
Just imagine what elegantly simple protocols we would have if we
required the descriptions to be in Morse code.
Good idea.
It's a better approach to enforce much simpler protocols.
Masataka Ohta
_______________________________________________
Ietf@xxxxxxxx
https://www1.ietf.org/mailman/listinfo/ietf
_______________________________________________
Ietf@xxxxxxxx
https://www1.ietf.org/mailman/listinfo/ietf
_______________________________________________
Ietf@xxxxxxxx
https://www1.ietf.org/mailman/listinfo/ietf