2.5 证明方法

对同步网络系统做出推断的最重要方法是对不变式断言的证明。一个不变式断言是指系统状态（尤其是所有进程的状态）的一个属性，该属性在每一轮之后的每次运行中都成立。我们允许在断言中提到已完成的轮数，这样就可以声明每次r轮之后的状态。同步系统的不变式断言一般通过对已完成的轮数r的归纳来证明，从r=0开始。

另一个重要的方法是模拟。粗略地说，其目的是表明一个同步算法A“实现”了另外一个同步算法B，即两者产生相同的输入/输出行为。当两个算法从相同的输入开始，在相同的轮数中出现相同的故障形式时，A和B之间的对应关系用与A和B的状态相关的断言来表述。这样的断言被称为模拟关系。与不变式断言相似，模拟关系一般通过对已完成的轮数的归纳来证明。