增加不變量 [tla-0002]

在有了這些程式之後，可以開始增加自己的不變量

Even(x) == x % 2 = 0

IsInc == x >= 0

Inv == IsInc /\ Even(x)
THEOREM Terminated == Spec => Termination

1. IsInc 要求 x 總是大於初始值 0
2. Even(x) 要求我們寫的程式只會產生偶數
3. Inv 把所有我們想證明的不變量組合在一起，/\ 表示邏輯的「a 且 b」語句。我想很容易猜到 \/ 表示邏輯的「a 或 b」語句

THEOREM 部分宣告 Spec 蘊含 Termination 不變量，這兩者都是 PlusCal 產生的，所以不用太在意細節，這裡的意義是證明程式確實會終止。