Towards a practitioners' approach to Abadi and Lamport's method
Kai Engelhardt, Willem Paul de Roever · Formal Aspects of Computing · 1995
Abstract Our own basic intuitions are presented when introducing the method developed by Abadi and Lamport in [AbL88a] for proving refinement between specifications of nondeterministic programs correct to people unacquainted with it. The example we use to illustrate this method is a nontrivial communication protocol that provides a mechanism analogous to message passing between migrating processes within a fixed finite network of nodes due to Kleinman, Moscowitz, Pnueli and Shapiro [KMP91]. Especially the cruel last step of a three step refinement proof of that protocol gives rise to a deeper understanding of, and some small enhancements to, Abadi and Lamport's 1988 method.