21-Jul-95 22:38:36-GMT,2574;000000000001
Received: by watsun.cc.columbia.edu id AA22693
(5.65c+CU/IDA-1.4.4/HLK for fdc); Fri, 21 Jul 1995 18:38:35 -0400
Date: Fri, 21 Jul 1995 18:38:35 -0400
From: Frank da Cruz
Message-Id: <199507212238.AA22693@watsun.cc.columbia.edu>
To: fdc@watsun.cc.columbia.edu
Path: news.columbia.edu!panix!news.mathworks.com!newshost.marcam.com!zip.eecs.umich.edu!news-server.eecs.umich.edu!huggins
From: huggins@tarski.eecs.umich.edu (James K. Huggins)
Newsgroups: comp.protocols.kermit.misc
Subject: Kermit Proof of Correctness Available
Followup-To: comp.protocols.kermit.misc
Date: 21 Jul 1995 20:10:18 GMT
Organization: University of Michigan EECS Dept., Ann Arbor, MI
Lines: 38
Distribution: world
Message-ID:
NNTP-Posting-Host: tarski.eecs.umich.edu
In his preface to Frank da Cruz's book Kermit: A File Transfer
Protocol, Don Knuth wrote:
I hope that many readers of this book will be challenged to find
high-level concepts and invariant relations by which various
versions of the Kermit protocol can be proved correct in a
mathematical sense.
I'm pleased to announce that such a proof has recently been completed.
The proof gives a complete specification of the core Kermit file
transfer protocol, and shows that it is both safe (if you get a file,
you can be sure it's the one that was sent) and live (if you send
a file, and the network isn't too bad, it gets to the other end).
The proof (written by myself) appears as part of a new book,
"Specification and Validation Methods", edited by Egon Boerger
and available through Oxford University Press (ISBN 0-19-853854-5,
official publishing date 3 August 1995).
Thanks to the good folks at Oxford University Press, as well as Frank
da Cruz at Columbia, the Kermit proof has been made available
as part of the Kermit repository at Columbia University. Those of
you with WWW access can find the cover page for the proof, including
more detailed information on the book containing the proof, at
http://www.columbia.edu/kermit/proof.html
The proof itself (in PostScript) is available via anonymous FTP as
ftp://kermit.columbia.edu/kermit/e/proof.ps
As the author of the proof, I'd be happy to hear any comments or
questions you might have about the proof. The proof uses a relatively
new specification methodology known as "evolving algebras"; an
introduction to the method is contained in the proof. I'd be happy
to discuss the technique with anyone who might be interested.
Jim Huggins (huggins@umich.edu)