SIMPLE PROTOCOL WHOSE PROOF ISN'T.

Abstract

Aho, Ullman, and Yannakakis have proposed a set of protocols that ensure reliable transmission of data across an error-prone channel. They have obtained lower bounds on the complexity required of the protocols to assure reliability for different classes of errors. They specify these protocols with finite-state machines. Although the protocol machines have only a small number of states, they are nontrivial to prove correct. This paper present proofs of one of these protocols using the finite-state-machine approach and the abstract-program approach. It also shows that the abstract-program approach gives special insight into the operation of the protocol.