滿額折
商品簡介
名人/編輯推薦
目次
商品簡介
本書是作者針對分布式併發計算系統超過25年的研究成果的總結。在本書中，作者提出用基於動作的時態邏輯（TLA）來為複雜信息系統的行為建立數學模型，進而使用嚴格的數學證明與檢驗的方法來驗證系統行為的正確性。為此，作者發明了建模語言TLA+以及模型檢查工具TLC。本書結合若干案例，深入淺出地描述了從數學原理到系統建模的哲學思想，以及從建模語言的工程實踐到模型驗證工具的運用技巧等內容。
名人/編輯推薦
用形式化的建模和驗證方法保證所設計的軟硬件系統的正確性
目次
出版者的話
譯者序
前言
致謝
第一部分 入門
第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.4 元組也是函數 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.9 元組 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
譯者序
前言
致謝
第一部分 入門
第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.4 元組也是函數 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.9 元組 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
購物須知
大陸出版品因裝訂品質及貨運條件與台灣出版品落差甚大，除封面破損、內頁脫落等較嚴重的狀態，其餘商品將正常出貨。
特別提醒：部分書籍附贈之內容(如音頻mp3或影片dvd等)已無實體光碟提供，需以QR CODE 連結至當地網站註冊“並通過驗證程序”，方可下載使用。
無現貨庫存之簡體書，將向海外調貨：
海外有庫存之書籍，等候約45個工作天;
海外無庫存之書籍，平均作業時間約60個工作天，然不保證確定可調到貨，尚請見諒。
為了保護您的權益，「三民網路書店」提供會員七日商品鑑賞期(收到商品為起始日)。
若要辦理退貨，請在商品鑑賞期內寄回，且商品必須是全新狀態與完整包裝(商品、附件、發票、隨貨贈品等)否則恕不接受退貨。