Issue No. 04 - April (1993 vol. 19)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/32.223804
<p>Flush channels generalize conventional asynchronous communication constructs such as virtual circuits and datagrams. They permit the programmer to specify receipt-order restrictions on a message-by-message basis, providing an opportunity for more concurrency in a distributed program. A Hoare-style partial correctness verification methodology for distributed systems which use flush channel communication is developed, and it is shown that it it possible to reason about such systems in a relatively natural way.</p>
flush channels; asynchronous communication constructs; virtual circuits; datagrams; receipt-order restrictions; message-by-message basis; concurrency; distributed program; Hoare-style partial correctness verification methodology; distributed processing; program verification
P. Kearns, M. Ahuja and T. Camp, "Proof Rules for Flush Channels," in IEEE Transactions on Software Engineering, vol. 19, no. , pp. 366-378, 1993.