実践ＴＬＡ＋　プラン駆動型システム開発の理解と演習

ＴＬＡ＋はプログラミング言語です。ただし、ＪａｖａやＣ／Ｃ＋＋などとは異なり設計用に特化された言語です。本書ではＭｉｃｒｏｓｏｆｔやＡｍａｚｏｎがミドルウェアの設計に利用しているＴＬＡ＋の概要とそのＩＤＥ（ＴＬＡ＋　Ｔｏｏｌｂｏｘ）の使い方を解説します。

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

【本書の内容】
本書は
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+へ

本の帯に関して

帯つきでの出荷はお約束しておりません。
商品ページに、帯のみに付与される特典物等の表記がある場合でも、確実に帯つきでの出荷はお約束しておりません。
また、帯は商品の一部ではなく「広告扱い」のため、帯の有無・破損による交換や返品は承っておりません。

版・表紙について

版・表紙（カバー）のご指定は承っておりません。ご注文いただくタイミングによっては、お届けする商品の版や表紙が商品ページ上のものとは異なる場合がございます。
また、初版にのみにお付けしている特典（初回特典、初回仕様特典）がある商品は、商品ページに特典の表記がされている場合でも、無くなり次第終了となります。