実践TLA+
https://www.seshop.com/static/images/product/24266/L.png
複雑精緻なシステムを構築する際に、設計 そのもの、仕様 そのものにバグがないかをテストできたら、もう少し幸せな開発人生を送れそうな気がします。 本書は送金システムの小規模な仕様から TLA+ を使ってヤバいバグを発見するところから始まります。この小さなサンプルをもとに、より良いアプリケーションの設計・テスト・構築に、どのように TLA+ を使えばよいかを理解し、実際のプロジェクトに援用できるよう、TLA+ の演算子、論理、関数、PlusCal、モデル、および同時実行の基礎を学びます。 設計図の整理の仕方、分散システムや最終的な整合性の指定の仕方を学んだら、アルゴリズムのパフォーマンスやデータ構造、ビジネスコードや MapReduce など、さまざまな実用的な問題に TLA+ を適用し、ケーススタディのアプリケーションを使って実践します。 TLA+ の生みの親である Leslie Lamport も、理論的背景を脚注で解説するなど、最先端のシステム開発テクノロジーのコアに触れることのできる1冊です。
目次
第0章 はじめに
第1部 TLA+とPlusCalのセマンティクス
第1章 例
第3章 演算子と関数
第4章 定数、モデル、インポート
第5章 並行処理
第6章 時相論理
第2部 TLA+の適用
第7章 アルゴリズム
第8章 データ構造
第9章 状態機械
第10章 ビジネスロジック
第11章 MapReduce
付録A 数学
付録B PTモジュール
付録C PlusCalからTLA+へ