Subject: Re: running code vs. formal testing methods

From: Graham Klyne <[email-masked]>
Date: Mon, 02 Aug 1999 14:27:13 +0100

At 17:42 31/07/99 -0600, Marshall Rose wrote: 
>look at the number of standards-track rfcs that have  progressed past the
proposed level. i think you would be hard-pressed to find a  comperable
number of real-world protocols specified and validated using formal
methods.  history is pretty clear that the way to get success in the
protocol arena is to focus on well-written natural-language  specifications
iteratively developed with multiple interoperable  inplementations.  /mtr 

I think it's worth noting that there is SOME track record of formal
specification in RFCs -- the one that first comes to mind is ABNF.  On the
semantic front, RFC 821 uses state diagrams to describe key aspects of
processing semantics.

My point:  this isn't a black-and-white issue.  Some formal techniques have
a track record of demonstrated success (a kind of meta-running-code?).

I think the winning techniques tend to be those that address a well-focused
problem rather than attempt to solve all specification issues.  Maybe this
is the IETF culture at work:  progressing by incremental well-understood
steps rather than trying to digest the problem whole?

#g

------------
Graham Klyne
([email-masked])

---

From: Dave Crocker <[email-masked]>
Date: Mon, 02 Aug 1999 07:18:34 -0700

>a track record of demonstrated success (a kind of meta-running-code?).

The core issue is that the IETF lets working groups decide on the level and 
nature of technical specification formality it needs to achieve its goal.

But the requirement for "Draft Standard" status is explicitly about 
interoperability testing, not conformance testing.  That's a formal point 
about informal methods of proving the specification.  (We don't have 
anything at all to do with certifying implementations.)

>steps rather than trying to digest the problem whole?

yup.

d/

=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
Dave Crocker                                         Tel: +1 408 246 8253
Brandenburg Consulting                               Fax: +1 408 273 6464
675 Spruce Drive                             <http://www.brandenburg.com>
Sunnyvale, CA 94086 USA                 <mailto:[email-masked]>

---

From: Dave Crocker <[email-masked]>
Date: Mon, 02 Aug 1999 07:18:34 -0700

yup.

d/

---

From: Jacob Palme <[email-masked]>
Date: Mon, 2 Aug 1999 19:00:02 +0200

>semantic front, RFC 821 uses state diagrams to describe key aspects of

XML has a validator service. If you specify your protocols using XML, 
then you can validate test examples against the specified syntax in 
the XML DTD. This has some similarities to validating ABNF. However, 
both ABNF and XML are limited in what they can check. In XML, I can 
specify that a certain attribute must have one of a list of allowed 
values (so-called enumerated) which is very useful, but I can not 
specify that a certain attribute must be numerical, which is possible 
with ABNF. And they will certainly only check some of your syntax, 
not your semantics.

A problem with ABNF is that there are different dialects of it, you 
can only use a validator if you are using the same dialect of ABNF as 
the validator.

I have tried XML (http://www.stg.brown.edu/service/xmlvalid/) and 
HTML validators (http://validator.w3.org/) available on the net, they 
are very useful. Are there ABNF validators on the net?
------------------------------------------------------------------------
Jacob Palme <[email-masked]> (Stockholm University and KTH)
for more info see URL: http://www.dsv.su.se/~jpalme

---

From: Jacob Palme <[email-masked]>
Date: Mon, 2 Aug 1999 19:00:02 +0200