●出版者的話
譯者序
前言
致謝
第一部分入門
第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.4TLA+規約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有界FIFO28
4.5我們在定義什麼30
第5章緩存示例31
5.1內存接口31
5.2函數33
5.3可線性化內存繫統35
組也是函數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.6CHOOSE54
第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.4Zeno規約100
9.5混合繫統規約102
9.6關於實時103
第10章組合規約104
10.1雙規約的組合104
10.2多規約的組合107
10.3FIFO109
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.4BNF語法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.1TLC介紹174
14.2TLC的應用範圍181
14.2.1TLC值181
14.2.2TLC如何計算表達式182
14.2.3賦值與代換184
14.2.4計算時態公式186
14.2.5模塊覆蓋187
14.2.6TLC如何計算狀態187
14.3TLC如何檢查屬性190
14.3.1模型檢查模式190
14.3.2仿真模式192
14.3.3視圖和指紋192
14.3.4利用對稱性193
14.3.5活性檢查的195
14.4TLC模塊196
14.5TLC的用法198
14.5.1運行TLC198
14.5.2調試規約200
14.5.3如何高效使用TLC204
14.6TLC不能做什麼207
14.7附加說明208
14.7.1配置文件語法208
14.7.2TLC值的可比性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.3TLA+的詞素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.5LET/IN構造240
16.1.6集合運算符240
16.1.7函數242
16.1.8記錄245
16.組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.1Sequences模塊276
18.2FiniteSets模塊277
18.3Bags模塊277
18.4關於數字的模塊279
第五部分TLA+版本2基礎
第19章TLA+版本2286
19.1簡介286
19.2遞歸運算符定義286
19.3LAMBDA表達式288
19.4定理與假設288
19.4.1命名288
19.4.2ASSUME/PROVE289
19.5實例化290
19.5.1實例化詞綴運算符290
19.5.2Leibniz運算符和實例化291
19.6命名子表達式292
19.6.1標簽和帶標簽的子表達式名稱292
19.6.2位置相關的子表達式名稱294
19.6.3LET定義中的子表達式297
19.6.4ASSUME/PROVE的子表達式297
19.6.5將子表達式名稱用作運算符298
19.7證明的語法298
19.7.1證明的結構298
19.7.2USE、HIDE與BY300
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.2ASSUME/PROVE的含義312
19.8.3時態證明312

本書繫統介紹了形式化建模語言TLA+以及模型檢查工具TLC，並結合若干案例，深入淺出地描述了從數學原理到繫統建模的哲學思想，以及從建模語言的工程實踐到模型驗證工具的運用技巧等內容。本書分為五個部分。第一部分包含大多數程序員和工程師需要了解的有關編寫繫統規約（即建立模型）的所有信息；第二部分包含更高級的示例與材料，供需要進階的讀者使用；第三部分和第四部分為TLA+的參考手冊，包括語言本身的數學定義及工具的原理與使用；第五部分介紹在基礎TLA+上所演進出的TLA+版本2的新特性和少許變更。本書適合高級軟硬件開發設計人員、測試人員、架構師以及相關學術研究人員閱讀。