比起直接寫出 Spec 等不變式，先寫 PlusCal language (https://lamport.azurewebsites.net/tla/tutorial/intro.html) 的程式再使用用它生成的 Spec 不變量會更簡單也更實用。因為 TLA+ 會嘗試生成所有可能的狀態，有可能出現所謂的 unbound model (https://learntla.com/topics/unbound-models.html)，就結果而言對它進行檢查永遠不會完成。用 PlusCal 語言寫的程式相對容易發現這種錯誤。

---- MODULE plustwo ----
EXTENDS Integers

CONSTANT Limit

(* --algorithm plustwo
variables x = 0;
begin
    while x < Limit do
        x := x + 2;
    end while;
end algorithm; *)
\* BEGIN TRANSLATION (chksum(pcal) = "3f62e9ff" /\ chksum(tla) = "239a9ecd")
\* END TRANSLATION
=====

由 PlusCal 產出的不變量會被包在 BEGIN TRANSLATION 到 END TRANSLATION 裡面，可以發現它還會檢查 checksum。由於這個區塊內的程式會被機器生成的內容覆蓋，因此千萬不要把自己寫的不變量放在這個區塊中。

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

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 產生的，所以不用太在意細節，這裡的意義是證明程式確實會終止。