TL;DR
- TLA+ を使って、システムの設計や仕様そのものにバグがないかを検査する方法を学ぶ本である。
- 送金システムの小さな仕様からバグを見つけるところから始め、演算子、論理、関数、PlusCal、モデル、並行処理の基礎を学んだ後、アルゴリズムやデータ構造、ビジネスロジック、MapReduce などの実用的な問題に適用する。
目次
- はじめに
- 第1部 TLA+とPlusCalのセマンティクス
- 例
- PlusCal
- 演算子と関数
- 定数、モデル、インポート
- 並行処理
- 時相論理
- 第2部 TLA+の適用
- アルゴリズム
- データ構造
- 状態機械
- ビジネスロジック
- MapReduce
- 付録A 数学
- 付録B PTモジュール
- 付録C PlusCalからTLA+へ