TLA+ 并不是一門很容易掌握的語(yǔ)言，在學(xué)習(xí)之前蒜魄，我們需要了解一些簡(jiǎn)單的數(shù)學(xué)知識(shí)扔亥。這里需要注意，為了打字方便谈为，很多數(shù)學(xué)符號(hào)我直接使用了 ASCII 來(lái)表示旅挤，具體符號(hào)與 ASCII 的對(duì)應(yīng)，大家可以參考 TLA+ cheat-sheet

算數(shù)

最基本的整數(shù)算數(shù)運(yùn)算包含在 TLA+ 的 Integers module 里面峦阁，主要就是常用的 +谦铃，-，*榔昔，^ 驹闰，% 這些，還包括 >撒会，<嘹朗，>=，<= 等诵肛。

Integers module 同時(shí)定義了：

• Int：所有整數(shù)
• Nat：所有自然數(shù)
• ..：m..n 表示了從 m 到 n 之間的所有整數(shù)集合

對(duì)于 /屹培，則是在 Real module 里面定義了默穴。Real module 也同時(shí)定義了 Real 用來(lái)表示所有的實(shí)數(shù)。

邏輯

在 TLA+ 里面褪秀，TRUE 表示真蓄诽，而 FALSE 則是假。譬如 1 + 1 = 2 的值是 TRUE媒吗，而 1 + 1 = 3 的值是 FALSE仑氛。

命題邏輯

跟整數(shù)有加減乘除運(yùn)算符一樣，布爾也有相關(guān)的命題邏輯運(yùn)算符闸英，我們需要知道如下 5 個(gè)：

• /\：and锯岖，當(dāng)且只有 F 和 G 都等于 TRUE，F /\ G 等于 TRUE
• \/：or甫何，當(dāng)且只有 F 或者 G 一個(gè)等于 TRUE（或者都為 TRUE）出吹，F \/ G 等于 TRUE
• ~：negation，當(dāng)且只有 F 等于 FALSE辙喂，~F 等于 TRUE
• =>：implication捶牢，當(dāng)且只有 F 等于 FALSE 或者 G 等于 TRUE（或者 F 和 G 都為 TRUE 或者 FALSE），F => G 等于 TRUE
• <=>：equivalence加派，當(dāng)且只有 F 和 G 都為 TRUE 或者都為 FALSE叫确，F <=> G 等于 TRUE

這里我們可能對(duì) => 的定義感到困惑跳芳，為什么只有 F 為 TRUE 并且 G 為 FALSE 的時(shí)候 F => G 才為 FALSE芍锦，我們可以通過(guò) (n > 5) => (n > 3) 來(lái)說(shuō)明，對(duì)于整數(shù) n 來(lái)說(shuō)飞盆，如果 n 為 6娄琉，n > 5 就是 TRUE，自然 n > 3 也是 TRUE吓歇，也就是 (n > 5) 蘊(yùn)含著 (n > 3)孽水，我們可以將 n 設(shè)置為 1，4 這些值在自行推導(dǎo)城看。

謂語(yǔ)邏輯

在命題邏輯基礎(chǔ)上女气，謂語(yǔ)邏輯擴(kuò)展了兩個(gè)運(yùn)算符，我們叫做量詞测柠。一個(gè)是全稱量詞 \A炼鞠，另一個(gè)則是存在量詞 \E。對(duì)于公式 \A x \in S: P(x) 來(lái)說(shuō)轰胁，在集合 S 里面所有的 x谒主，P(x) 都必須等于 TRUE，那么該公式值才是 TRUE赃阀。而對(duì)于 \E x \in S: P(x) 來(lái)說(shuō)霎肯，只要 S 里面一個(gè) x 存在 P(x) 等于 TRUE，那么該公式的值就是 TRUE。

CHOOSE

CHOOSE 操作符類似于上面說(shuō)的 \E观游。對(duì)于公式 \E x \in S : P(x) 來(lái)說(shuō)搂捧，如果在集合 S 里面存在一個(gè)值 x，滿足 P(x) 為 TRUE懂缕，那么 CHOOSE x \in S : P(x) 就等于這個(gè)值异旧。

當(dāng)使用 CHOOSE 在集合里面選擇了一個(gè)值之后，每次執(zhí)行都會(huì)使用這個(gè)值提佣，譬如對(duì)于 v' = CHOOSE n \in 1..10 : TRUE 來(lái)說(shuō)吮蛹，我們并不知道 CHOOSE 選擇了哪一個(gè)值，沒(méi)準(zhǔn)是 1拌屏，也沒(méi)準(zhǔn)是 10潮针，但我們能夠確定，每次執(zhí)行都會(huì)是這個(gè)值倚喂。如果我們需要每次使用不同的值每篷，可以通過(guò) \E n \in 1..10 : v' = n 來(lái)設(shè)置。

集合

集合應(yīng)該是 TLA+ 的理論基石端圈，一個(gè)集合可能含有有限或者無(wú)限個(gè)數(shù)的元素焦读。譬如所有自然數(shù)集合就是是一個(gè)無(wú)窮集合。集合主要有以下操作：

• \intersect 或者 \cap：兩個(gè)集合的交集舱权，譬如 {1, 2} \intersect {2, 3} = {2}
• \union 或者 \cup：兩個(gè)集合的并集矗晃，譬如 {1, 2} \union {2, 3} = {1, 2, 3}
• \subseteq：一個(gè)集合是否是另一個(gè)集合的子集，譬如 {1, 3} \subseteq {1, 2, 3} 等于 TRUE
• \：兩個(gè)集合的差集宴倍，譬如 {1, 2, 3} \ {1, 4} = {2, 3}
• SUBSET：集合的子集张症，譬如 {1, 2} 的子集就是 {{}, {1}, {2}, {1, 2}}
• UNION：集合的并集，譬如 {{1, 2}, {2, 3}, {3, 4}} 的并集就是 {1, 2, 3, 4}
• Cardinality(S)：有限集合 S 中元素的個(gè)數(shù)
• IsFiniteSet(S)：驗(yàn)證集合 S 是否是有限的還是無(wú)限的

這里我們?cè)谥攸c(diǎn)關(guān)注兩個(gè)集合的構(gòu)造操作符：

• {x \in S : P(x)}：集合由在 S 中滿足 P(x) 為 TRUE 的元素構(gòu)造鸵贬，譬如 {n \in Nat : n % 2 = 1} 就返回了一個(gè)偶數(shù)集合
• {e(x) : x \in S}：集合由在 S 中元素通過(guò) e(x) 得到新值構(gòu)造俗他，譬如 {2 * n + 1 : n \in Nat} 就返回了一個(gè)奇數(shù)集合

函數(shù)

TLA+ 里面的函數(shù)跟我們程序里面的函數(shù)意義是不一樣的，反倒有點(diǎn)類似于數(shù)組阔逼，這點(diǎn)一定要注意兆衅。

對(duì)于函數(shù)，首先我們需要了解的是值域嗜浮，我們可以認(rèn)為就是程序語(yǔ)言里面數(shù)組的索引集合羡亩，譬如對(duì)于 tuple（一種特殊的函數(shù)來(lái)說(shuō)），DOMAIN <<"a", "b", "c">> 就是一個(gè) 1..3 的集合周伦。

如果 f 是一個(gè)函數(shù)夕春，而 x 是 f 值域里面的一個(gè)元素，f[x] 就表示的將 f 應(yīng)用到 x 上面专挪。對(duì)于上面的 tuple及志，<<"a", "b", "c">>[2] 就會(huì)得到 "b"片排，而 <<"a", "b", "c">>[4] 則會(huì)報(bào)錯(cuò)。

我們可以通過(guò) [x \in S |-> e]構(gòu)造任意值域的函數(shù)速侈，這里仍然先以 tuple 為例率寡， tuple，一種特殊的函數(shù)倚搬，它的值域就是集合 1..n冶共，n 為 tuple 的個(gè)數(shù)。譬如 tuple 可以寫成 [ i \in 1..3 |-> i - 7]每界，這個(gè)就會(huì)得到 tuple <<-6, -5, -4>>捅僵，然后我們可以使用 <<-6, -5, -4>>[1] 得到 -6 了。

我們?cè)賮?lái)看一個(gè)更通用的例子眨层，[i \in {2, 4, 6, 8} |-> i - 42][4] 庙楚，這里我們得到的值是 4 - 42，也就是 38趴樱。

當(dāng)一個(gè)函數(shù) f 的值域在 S馒闷，并且 f[x] 在集合 T 里面，我們就可以用 [S -> T] 來(lái)表示所有這樣函數(shù)的集合叁征。

我們也可以使用 EXCEPT 來(lái)構(gòu)造另一個(gè)函數(shù)纳账，對(duì)于公式 [f EXCEPT ![e1] = e2] 表示新的函數(shù) f’ 等于 f 除了 f'[e1] = e2。我們也可以使用 @ 來(lái)表示 f[e1]捺疼，譬如 f' = [f EXCEPT ![e1] = f[e1] + 1 中疏虫，我們就可以寫成 f' = [f EXCEPT ![e1] = @ + 1

小結(jié)

可以看到，TLA+ 需要的數(shù)學(xué)知識(shí)其實(shí)就是最基本的四則運(yùn)算帅涂，布爾代數(shù)议薪，集合論相關(guān)的尤蛮。當(dāng)然媳友，還有很多運(yùn)算符這里沒(méi)有提到，后面實(shí)際例子的時(shí)候我們繼續(xù)詳細(xì)說(shuō)明产捞。