An Assertional Correctness Proof of a Distributed Program

I showed in [27] that there is no invariant way of defining the global state of a distributed system. Assertional methods, such as [23], reason about the global state. So, I concluded that these methods were not appropriate for reasoning about distributed systems. When I wrote this paper, I was at SRI and partly funded by a government contract for which we had promised to write a correctness proof of a distributed algorithm. I tried to figure out how to write a formal proof without reasoning about the global state, but I couldn’t. The final report was due, so I decided that there was no alternative to writing an assertional proof. I knew there would be no problem writing such a proof, but I expected that, with its reliance on an arbitrary global state, the proof would be ugly. To my surprise, I discovered that the proof was quite elegant. Philosophical considerations told me that I shouldn’t reason about global states, but this experience indicated that such reasoning worked fine. I have always placed more reliance on experience than philosophy, so I have written assertional proofs of distributed systems ever since. (Others, more inclined to philosophy, have spent decades looking for special ways to reason about distributed systems.)