用TLA+定義系統(tǒng)：TLA+語言與工具在軟硬件設計中的應用

定　價：￥139.00

作　者：	[美] 萊斯利·蘭伯特（Leslie Lamport）著，董路明，賀志平譯
出版社：	機械工業(yè)出版社
叢編項：
標　簽：	暫缺

購買這本書可以去

ISBN：	9787111678229	出版時間：	2021-04-01	包裝：	平裝
開本：	16開	頁數(shù)：	328	字數(shù)：

內容簡介

　　本書是作者針對分布式并發(fā)計算系統(tǒng)超過25年的研究成果的總結。在本書中，作者提出用基于動作的時態(tài)邏輯（TLA）來為復雜信息系統(tǒng)的行為建立數(shù)學模型，進而使用嚴格的數(shù)學證明與檢驗的方法來驗證系統(tǒng)行為的正確性。為此，作者發(fā)明了建模語言TLA+以及模型檢查工具TLC。本書結合若干案例，深入淺出地描述了從數(shù)學原理到系統(tǒng)建模的哲學思想，以及從建模語言的工程實踐到模型驗證工具的運用技巧等內容。本書分為五個部分。第一部分包含大多數(shù)程序員和工程師需要了解的有關編寫系統(tǒng)規(guī)約（即建立模型）的所有信息；第二部分包含更高級的示例與材料，供需要進階的讀者使用；第三部分和第四部分為TLA+的參考手冊，包括語言本身的定義及工具的原理與使用；第五部分介紹在基礎TLA+語言上所演進出的TLA+版本2的新特性和少許變更。

作者簡介

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

圖書目錄

出版者的話
譯者序
前言
致謝
部分入門
第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 內部規(guī)約 23
4.2 剖析實例化25
4.2.1 實例化是一種代換 25
4.2.2 參數(shù)化的實例化 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 函數(shù) 33
5.3 可線性化內存系統(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ù)據結構 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 內存規(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 轉化映射和公平性 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 接口轉化123
10.8.1 二進制時鐘123
10.8.2 轉化通道125
10.8.3 接口轉化推廣 128
10.8.4 開放系統(tǒng)規(guī)約 129
10.9 規(guī)約形式選擇 131
第 11 章高級示例 132
11.1 定義數(shù)據結構 132
11.1.1 局部定義132
11.1.2 圖 134
11.1.3 求解微分方程 137
11.1.4 BNF 語法139
11.2 其他內存系統(tǒng)的規(guī)約 145
11.2.1 接口 146
11.2.2 正確性條件147
11.2.3 串行內存系統(tǒng) 148
11.2.4 順序一致內存系統(tǒng) 155
11.2.5 對內存規(guī)約的思考 161
第三部分工具
第 12 章語法分析器 164
第 13 章 TLATEX 排版器 166
13.1 引言 166
13.2 陰影效果的注釋 167
13.3 規(guī)約排版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 計算時態(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 調試規(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