介紹
對于一套系統(tǒng)的設(shè)計盐股，通常我都是想好了，然后直接捋起袖子寫代碼了耻卡。寫完了疯汁，在開始加很多 test 來保證它的正確性。但其實卵酪，我并不能保證設(shè)計是完全正確的幌蚊。也就是說谤碳，我的實現(xiàn)滿足了該系統(tǒng)的需求，但也有可能在一些 corner case 上面并沒有考慮周全溢豆。同時蜒简， 雖然后面可以寫很多 test，但并不一定能 cover 到所有的分支漩仙。所以搓茬，為了更好的確保設(shè)計的正確性，我們需要使用 TLA+ 或者其他類似的工具队他。
TLA+ 是一門形式規(guī)格說明語言(formal specification language)卷仑，主要用來驗證系統(tǒng)的設(shè)計和算法的正確性。TLA+ 是大神 Lamport 搗鼓出來的東西麸折，關(guān)于大神 Lamport锡凝，這里就不多做介紹了，反正就是 NB 的一塌糊涂了垢啼。
TLA+ 是對系統(tǒng)（譬如程序窜锯，算法，操作系統(tǒng)等）更高層的建模芭析，但 TLA+ 并不能生產(chǎn)任何代碼锚扎。對于很多程序員來說，首要直覺這是這玩意到底有啥用放刨？TLA+ 可以認為是一種新的思考方式工秩，是在代碼之上更上層的規(guī)格說明尸饺。通過 TLA+ 來設(shè)計系統(tǒng)进统，能讓我們更好的對整個系統(tǒng)進行抽象。
抽象
抽象對于程序員來說浪听，可能是最重要的一個能力螟碎。通過抽象，能然我們更好的理解復(fù)雜的系統(tǒng)迹栓，如果我們不能對一個系統(tǒng)進行抽象掉分，我們并不能正確的理解這個系統(tǒng)。悲催的是克伊，我個人認為我自己還需要提高這方面的能力酥郭，正好，可以通過學(xué)習(xí) TLA+ 來提高愿吹。因為對于學(xué)習(xí) TLA+ 來說不从，最難的部分就是對系統(tǒng)進行抽象。
對于 TLA+ 來說犁跪，一個系統(tǒng)的執(zhí)行其實可以表示為一個離散步驟序列（A sequence of discrete steps）椿息。這里我們主要關(guān)注三個東西歹袁。
- Discrete：對于一個連續(xù)演化的系統(tǒng)，我們可以抽象為一系列的離散事件寝优。譬如条舔，對于一個時鐘來說，雖然時間的流逝是連續(xù)的乏矾，但我們可以抽象為每次按照一個離散的 tick 前進的孟抗。
- Sequence：對于一個并行的系統(tǒng)來說，我們能使用一個步驟序列來表示钻心。雖然這看起來很奇怪夸浅，但實際上我們我們是能夠用一個序列程序來模擬并發(fā)系統(tǒng)的。
- Step：TLA+ 描述一個 step 就是一個狀態(tài)變更扔役。一次執(zhí)行可以表示為一個狀態(tài)序列帆喇，而一個 step 就是從一個狀態(tài)切換到另一個狀態(tài)。對于一個狀態(tài)來說亿胸，就是給一些變量賦值坯钦。
狀態(tài)機
對于一個系統(tǒng)來說，TLA+ 會將其抽象為狀態(tài)機侈玄。一個狀態(tài)機可以被如下描述：
- 所有可能的初始狀態(tài)
- 對于任意狀態(tài)婉刀，后面的狀態(tài)是什么
因為我們在上面說過，狀態(tài)就是一次對變量的賦值序仙，所以我們繼續(xù)做如下描述：
- 變量是什么
- 變量的所有可能初始值
- 在當(dāng)前狀態(tài)下這些變量的值以及在下一個狀態(tài)下這些變量的可能的值之間的關(guān)系
這個聽起來有點繞突颊，我們可以用一個簡單的 C 例子（先別糾結(jié) main 前面的 void）來說明：
int i;
void main() {
i = someNumber();
i = i + 1;
}
這里 someNumber() 會隨機返回 0 到 1000 里面的一個數(shù)值。所以對于不同的返回值潘悼，我們其實有不同的執(zhí)行律秃。
這里，我們就一個變量治唤，也就是 i棒动，假設(shè) someNumber() 返回 42，那么一個執(zhí)行就是 [i : 0] -> [i : 42] -> [i: 43]宾添。我們先按照狀態(tài)機來描述這個例子：
- 變量船惨，也就是 i
- 初始值，這里就是 0
- 當(dāng)前狀態(tài) i 的值和下一個狀態(tài) i 的可能值之間的關(guān)系缕陕。
上面最后 i 為 43 之后粱锐，下一個狀態(tài)并沒有值，因為程序結(jié)束了扛邑。但如果 someNumber() 返回 43怜浅，那么整個執(zhí)行就是 [i : 0] -> [i : 43] -> [i: 44]，在 43 之后鹿榜，下一個狀態(tài)的值是 44海雪。所以對于當(dāng)前狀態(tài) 43 來說锦爵，我們在下一個狀態(tài)會有不同的值，這是不可能的奥裸。也就是說险掀，我們不能只通過一個 i 變量來將這個程序描述成狀態(tài)機。
這里湾宙，我們引入另一個變量樟氢，pc（program control），作為一個控制狀態(tài)侠鳄。對于上面例子埠啃，現(xiàn)在就是兩個變量 i 和 pc。初始值 i 為 0伟恶，pc 為 “start”碴开。當(dāng)?shù)谝粭l語句執(zhí)行之后，pc 為 “middle”博秫，而程序結(jié)束的時候潦牛，pc 為 “done”。那么我們現(xiàn)在可以描述兩個狀態(tài)之間的關(guān)系了：
- 如果當(dāng)前 pc 值為 “start”挡育，那么 i 的下一個值就是在
{0, 1, …, 1000}里面的一個值巴碗，pc 就是 “middle” - 如果當(dāng)前 pc 值為 “middle”，那么 i 的下一個值就是當(dāng)前 i 的值加 1即寒， pc 就是 “done”
- 否則沒有下一個值
Math
我們現(xiàn)在開始嘗試用數(shù)學(xué)的方式來描述上面的狀態(tài)機橡淆。我們定義 pc 和 i 分別為當(dāng)前值，而下一個狀態(tài)的值為 pc’ 和 i’母赵。我們可以從一個偽代碼開始逸爵，然后開始逐漸用 TLA+ 來描述。
if pc = "start"
then i' in {0, 1, ..., 1000}
pc' = "middle"
else if pc = "middle"
then i' = i + 1
pc' = "done"
else no next values
這里需要注意市咽，= 在數(shù)學(xué)里面是相等的意思痊银，類似 2 + 2 = 4抵蚊，并不是通常程序里面的賦值的意思施绎。
{0, 1, ..., 1000} 是一個集合，我們可以使用 0..1000 來表示贞绳，in 在集合里面是 ∈谷醉，但為了方便輸入，我們直接使用 ASCII 的 \in 來表示冈闭。
對于第一個 then 俱尼，里面有兩個獨立的公式（formula），但 then 這個應(yīng)該是一個單一的公式萎攒，并且斷定里面所有的公式都要為真遇八，所以我們這里可以使用 and 來連接這兩個公式矛绘。我們使用 /\ 來表示。
no next values 也是一個公式刃永，我們直接使用 FALSE 來表示货矮。所以上面可以寫成：
if pc = "start"
then i' \in 0..1000 /\
pc' = "middle"
else if pc = "middle"
then i' = i + 1 /\
pc' = "done"
else FALSE
這里需要注意，我們不能按照程序執(zhí)行的順序思維來思考斯够，也就是說囚玫，如果 pc 為 start，我們就 then 做什么事情读规，不然我們就 else 做什么事情抓督。這個公式應(yīng)該理解為，如果 pc 是 start束亏，那么這個公式的值就等于 then 這個公式的值铃在，否則就是等于 else 這個公式的值。
對于這個公式碍遍，i = 17, pc = "start", i' = 534, pc' = "middle"它的值等于 true涌穆，而對于 i = 534, pc = "middle", i' = 77, pc' = "done" 則是 false。
我們繼續(xù)雀久，對于上面的公式宿稀，返回 true 的情況就是兩種，if pc = "start" /\ (i' \in 0..1000 /\ pc' = "middle") 為 true 或者 if pc = "middle" /\ (i' = i + 1 /\ pc' = "done") 等于 true赖捌。or 我們可以使用 \/ 來表示祝沸，所以上面可以寫成：
((pc = "start)
/\ (i' \in 0..1000)
/\ (pc' = "middle"))
\/ ((pc = "middle")
/\ (i' = i + 1)
/\ (pc' = "done"))
TLA+ 支持符號列表這樣的格式，我們順便去掉括號越庇，繼續(xù)簡化罩锐，得到：
\/ /\ pc = "start
/\ i' \in 0..1000
/\ pc' = "middle"
\/ /\ pc = "middle"
/\ i' = i + 1
/\ pc' = "done"
上面我們對一個簡單的 C 程序重新用 TLA+ 來描述，代碼上面看起來比 C 的復(fù)雜了不少卤唉，但卻能更好的描述系統(tǒng)涩惑。在 C 里面，someNumber() 這個函數(shù)返回值是不確定的桑驱，我們并不能很好的對不確定的系統(tǒng)進行描述的竭恬。但使用 TLA+ 卻非常方便，在上面的例子里面我們直接使用數(shù)學(xué)集合來描述熬的。
這里我們需要注意痊硕，我們通過 TLA+ 來思考的是一個公式，并不是程序命令執(zhí)行的序列押框。所以一定要用數(shù)學(xué)的方式來思考整個系統(tǒng)岔绸，這點恰恰是對程序員來說最困難的一點，畢竟要轉(zhuǎn)換之前的設(shè)計思路。后面我們會先介紹一下 TLA+ 相關(guān)的數(shù)學(xué)知識盒揉。
小結(jié)
TLA+ 是一門非常強大的語言晋被，它在系統(tǒng)設(shè)計上面能讓我們更好的對系統(tǒng)進行抽象，然后驗證設(shè)計的正確性刚盈。
上面介紹的是 Lamport 的 TLA+ 視頻第一章的學(xué)習(xí)筆記墨微。實話，個人還沒有完全理解狀態(tài)機這些東西扁掸，畢竟它的思考模式跟傳統(tǒng)的程序語言完全不一樣翘县。
后面，我會開始逐漸學(xué)習(xí) TLA+谴分，最終目標是將我們系統(tǒng)里面的一些關(guān)鍵模塊锈麸，譬如分布式事務(wù)這些，使用 TLA+ 進行驗證牺蹄。
