Using Operational Intuition about Events and Causality in Assertional Proofs

There are two approaches to reasoning about distributed algorithms. In the operational approach, one reasons "dynamically" about the events that can occur and the temporal precedence relation (called causality) between those events. In the assertional approach, one reasons "statically" about reachable states by means of assertions (called invariants) that are true for all reachable states. The purpose of this paper is to show that the operational and assertional approaches can be combined in such a way that the advantages of both approaches are attained. On the one hand, operational reasoning about events and causality affords an intuitive way to think about and understand distributed algorithms. On the other hand, assertional proof techniques allow such intuitive understanding to be used to guide and structure formal correctness proofs. By combining these two approaches, the difficult task of verifying distributed algorithms is made easier. It is also shown that the notions of ev..