出版者的話
譯者序
前言
致謝
部分 入門
第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組也是函數 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組 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 時態證明312

本書將指導你如何使用TLA 語言編寫計算機繫統規約。全書篇幅比較長，但大多數人隻需要閱讀部分的內容就夠了，這部分包含了大多數工程師需要了解的與編寫規約有關的知識，至於學習它所需要的背景知識，隻要求具備工程學或計算機科學的本科生所應掌握的數學和計算機知識即可。第二部分將為需要進階的讀者提供更深入的內容。本書的其餘部分是參考手冊——第三部分介紹TLA 工具，第四部分介紹TLA 語言本身。
TLA官網http://lamport.org有可供下載的配套資源，包括TLA 工具、練習、參考資料和勘誤清單。你也可以在搜索引擎上輸入uidlamporttlahomepage來找到上述頁面，但請不要把這個字符串放到互聯網上共享。
何為規約
寫作是發現你的想法有多麼草率的根本方法。
——Guindon
規約是“繫統應該做什麼”的書面定義。定義一個繫統有助於我們更好地理解它。在構建繫統之前好先理解該繫統，因此在實現之前先編寫繫統規約是個好主意。
本書講述了繫統的行為屬性，也可稱之為功能屬性或邏輯屬性。這些屬性定義繫統應該做什麼。當然繫統還有其他我們這裡不考慮的重要屬性，比如性能屬性。差情況下的性能通常可以表示為行為屬性，在第9章我們講述了如何定義繫統在一定時間內的行為，不過，本書暫時不考慮如何定義平均性能。
我們編寫規約的基本工具是數學。數學是一門嚴謹的語言，比自然語言（例如英語或中文）更為精準。在工程實踐中，不精準就很容易出錯，因此科學和工程學通常采用數學作為基本語言。
本書用到的數學語言會比你一直使用的數學語言更形式化一些。相對於形式化數學，大多數數學家和科學家在寫作中使用的數學表達方式並不十分精準，應用於小範圍還勉強可以，應用於大範圍則不佳。在非形式化數學語言中，每個方程都是一個精確的斷言，但你必須閱讀方程前後的解釋性文字纔能理解方程之間的關繫以及定理的確切含義。邏輯學家已經研究出了消除這些解釋性文字並使數學更形式化、更精準完備的方法。
大多數數學家和科學家可能認為形式化數學又長又乏味，這是不對的，普通數學也可以用一種精準完備的形式化語言來簡潔表達。例如在第11章關於微分方程的Diffeential-Equations模塊中，隻需要用20多行就可以定義任意微分方程的解。不過很少有規約需要用到如此深奧的數學知識，大多數時候隻需要簡單應用一些基礎數學概念即可。
為何是TLA
我們通過描述在執行過程中可能會發生的行為來定義繫統。1977年，AmirPnueli引入了時態邏輯（temporallogic）來描述繫統行為。從理論上講，繫統可以用單個時態邏輯公式表示，但在實際運用上卻有些問題：它雖然能很理想地描述繫統的某些屬性，但在描述其他屬性上卻不太方便。因此，我們通常將它與更傳統的繫統表示方式結合在一起來定義繫統。
也可稱為時序邏輯或時間邏輯，在本書中為了術語統一，均譯為時態邏輯。——譯者注
在20世紀80年代後期，我發明了TLA，即基於動作（Action）的時態邏輯——這是Pnueli初始邏輯的簡單變體。TLA使得用單個公式表示繫統變得切實可行。TLA規約的大部分由普通的、非時態邏輯的數學公式組成，時態邏輯僅在其擅長描述的屬性中引入並發揮作用。TLA還給出了一種很友好的繫統推理模式，這種模式被稱為斷言式推理（assertionalreasoning），其在實踐中被證明是有效的。不過，本書僅涉及規約本身，較少引入數學證明。
TLA 版本2對證明做了大量改進，參見19.7節。——譯者注
時態邏輯使用了一套基本邏輯來表示普通數學，還有許多其他方法也可以使普通數學形式化。大多數計算機科學家都喜歡使用與他們熟悉的編程語言近似的語言，相反，我選擇了大多數數學家更喜歡的方法，邏輯學家將其稱為一階邏輯和集合論。
TLA為描述繫統提供了數學基礎。要編寫規約，我們需要在此基礎上構建完整的語言體繫。我初認為該語言應該是某種抽像的編程語言，其語義將基於TLA。一開始我不知道用哪種編程語言結構好，於是決定直接用TLA編寫規約，計劃在需要時再引入編程語言。令我驚訝的是，到後來我發現不需要了，我所需的就是一種編寫數學公式的健壯語言。
盡管數學家已經發展了編寫公式的科學，但他們還沒有將其轉化為工程學科，他們為小規模的數學模型開發了符號語言，但對於大型應用還沒有好的方法，因為真實繫統的規約可能長達數十頁甚至數百頁。數學家知道如何編寫20行的公式，但對長達20頁的公式卻束手無策。因此，我不得不在語言中引入書寫長公式的符號方法，這些方法的形成得益於我從編程語言中學到的將大型規約模塊化的思路。
我將這種語言稱為TLA 。在編寫不同離散繫統的規約時，我不斷對TLA 進行提煉和改進，直到後來TLA 趨於穩定。我發現TLA 可以很好地定義從應用程序接口（API）到分布式繫統的各種繫統。它可以用來為幾乎任何類型的離散繫統編寫精準的形式化定義，尤其適合描述異步繫統，即組件運行不嚴格遵循鎖步操作（lock-step）的繫統。
關於本書
本書的部分包括第1～7章，是本書的核心，需要從頭到尾閱讀。它描述了如何定義稱為安全屬性的一類屬