実践TLA+

第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の制限

お問い合わせ

内容についてのお問い合わせは、正誤表、追加情報をご確認後に、お送りいただくようお願いいたします。

正誤表、追加情報に掲載されていない書籍内容へのお問い合わせや
その他書籍に関するお問い合わせは、書籍のお問い合わせフォームからお送りください。

利用許諾に関するお問い合わせ

本書の書影（表紙画像）をご利用になりたい場合は書影許諾申請フォームから申請をお願いいたします。
書影（表紙画像）以外のご利用については、こちらからお問い合わせください。