Like live polio vaccine there tends to be a prophilactic effect that has
Although formal methods were not used in the design of Java and were not
part of the design of C# as far as I am aware, both languages were
designed after the field of software language development had spent a
great deal of time working on ways to prove the correctness of the
language features they incorporate.
The principle advantage to formal methods thus far appears to be
pedagogical, once you have tried to prove large stringy ugly systems
correct you start to see more of an advantage to starting with something
I am sure that there are other people who work on IETF protocols that go
through the process of producing proof sketches as part of their design
work. As for sharing them more widely, lets start with the low hanging
fruit like using clear typography...
Behalf Of Harald Tveit Alvestrand
Sent: Thursday, November 17, 2005 1:35 PM
To: Frank Ellermann; ietf(_at_)ietf(_dot_)org
Subject: Re: Diagrams
I remember that when the ITU-T was pushing for more use of
formal tools in its IETF cooperation, around the London
timeframe (2001), one person wrote a formal definition of
OSPF in one of their formalisms.
I don't remember if he found any problems in the spec based
on that exercise, but people more intimately connected to
this problem space may remember more.
--On 17. november 2005 17:59 +0100 Frank Ellermann
Steve Crocker wrote:
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.
Do you expect Phil's reply before 2007 ? There were some
SDL-tools about fifteen years ago. Bye, Frank
Ietf mailing list
Ietf mailing list