This paper presents and advocates a method for formally specifying and verifying distributed programs. The method, which is based on the partial order of local states generated during execution, avoids the notion of time or physical global state. Programs are specified by documenting the relationship between states which are adjacent to each other in the partial order. Program properties are proven using induction on the happens-before relation and its complement. The technique is illustrated by specifying and proving Lamport's algorithm for mutual exclusion.
展开▼
