home *** CD-ROM | disk | FTP | other *** search
/ kermit.columbia.edu / kermit.columbia.edu.tar / kermit.columbia.edu / e / proof.msg < prev    next >
Text File  |  1995-07-20  |  3KB  |  60 lines
  1. 21-Jul-95 22:38:36-GMT,2574;000000000001
  2. Received: by watsun.cc.columbia.edu id AA22693
  3.   (5.65c+CU/IDA-1.4.4/HLK for fdc); Fri, 21 Jul 1995 18:38:35 -0400
  4. Date: Fri, 21 Jul 1995 18:38:35 -0400
  5. From: Frank da Cruz <fdc@watsun.cc.columbia.edu>
  6. Message-Id: <199507212238.AA22693@watsun.cc.columbia.edu>
  7. To: fdc@watsun.cc.columbia.edu
  8.  
  9. Path: news.columbia.edu!panix!news.mathworks.com!newshost.marcam.com!zip.eecs.umich.edu!news-server.eecs.umich.edu!huggins
  10. From: huggins@tarski.eecs.umich.edu (James K. Huggins)
  11. Newsgroups: comp.protocols.kermit.misc
  12. Subject: Kermit Proof of Correctness Available
  13. Followup-To: comp.protocols.kermit.misc
  14. Date: 21 Jul 1995 20:10:18 GMT
  15. Organization: University of Michigan EECS Dept., Ann Arbor, MI
  16. Lines: 38
  17. Distribution: world
  18. Message-ID: <HUGGINS.95Jul21161018@tarski.eecs.umich.edu>
  19. NNTP-Posting-Host: tarski.eecs.umich.edu
  20.  
  21. In his preface to Frank da Cruz's book Kermit: A File Transfer
  22. Protocol, Don Knuth wrote:
  23.  
  24.      I hope that many readers of this book will be challenged to find
  25.      high-level concepts and invariant relations by which various
  26.      versions of the Kermit protocol can be proved correct in a
  27.      mathematical sense.
  28.  
  29. I'm pleased to announce that such a proof has recently been completed.
  30. The proof gives a complete specification of the core Kermit file
  31. transfer protocol, and shows that it is both safe (if you get a file,
  32. you can be sure it's the one that was sent) and live (if you send
  33. a file, and the network isn't too bad, it gets to the other end).
  34.  
  35. The proof (written by myself) appears as part of a new book,
  36. "Specification and Validation Methods", edited by Egon Boerger
  37. and available through Oxford University Press (ISBN 0-19-853854-5,
  38. official publishing date 3 August 1995).  
  39.  
  40. Thanks to the good folks at Oxford University Press, as well as Frank
  41. da Cruz at Columbia, the Kermit proof has been made available 
  42. as part of the Kermit repository at Columbia University.  Those of
  43. you with WWW access can find the cover page for the proof, including
  44. more detailed information on the book containing the proof, at
  45.  
  46.     http://www.columbia.edu/kermit/proof.html   
  47.  
  48. The proof itself (in PostScript) is available via anonymous FTP as
  49.  
  50.     ftp://kermit.columbia.edu/kermit/e/proof.ps      
  51.  
  52. As the author of the proof, I'd be happy to hear any comments or
  53. questions you might have about the proof.  The proof uses a relatively
  54. new specification methodology known as "evolving algebras"; an
  55. introduction to the method is contained in the proof.  I'd be happy
  56. to discuss the technique with anyone who might be interested.
  57.  
  58. Jim Huggins (huggins@umich.edu)
  59.  
  60.