出版者的話
譯者序
前言
致謝
部分 入門
第1章 簡單數(shù)學基礎2
1.1 命題邏輯 2
1.2 集合4
1.3 謂詞邏輯 4
1.4 公式與陳述句 6
第2章 定義一個簡單時鐘 7
2.1 行為7
2.2 時鐘7
2.3 解讀規(guī)約 9
2.4 TLA 規(guī)約 10
2.5 規(guī)約的另一種寫法 12
第 3 章 異步接口示例 13
3.1 個規(guī)約14
3.2 另一個規(guī)約17
3.3 類型回顧 18
3.4 定義 19
3.5 注釋 20
第 4 章 FIFO 接口示例23
4.1 內(nèi)部規(guī)約 23
4.2 剖析實例化25
4.2.1 實例化是一種代換 25
4.2.2 參數(shù)化的實例化 26
4.2.3 隱式代換 26
4.2.4 不需重命名的實例化 27
4.3 隱藏內(nèi)部變量 27
4.4 有界 FIFO 28
4.5 我們在定義什么 30
第 5 章 緩存示例31
5.1 內(nèi)存接口 31
5.2 函數(shù) 33
5.3 可線性化內(nèi)存系統(tǒng) 35
5.4 元組也是函數(shù) 37
5.5 遞歸函數(shù)定義 38
5.6 直寫式緩存39
5.7 不變式 44
5.8 證明實現(xiàn) 45
第 6 章 數(shù)學基礎拓展 47
6.1 集合 47
6.2 “笨表達式” 48
6.3 遞歸回顧 49
6.4 函數(shù)與運算符 51
6.5 函數(shù)使用 53
6.6 choose 54
第 7 章 編寫規(guī)約：一些建議 55
7.1 為什么要編寫規(guī)約 55
7.2 我們要定義什么 55
7.3 原子粒度 56
7.4 數(shù)據(jù)結構 57
7.5 編寫規(guī)約的步驟 57
7.6 進一步提示58
7.7 定義系統(tǒng)的時機和方法 60
第二部分 更多高級主題
第 8 章 活性和公平性 64
8.1 時態(tài)公式 64
8.2 時態(tài)重言式68
8.3 時態(tài)證明規(guī)則 71
8.4 弱公平性 71
8.5 內(nèi)存規(guī)約 75
8.5.1 活性要求 75
8.5.2 換個表示法 76
8.5.3 推廣80
8.6 強公平性 81
8.7 直寫式緩存82
8.8 時態(tài)公式量化 84
8.9 時態(tài)邏輯剖析 85
8.9.1 回顧85
8.9.2 閉包85
8.9.3 閉包和可能性 87
8.9.4 轉(zhuǎn)化映射和公平性 87
8.9.5 活性不重要 89
8.9.6 時態(tài)邏輯讓人困惑 89
第 9 章 實時系統(tǒng)90
9.1 回顧時鐘規(guī)約 90
9.2 通用實時規(guī)約 93
9.3 實時緩存 96
9.4 Zeno 規(guī)約100
9.5 混合系統(tǒng)規(guī)約 102
9.6 關于實時103
第 10 章 組合規(guī)約 104
10.1 雙規(guī)約的組合 104
10.2 多規(guī)約的組合 107
10.3 FIFO 109
10.4 共享狀態(tài)的組合 111
10.4.1 顯式狀態(tài)變化 112
10.4.2 相交動作的組合 114
10.5 簡短回顧118
10.5.1 組合方法的分類 118
10.5.2 審視交錯規(guī)約 118
10.5.3 審視相交動作規(guī)約 118
10.6 活性和隱藏 119
10.6.1 活性和閉包119
10.6.2 隱藏 120
10.7 開放系統(tǒng)規(guī)約 121
10.8 接口轉(zhuǎn)化123
10.8.1 二進制時鐘123
10.8.2 轉(zhuǎn)化通道125
10.8.3 接口轉(zhuǎn)化推廣 128
10.8.4 開放系統(tǒng)規(guī)約 129
10.9 規(guī)約形式選擇 131
第 11 章 高級示例 132
11.1 定義數(shù)據(jù)結構 132
11.1.1 局部定義132
11.1.2 圖 134
11.1.3 求解微分方程 137
11.1.4 BNF 語法139
11.2 其他內(nèi)存系統(tǒng)的規(guī)約 145
11.2.1 接口 146
11.2.2 正確性條件147
11.2.3 串行內(nèi)存系統(tǒng) 148
11.2.4 順序一致內(nèi)存系統(tǒng) 155
11.2.5 對內(nèi)存規(guī)約的思考 161
第三部分 工具
第 12 章 語法分析器 164
第 13 章 TLATEX 排版器 166
13.1 引言 166
13.2 陰影效果的注釋 167
13.3 規(guī)約排版168
13.4 注釋排版168
13.5 調(diào)整輸出格式 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 計算時態(tài)公式 186
14.2.5 模塊覆蓋187
14.2.6 TLC 如何計算狀態(tài) 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 調(diào)試規(guī)約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 優(yōu)先級與關聯(lián)性 226
15.2.2 對齊 229
15.2.3 注釋 230
15.2.4 時態(tài)公式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 函數(shù) 242
16.1.8 記錄 245
16.1.9 元組 246
16.1.10 字符串 247
16.1.11 數(shù)字 248
16.2 非恒定運算符 249
16.2.1 基礎恒定表達式 249
16.2.2 狀態(tài)函數(shù)的含義 250
16.2.3 動作運算符251
16.2.4 時態(tài)運算符254
第 17 章 模塊的含義 257
17.1 運算符與表達式 257
17.1.1 運算符的元數(shù)與順序 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 函數(shù)定義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 關于數(shù)字的模塊 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 當前狀態(tài)302
19.7.4 具有證明的步驟 303
19.7.5 無證明的步驟 306
19.7.6 對步驟與其組成部分的引用 308
19.7.7 對實例化的定理的引用 310
19.7.8 時態(tài)證明311
19.8 證明的語義 311
19.8.1 布爾運算符的含義 311
19.8.2 assume/prove 的含義 312
19.8.3 時態(tài)證明312