这是Leslie Lamport的文章教学并发中的一个简单的并发程序。
考虑N从 0 到N-1每个进程i执行的进程
x[i] := 1
y[i] := x[(i - 1) % N]
并停止，每个x[i]初始等于 0。（每个的读取和写入x[i]都假定是原子的。）
该算法满足以下性质：在每个进程停止后，y[i]至少有一个进程等于 1 i。很容易验证：最后i写入的进程y[i]必须设置为 1。
然后，兰波特评论说
但是该进程没有设置
y[i]为 1，因为它是最后一个 write 进程y。该算法满足此属性，因为它保持一个归纳不变量。你知道那个不变量是什么吗？如果不是，那么您并不完全理解该算法为什么满足此属性。
所以，
并发程序的归纳不变量是什么？
s 模拟以下x行为：当且x[i]仅1当进程i已经运行时。自然，在所有过程完成后，所有xs 都因此设置为1。
ys 有点棘手：y[i]如果已设置则设置x[i-1]，也就是说，当且仅当s的前身在写入时已经运行。y[i]1iiy
程序不变量是：如果一个进程设置了y[i]，它必须已经设置x[i]为1。无论y[i]设置为0还是都是如此1。
证明这个不变量很容易：一开始，没有一个ys 被设置，所以它很容易成立。在程序执行期间，每次写入y[i]都在写入之后进行排序x[i]。因此，该不变量也适用于之后程序的每一步。
进一步的推理是这样的：完成的最后一个过程设置y[i]为1因为根据作为最后一个进程的定义，它的前身必须已经在该点完成执行（即它的y值已经设置）。这意味着，由于不变量，它的x值（它决定了最后一个进程的y值）必须是1.
另一种看待它的方式：您找不到所有ys 都设置为的执行顺序0的执行顺序。这样做将要求所有进程在其前身之前执行。然而，由于我们的进程被安排在一个环中（也就是说，如果我遵循前驱链，我最终将再次回到我的起点），这导致了一个矛盾，即至少一个进程必须在它写入之前完成执行y.
在TLA+语法中，这个程序的一个归纳不变量是：
/\ \A i \in 0..N-1 : (pc[i] \in {"s2", "Done"} => x[i] = 1)
/\ (\A i \in 0..N-1 : pc[i] = "Done") => \E i \in 0..N-1 : y[i] = 1
归纳不变量是满足以下两个条件的不变量：
Init => Inv
Inv /\ Next => Inv'
在哪里：
Inv是归纳不变量Init是描述初始状态的谓词Next是描述状态转换的谓词。请注意，归纳不变量仅与当前状态和下一个状态有关。它没有引用执行历史，它与系统过去的行为无关。
在并发系统的原理和规范（通常称为TLA+ Hyperbook）的第 7.2.1 节中，Lamport 描述了为什么他更喜欢使用归纳不变量而不是行为证明（即那些参考执行历史的证明）。
行为证明可以更正式，但我不知道任何实用的方法可以使它们完全正式——也就是说，编写真实算法的可执行描述和满足正确性属性的正式行为证明。这就是为什么在超过 35 年的并发算法编写过程中，我发现行为推理对于更复杂的算法不可靠的原因之一。我相信另一个原因是，对于足够复杂的算法，行为证明本质上比基于状态的证明更复杂。这导致人们为这些算法编写不太严格的行为证明——尤其是没有完全正式的证明可以作为指导。
为了避免错误，我们必须考虑状态，而不是执行......不过，行为推理提供了一种不同的算法思考方式，思考总是有帮助的。行为推理只有在使用它而不是基于状态的推理而不是作为它的补充时才是不好的。
我们有兴趣证明的属性是（在 TLA+ 语法中）：
(\A i \in 0..N-1 : pc[i] = "Done") => \E i \in 0..N-1 : y[i] = 1
在这里，我使用 PlusCal 约定，使用名为“pc”的变量（我认为它是“程序计数器”）来描述每个进程的控制状态。
这个属性是不变量，但它不是归纳不变量，因为它不满足上述条件。
您可以通过编写如下所示的证明来使用归纳不变量来证明属性：
1. Init => Inv
2. Inv /\ Next => Inv'
3. Inv => DesiredProperty
为了得出一个归纳不变量，我们需要给算法的每一步都打上标签，我们称它们为“s1”、“s2”和“Done”，其中“Done”是每个进程的终端状态。
s1: x[self] := 1;
s2: y[self] := x[(self-1) % N]
考虑程序处于执行的倒数第二个（倒数第二个）状态时的状态。
在最后一个执行状态，pc[i]="Done"对于 i 的所有值。在倒数第二个状态中，pc[i]="Done"对于除一个之外的所有 i 值，我们称其为 j，其中pc[j]="s2"。
如果进程 i 处于“完成”状态，则 必须为真x[i]=1，因为该进程必须已执行语句“s1”。类似地，处于状态“s2”的进程 j 肯定也执行了语句“s1”，所以 一定是真的x[j]=1。
我们可以将其表示为一个不变量，它恰好是一个归纳不变量。
\A i \in 0..N-1 : (pc[i] \in {"s2", "Done"} => x[i] = 1)
为了证明我们的不变量是一个归纳不变量，我们需要一个适当的模型，它有一个
Init状态谓词和一个Next状态谓词。
我们可以从描述PlusCal中的算法开始。这是一个非常简单的算法，所以我称之为“简单”。
--algorithm Simple
variables
x = [i \in 0..N-1 |->0];
y = [i \in 0..N-1 |->0];
process Proc \in 0..N-1
begin
s1: x[self] := 1;
s2: y[self] := x[(self-1) % N]
end process
end algorithm
我们可以将 PlusCal 模型翻译成 TLA+。这是我们将 PlusCal 翻译成 TLA+ 时的样子（我省略了终止条件，因为我们在这里不需要它）。
------------------------------- MODULE Simple -------------------------------
EXTENDS Naturals
CONSTANTS N
VARIABLES x, y, pc
vars == << x, y, pc >>
ProcSet == (0..N-1)
Init == (* Global variables *)
/\ x = [i \in 0..N-1 |->0]
/\ y = [i \in 0..N-1 |->0]
/\ pc = [self \in ProcSet |-> "s1"]
s1(self) == /\ pc[self] = "s1"
/\ x' = [x EXCEPT ![self] = 1]
/\ pc' = [pc EXCEPT ![self] = "s2"]
/\ y' = y
s2(self) == /\ pc[self] = "s2"
/\ y' = [y EXCEPT ![self] = x[(self-1) % N]]
/\ pc' = [pc EXCEPT ![self] = "Done"]
/\ x' = x
Proc(self) == s1(self) \/ s2(self)
Next == (\E self \in 0..N-1: Proc(self))
\/ (* Disjunct to prevent deadlock on termination *)
((\A self \in ProcSet: pc[self] = "Done") /\ UNCHANGED vars)
Spec == Init /\ [][Next]_vars
=============================================================================
注意它是如何定义Init和 Next状态谓词的。
我们现在可以指定要证明的归纳不变量。我们还希望我们的归纳不变量暗示我们有兴趣证明的属性，因此我们将其添加为合取。
Inv == /\ \A i \in 0..N-1 : (pc[i] \in {"s2", "Done"} => x[i] = 1)
/\ (\A i \in 0..N-1 : pc[i] = "Done") => \E i \in 0..N-1 : y[i] = 1
Init => Inv为什么这是真的应该很明显，因为Inv如果为真，则其中的前件都是假Init的。
Inv /\ Next => Inv'(\A i \in 0..N-1 : (pc[i] \in {"s2", "Done"} => x[i] = 1))'
有趣的情况是对于某些 i的地方pc[i]="s1"和情况。pc'[i]="s2"根据 的定义s1，应该清楚为什么这是真的。
((\A i \in 0..N-1 : pc[i] = "Done") => \E i \in 0..N-1 : y[i] = 1)'
有趣的情况是我们之前讨论过的情况，pc[i]="Done"对于 i 的所有值，除了一个 j，其中pc[j]="s2".
通过 Inv 的第一个合取，我们知道x[i]=1对于 i 的所有值。
由s2, y'[j]=1.
Inv => DesiredProperty在这里，我们想要的属性是
(\A i \in 0..N-1 : pc[i] = "Done") => \E i \in 0..N-1 : y[i] = 1
请注意，我们刚刚将我们感兴趣的属性与不变量相加，因此证明这一点很简单。
您可以使用TLA+ 证明系统(TLAPS) 编写正式证明，可以通过机械方式检查以确定其是否正确。
这是我使用 TLAPS 编写和验证的证明，它使用归纳不变量来证明所需的属性。（注意：这是我使用 TLAPS 编写的第一个证明，所以请记住这是由新手编写的）。
AtLeastOneYWhenDone == (\A i \in 0..N-1 : pc[i] = "Done") => \E i \in 0..N-1 : y[i] = 1
TypeOK == /\ x \in [0..N-1 -> {0,1}]
/\ y \in [0..N-1 -> {0,1}]
/\ pc \in [ProcSet -> {"s1", "s2", "Done"}]
Inv == /\ TypeOK
/\ \A i \in 0..N-1 : (pc[i] \in {"s2", "Done"} => x[i] = 1)
/\ AtLeastOneYWhenDone
ASSUME NIsInNat == N \in Nat \ {0}
\* TLAPS doesn't know this property of modulus operator
AXIOM ModInRange == \A i \in 0..N-1: (i-1) % N \in 0..N-1
THEOREM Spec=>[]AtLeastOneYWhenDone
<1> USE DEF ProcSet, Inv
<1>1. Init => Inv
BY NIsInNat DEF Init, Inv, TypeOK, AtLeastOneYWhenDone
<1>2. Inv /\ [Next]_vars => Inv'
<2> SUFFICES ASSUME Inv,
[Next]_vars
PROVE Inv'
OBVIOUS
<2>1. CASE Next
<3>1. CASE \E self \in 0..N-1: Proc(self)
<4> SUFFICES ASSUME NEW self \in 0..N-1,
Proc(self)
PROVE Inv'
BY <3>1
<4>1. CASE s1(self)
BY <4>1, NIsInNat DEF s1, TypeOK, AtLeastOneYWhenDone
<4>2. CASE s2(self)
BY <4>2, NIsInNat, ModInRange DEF s2, TypeOK, AtLeastOneYWhenDone
<4>3. QED
BY <3>1, <4>1, <4>2 DEF Proc
<3>2. CASE (\A self \in ProcSet: pc[self] = "Done") /\ UNCHANGED vars
BY <3>2 DEF TypeOK, vars, AtLeastOneYWhenDone
<3>3. QED
BY <2>1, <3>1, <3>2 DEF Next
<2>2. CASE UNCHANGED vars
BY <2>2 DEF TypeOK, vars, AtLeastOneYWhenDone
<2>3. QED
BY <2>1, <2>2
<1>3. Inv => AtLeastOneYWhenDone
OBVIOUS
<1>4. QED
BY <1>1, <1>2, <1>3, PTL DEF Spec
请注意，在使用 TLAPS 的证明中，您需要有一个类型检查不变量（它在TypeOK上面被称为），并且您还需要处理没有任何变量发生变化的“口吃状态”，这就是我们使用[Next]_vars而不是Next.
这是完整模型和证明的要点。