用TLA+定義系統：TLA+語言與工具在軟硬件設計中的應用 Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engine

本書是作者針對分佈式並發計算系統超過25年的研究成果的總結。
在本書中，作者提出用基於動作的時態邏輯（TLA）來為複雜信息系統的行為建立數學模型，
進而使用嚴格的數學證明與檢驗的方法來驗證系統行為的正確性。
為此，作者發明了建模語言TLA+以及模型檢查工具TLC。
本書結合若干案例，深入淺出地描述了從數學原理到系統建模的哲學思想，
以及從建模語言的工程實踐到模型驗證工具的運用技巧等內容。

萊斯利·蘭伯特（Leslie Lamport） 微軟研究院的首席研究員，2013年圖靈獎得主，美國國家科學院和國家工程院院士，LaTeX系統創始人。
他是擁有傑出貢獻和輝煌成就的計算機大師、分佈式系統領域的先鋒人物，他的分佈式計算理論奠定了計算機學科的基礎。
他於1978年發表的論文“Time, Clocks, and the Ordering of Events in a Distributed System”至今仍保持著計算機科學史上的被引用量紀錄。

目錄

出版者的話
譯者序
前言
致謝
第一部分入門
第1章簡單數學基礎2
1.1命題邏輯2
1.2集合4
1.3謂詞邏輯4
1.4公式與陳述句6

第2章定義一個簡單時鐘7
2.1行為7
2.2時鐘7
2.3解讀規約9
2.4 TLA+規約10
2.5規約的另一種寫法12

第3章異步接口示例13
3.1第一個規約14
3.2另一個規約17
3.3類型回顧18
3.4定義19
3.5註釋20

第4章FIFO接口示例23
4.1內部規約23
4.2剖析實例化25
4.2.1實例化是一種代換25
4.2.2參數化的實例化26
4.2.3隱式代換26
4.2.4不需重命名的實例化27
4.3隱藏內部變量27
4.4有界FIFO 28
4.5我們在定義什麼30

第5章緩存示例31
5.1內存接口31
5.2函數33
5.3可線性化內存系統35
5.4元組也是函數37
5.5遞歸函數定義38
5.6直寫式緩存39
5.7不變式44
5.8證明實現45

第6章數學基礎拓展47
6.1集合47
6.2 “笨表達式” 48
6.3遞歸回顧49
6.4函數與運算符51
6.5函數使用53
6.6 choose 54

第7章編寫規約：一些建議55
7.1為什麼要編寫規約55
7.2我們要定義什麼55
7.3原子粒度56
7.4數據結構57
7.5編寫規約的步驟57
7.6進一步提示58
7.7定義系統的時機和方法60

第二部分更多高級主題
第8章活性和公平性64
8.1時態公式64
8.2時態重言式68
8.3時態證明規則71
8.4弱公平性71
8.5內存規約75
8.5.1活性要求75
8.5.2換個表示法76
8.5.3推廣80
8.6強公平性81
8.7直寫式緩存82
8.8時態公式量化84
8.9時態邏輯剖析85
8.9.1回顧85
8.9.2閉包85
8.9.3閉包和可能性87
8.9.4轉化映射和公平性87
8.9.5活性不重要89
8.9.6時態邏輯讓人困惑89

第9章實時系統90
9.1回顧時鐘規約90
9.2通用實時規約93
9.3實時緩存96
9.4 Zeno規約100
9.5混合系統規約102
9.6關於實時103

第10章組合規約104
10.1雙規約的組合104
10.2多規約的組合107
10.3 FIFO 109
10.4共享狀態的組合111
10.4.1顯式狀態變化112
10.4.2相交動作的組合114
10.5簡短回顧118
10.5 .1組合方法的分類118
10.5.2審視交錯規約118
10.5.3審視相交動作規約118
10.6活性和隱藏119
10.6.1活性和閉包119
10.6.2隱藏120
10.7開放系統規約121
10.8接口轉化123
10.8.1二進制時鐘123
10.8.2轉化通道125
10.8.3接口轉化推廣128
10.8.4開放系統規約129
10.9規約形式選擇131

第11章高級示例132
11.1定義數據結構132
11.1.1局部定義132
11.1.2圖134
11.1.3求解微分方程137
11.1.4 BNF語法139
11.2其他內存系統的規約145
11.2.1接口146
11.2.2正確性條件147
11.2 .3串行內存系統148
11.2.4順序一致內存系統155
11.2.5對內存規約的思考161

第三部分工具
第12章語法分析器164

第13章TLATEX排版器166
13.1引言166
13.2陰影效果的註釋167
13.3規約排版168
13.4註釋排版168
13.5調整輸出格式170
13.6輸出文件170
13.7故障定位172
13.8使用LATEX命令172

第14章TLC模型檢查器174
14.1 TLC介紹174
14.2 TLC的應用範圍181
14.2.1 TLC值181
14.2.2 TLC如何計算表達式182
14.2.3賦值與代換184
14.2.4計算時態公式186
14.2.5模塊覆蓋187
14.2.6 TLC如何計算狀態187
14.3 TLC如何檢查屬性190
14.3.1模型檢查模式190
14.3.2仿真模式192
14.3.3視圖和指紋192
14.3. 4利用對稱性193
14.3.5活性檢查的限制195
14.4 TLC模塊196
14.5 TLC的用法198
14.5.1運行TLC 198
14.5.2調試規約200
14.5.3如何高效使用TLC 204
14.6 TLC不能做什麼207
14.7附加說明208
14.7.1配置文件語法208
14.7.2 TLC值的可比性209

第四部分TLA+語言
第15章TLA+語法218
15.1簡化語法218
15.2完整的語法226
15.2.1優先級與關聯性226
15.2.2對齊229
15.2.3註釋230
15.2.4時態公式231
15.2.5兩種異常231
15.3 TLA+的詞素232

第16章TLA+的運算符233
16.1恆定運算符233
16.1.1布爾運算符234
16.1.2選擇運算符236
16.1.3布爾運算符的解釋237
16.1.4條件構造239
16.1.5 let/in構造240
16.1.6集合運算符240
16.1.7函數242
16.1.8記錄245
16.1.9元組246
16.1.10字符串247
16.1.11數字248
16.2非恆定運算符249
16.2.1基礎恆定表達式249
16.2.2狀態函數的含義250
16.2.3動作運算符251
16.2.4時態運算符254

第17章模塊的含義257
17.1運算符與表達式257
17.1.1運算符的元數與順序257
17.1.2 λ表達式258
17.1.3簡化運算符應用259
17.1.4表達式260
17.2級別261
17.3上下文263
17.4 λ表達式的含義264
17.5模塊的含義265
17.5.1引入266
17.5.2聲明266
17.5 .3運算符定義267
17.5.4函數定義267
17.5.5實例化267
17.5.6定理與假設269
17.5.7子模塊269
17.6模塊的正確性270
17.7尋找相關模塊270
17.8實例化的語義271

第18章標準模塊276
18.1 Sequences模塊276
18.2 FiniteSets模塊277
18.3 Bags模塊277
18.4關於數字的模塊279

第五部分TLA+版本2基礎
第19章TLA+版本2 286
19.1簡介286
19.2遞歸運算符定義286
19.3 lambda表達式288
19.4定理與假設288
19.4.1命名288
19.4.2 assume/prove 289
19.5實例化290
19.5.1實例化詞綴運算符290
19.5.2 Leibniz運算符和實例化291
19.6命名子表達式292
19.6.1標籤和帶標籤的子表達式名稱292
19.6 .2位置相關的子表達式名稱294
19.6.3 let定義中的子表達式297
19.6.4 assume/prove的子表達式297
19.6.5將子表達式名稱用作運算符298
19.7證明的語法298
19.7.1證明的結構298
19.7.2 use、hide與by 300
19.7.3當前狀態302
19.7.4具有證明的步驟303
19.7.5無證明的步驟306
19.7.6對步驟與其組成部分的引用308
19.7 .7對實例化的定理的引用310
19.7.8時態證明311
19.8證明的語義311
19.8.1布爾運算符的含義311
19.8.2 assume/prove的含義312
19.8.3時態...