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

定　價(jià)：￥139.00

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

購買這本書可以去

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

內(nèi)容簡介

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

作者簡介

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

圖書目錄

出版者的話
譯者序
前言
致謝
部分入門
第1章簡單數(shù)學(xué)基礎(chǔ)2
1.1 命題邏輯 2
1.2 集合4
1.3 謂詞邏輯 4
1.4 公式與陳述句 6
第2章定義一個(gè)簡單時(shí)鐘 7
2.1 行為7
2.2 時(shí)鐘7
2.3 解讀規(guī)約 9
2.4 TLA 規(guī)約 10
2.5 規(guī)約的另一種寫法 12
第 3 章異步接口示例 13
3.1 個(gè)規(guī)約14
3.2 另一個(gè)規(guī)約17
3.3 類型回顧 18
3.4 定義 19
3.5 注釋 20
第 4 章 FIFO 接口示例23
4.1 內(nèi)部規(guī)約 23
4.2 剖析實(shí)例化25
4.2.1 實(shí)例化是一種代換 25
4.2.2 參數(shù)化的實(shí)例化 26
4.2.3 隱式代換 26
4.2.4 不需重命名的實(shí)例化 27
4.3 隱藏內(nèi)部變量 27
4.4 有界 FIFO 28
4.5 我們?cè)诙x什么 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 證明實(shí)現(xiàn) 45
第 6 章數(shù)學(xué)基礎(chǔ)拓展 47
6.1 集合 47
6.2 “笨表達(dá)式” 48
6.3 遞歸回顧 49
6.4 函數(shù)與運(yùn)算符 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ù)結(jié)構(gòu) 57
7.5 編寫規(guī)約的步驟 57
7.6 進(jìn)一步提示58
7.7 定義系統(tǒng)的時(shí)機(jī)和方法 60
第二部分更多高級(jí)主題
第 8 章活性和公平性 64
8.1 時(shí)態(tài)公式 64
8.2 時(shí)態(tài)重言式68
8.3 時(shí)態(tài)證明規(guī)則 71
8.4 弱公平性 71
8.5 內(nèi)存規(guī)約 75
8.5.1 活性要求 75
8.5.2 換個(gè)表示法 76
8.5.3 推廣80
8.6 強(qiáng)公平性 81
8.7 直寫式緩存82
8.8 時(shí)態(tài)公式量化 84
8.9 時(shí)態(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 時(shí)態(tài)邏輯讓人困惑 89
第 9 章實(shí)時(shí)系統(tǒng)90
9.1 回顧時(shí)鐘規(guī)約 90
9.2 通用實(shí)時(shí)規(guī)約 93
9.3 實(shí)時(shí)緩存 96
9.4 Zeno 規(guī)約100
9.5 混合系統(tǒng)規(guī)約 102
9.6 關(guān)于實(shí)時(shí)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 相交動(dòng)作的組合 114
10.5 簡短回顧118
10.5.1 組合方法的分類 118
10.5.2 審視交錯(cuò)規(guī)約 118
10.5.3 審視相交動(dòng)作規(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 二進(jìn)制時(shí)鐘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 章高級(jí)示例 132
11.1 定義數(shù)據(jù)結(jié)構(gòu) 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 對(duì)內(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 的應(yīng)用范圍 181
14.2.1 TLC 值181
14.2.2 TLC 如何計(jì)算表達(dá)式 182
14.2.3 賦值與代換184
14.2.4 計(jì)算時(shí)態(tài)公式 186
14.2.5 模塊覆蓋187
14.2.6 TLC 如何計(jì)算狀態(tài) 187
14.3 TLC 如何檢查屬性190
14.3.1 模型檢查模式 190
14.3.2 仿真模式192
14.3.3 視圖和指紋192
14.3.4 利用對(duì)稱性193
14.3.5 活性檢查的限制 195
14.4 TLC 模塊 196
14.5 TLC 的用法 198
14.5.1 運(yùn)行 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)先級(jí)與關(guān)聯(lián)性 226
15.2.2 對(duì)齊 229
15.2.3 注釋 230
15.2.4 時(shí)態(tài)公式231
15.2.5 兩種異常231
15.3 TLA 的詞素 232
第 16 章 TLA 的運(yùn)算符 233
16.1 恒定運(yùn)算符 233
16.1.1 布爾運(yùn)算符234
16.1.2 選擇運(yùn)算符236
16.1.3 布爾運(yùn)算符的解釋 237
16.1.4 條件構(gòu)造239
16.1.5 let/in 構(gòu)造 240
16.1.6 集合運(yùn)算符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 非恒定運(yùn)算符 249
16.2.1 基礎(chǔ)恒定表達(dá)式 249
16.2.2 狀態(tài)函數(shù)的含義 250
16.2.3 動(dòng)作運(yùn)算符251
16.2.4 時(shí)態(tài)運(yùn)算符254
第 17 章模塊的含義 257
17.1 運(yùn)算符與表達(dá)式 257
17.1.1 運(yùn)算符的元數(shù)與順序 257
17.1.2 λ 表達(dá)式 258
17.1.3 簡化運(yùn)算符應(yīng)用 259
17.1.4 表達(dá)式 260
17.2 級(jí)別 261
17.3 上下文 263
17.4 λ 表達(dá)式的含義 264
17.5 模塊的含義 265
17.5.1 引入 266
17.5.2 聲明 266
17.5.3 運(yùn)算符定義267
17.5.4 函數(shù)定義267
17.5.5 實(shí)例化 267
17.5.6 定理與假設(shè)269
17.5.7 子模塊 269
17.6 模塊的正確性 270
17.7 尋找相關(guān)模塊 270
17.8 實(shí)例化的語義 271
第 18 章標(biāo)準(zhǔn)模塊 276
18.1 Sequences 模塊276
18.2 FiniteSets 模塊 277
18.3 Bags 模塊277
18.4 關(guān)于數(shù)字的模塊 279
第五部分 TLA 版本 2 基礎(chǔ)
第 19 章 TLA 版本 2 286
19.1 簡介 286
19.2 遞歸運(yùn)算符定義 286
19.3 lambda 表達(dá)式 288
19.4 定理與假設(shè) 288
19.4.1 命名 288
19.4.2 assume/prove 289
19.5 實(shí)例化 290
19.5.1 實(shí)例化詞綴運(yùn)算符 290
19.5.2 Leibniz 運(yùn)算符和實(shí)例化 291
19.6 命名子表達(dá)式 292
19.6.1 標(biāo)簽和帶標(biāo)簽的子表達(dá)式名稱 292
19.6.2 位置相關(guān)的子表達(dá)式名稱 294
19.6.3 let 定義中的子表達(dá)式 297
19.6.4 assume/prove 的子表達(dá)式 297
19.6.5 將子表達(dá)式名稱用作運(yùn)算符 298
19.7 證明的語法 298
19.7.1 證明的結(jié)構(gòu)298
19.7.2 use、hide 與 by 300
19.7.3 當(dāng)前狀態(tài)302
19.7.4 具有證明的步驟 303
19.7.5 無證明的步驟 306
19.7.6 對(duì)步驟與其組成部分的引用 308
19.7.7 對(duì)實(shí)例化的定理的引用 310
19.7.8 時(shí)態(tài)證明311
19.8 證明的語義 311
19.8.1 布爾運(yùn)算符的含義 311
19.8.2 assume/prove 的含義 312
19.8.3 時(shí)態(tài)證明312