実践ＴＬＡ＋

プラン駆動型システム開発の理解と演習
Ｐａｃｔｉｃａｌ　ＴＬＡ＋：Ｐｌａｎｎｉｎｇ　Ｄｒｉｖｅｎ　Ｄｅｖｅｌｏｐｍｅｎｔ

翔泳社
ヒレル・ウェイン　クイープ　

• 価格: 3,850円（本体3,500円＋税）
• 発行年月: 2021年09月
• 判型: Ａ５
• ISBN: 9784798169163

内容情報

[BOOKデータベースより]

第１部　ＴＬＡ＋とＰｌｕｓＣａｌのセマンティクス（例；ＰｌｕｓＣａｌ；演算子と関数；定数、モデル、インポート；並行処理　ほか）
第２部　ＴＬＡ＋の適用（アルゴリズム；データ構造；状態機械；ビジネスロジック；ＭａｐＲｅｄｕｃｅ）
付録

[日販商品データベースより]

設計だってテストしたい！





【本書の内容】

本書は

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でご覧いただける。