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)