実践 TLA+

設計だってテストしたい! 【本書の内容】 本書は Hillel Wayne, "Practical TLA+", Apress, 2018 の邦訳版です。 複雑精緻なシステムを構築する際に、設計そのもの、仕様そのものにバグがないかをテストできたら、もう少し幸せな開発人生を送れそうな気がします。 本書は送金システムの小規模な仕様から TLA+を使ってヤバいバグを発見するところから始まります。この小さなサンプルをもとに、より良いアプリケーションの設計・テスト・構築に、どのように TLA+を使えばよいかを理解し、実際のプロジェクトに援用できるよう、 TLA+の演算子、論理、関数、 PlusCal 、モデル、および同時実行の基礎を学びます。 設計図の整理の仕方、分散システムや最終的な整合性の指定の仕方を学んだら、アルゴリズムのパフォーマンスやデータ構造、ビジネスコードや MapReduce など、さまざまな実用的な問題に TLA+を適用し、ケーススタディのアプリケーションを使って実践します。 TLA+の生みの親である Leslie Lamport も、理論的背景を脚注で解説するなど、最先端のシステム開発テクノロジーのコアに触れることのできる 1 冊です。 【本書のポイント】 ・ TLA+の言語仕様を手を動かしながら学べる ・小さなサンプルから並行処理や分散システムまで TLA+を適用できるようになる ・短時間で読み終わるものの滋養は豊富 【読者が得られること】 ・ TLA+が理解できる ・ TLA+を使ったシステム開発に乗り出せる ・上流からテスト駆動ができる ・バグの少ないシステムを構築できる 【対象読者】 ・アーキテクト ・デベロッパー ・エンジニア 【著者について】 ● Hillel Wayne (ヒレル・ウェイン) 形式手法と仕様記述を専門とするソフトウェアコンサルタント。経験工学、ソフトウェアの歴史、教育などについても造詣が深い。ジャグリングとチョコレート作りが趣味。 シカゴ在住。その他の活動は、 hillelwayne.com または Twitter の@hillelogram でご覧いただける。 第 0 章 はじめに 第 1 部 TLA+と PlusCal のセマンティクス 第 1 章 例 第 2 章 PlusCal 第 3 章 演算子と関数 第 4 章 定数、モデル、インポート 第 5 章 並行処理 第 6 章 時相論理 第 2 部 TLA+の適用 第 7 章 アルゴリズム 第 8 章 データ構造 第 9 章 状態機械 第 10 章 ビジネスロジック 第 11 章 MapReduce 付録 A 数学 付録 B PT モジュール 付録 C PlusCal から TLA+へ