『実践TLA+』
https://gyazo.com/9062768b7e9113062a13c0e976f0598f
2021/9/15
設計、仕様のテストをする
第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の制限