実践TLA+


実践TLA+


翔泳社


著者:Hillel Wayne
訳者:株式会社クイープ
監修:株式会社クイープ


著者紹介
テクニカルレビューア紹介
謝辞

第0章 はじめに
0.1 本書で教えること
0.2 本書では取り上げないこと
0.3 本書の前提条件
0.4 本書の構成
0.5 最初の準備

第1部 TLA+とPlusCal のセマンティクス
第1章 例
1.1 問題
1.2 複数のプロセス
1.3 時相特性
1.4 まとめ

第2章 PlusCal
2.1 はじめに
2.2 仕様
2.3 PlusCalアルゴリズムの本体
2.4 複雑な振る舞い
2.5 まとめ

第3章 演算子と関数
3.1 演算子
3.2 不変条件
3.3 関数
3.4 例
3.5 まとめ

第4章 定数、モデル、インポート
4.1 定数
4.2 TLCランタイム
4.3 インポート
4.4 まとめ

第5章 並行処理
5.1 ラベル
5.2 プロセス
5.3 プロシージャ
5.4 例
5.5 まとめ

第6章 時相論理
6.1 停止性
6.2 時相演算子
6.3 活性の制限
6.4 例
6.5 まとめ

第2部 TLA+の適用
第7章 アルゴリズム
7.1 シングルプロセスアルゴリズム
7.2 Max
7.3 Leftpad
7.4 アルゴリズムの特性
7.5 マルチプロセスアルゴリズム
7.6 まとめ

第8章 データ構造
8.1 リンクリスト
8.2 検証
8.3 例
8.4 まとめ

第9章 状態機械
9.1 状態機械
9.2 実装の足場を組む
9.3 ゴースト変数
9.4 まとめ

第10章ビジネスロジック
10.1 要件
10.2 予約を追加する
10.3 まとめ

第11章 MapReduce
11.1 問題の概要
11.2 第1ステージ:基本的な仕様
11.3 第2ステージ:Liveness
11.4 第3ステージ:ステータス
11.5 練習問題
11.6 まとめ

付録A 数学
A.1 命題論理
A.2 集合
A.3 述語論理

付録B PTモジュール
付録C PlusCalからTLA+へ
C.1 時相論理
C.2 アクション
C.3 TLA
C.4 PlusCal制限

索引