【本書の内容】
本書は
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章 はじめに
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の制限
翔泳社のプログラミング書籍の中から、入門・初級者向けの書籍をピックアップ！
【Linux本特集】入門～達人レベルまで！クラウド時代の必須知識Linuxを学ぶおすすめの本
ライティングのスキルアップにおすすめの本。Webライティングやコピーライティングなど
お金と経済の基礎知識から、資産形成・投資術、お金教育や介護まで。暮らしに役立つマネー本
おしゃれな部屋作りのヒントやインテリアの基礎知識、色使い、うつわや洋食器の知識まで、幅広い書籍をご紹介
Excel、日商簿記、業務の自動化を実現するRPAやPythonの技術など、事務職としてステップアップしたい人に！
