実践 TLA+

TLA+ は、プログラムを書く前の設計や仕様そのものに誤りがないかを、機械に網羅的に確かめさせるための仕様記述言語です。『実践 TLA+』 (Hillel Wayne 著、株式会社クイープ 訳・監修、翔泳社、2021 年 9 月 15 日発売) は、2018 年に Apress から刊行された Practical TLA+ の邦訳で、副題は「プラン駆動型システム開発の理解と演習」です。送金システムの小さな仕様から深刻なバグを見つけるところから始め、TLA+ と PlusCal の書き方を身に付けたうえで、アルゴリズム、データ構造、ビジネスロジック、MapReduce といった実用的な問題に当てはめていきます。著者は形式手法と仕様記述を専門とするソフトウェアコンサルタントで、版元の紹介によれば、TLA+ の生みの親である Leslie Lamport も理論的な背景を脚注で解説しています。

第 0 章と 2 部 11 章、付録 3 本の構成

目次は第 0 章「はじめに」のあと 2 部に分かれます。第 1 部「TLA+ と PlusCal のセマンティクス」は第 1 章「例」から始まり、PlusCal、演算子と関数、定数とモデルとインポート、並行処理、時相論理の順に、言語の意味を一つずつ押さえる 6 章です。第 2 部「TLA+ の適用」は、アルゴリズム、データ構造、状態機械、ビジネスロジック、MapReduce の 5 章で、身に付けた書き方を種類の違う問題に当てはめます。巻末には数学、PT モジュール、PlusCal から TLA+ への 3 本の付録が付きます。版元の紹介では、第 1 部で学ぶ範囲を演算子、論理、関数、PlusCal、モデル、同時実行の基礎とし、そのうえで設計図の整理の仕方や、分散システムと 最終的な整合性 の指定の仕方へ進むと説明しています。

テストでは見つけにくい設計のバグを、状態を総当たりして探す

並行に動く処理や複数のマシンにまたがる処理では、命令の実行順序の組み合わせが膨大になり、ごくまれな順序でしか起きない 競合状態 は、単体テストや結合テストを何度回しても再現しないことがあります。TLA+ は、システムが取りうる状態と、状態から状態への移り変わりを数学の言葉で書き下し、モデル検査器と呼ばれる道具に、決めた範囲の中で到達しうる状態をすべて調べさせます。「残高が負にならない」のような常に守られるべき性質や、「送金はいずれ完了する」のような時間の流れにかかわる性質を書いておけば、それを破る実行の道筋が具体的な手順の列として示されます。PlusCal は、この仕様を擬似コードに近い書き方で記述するための言語で、TLA+ に変換して検査に回します。数式だけで仕様を書くことに抵抗がある開発者でも、手続きの形から入れるのが PlusCal の利点で、本書でも第 1 章の例に続く第 2 章が PlusCal に充てられています。

数学の前提と、仕様を書く練習に要る手間

形式手法という言葉から難解な数学を想像するかもしれませんが、TLA+ の仕様で使うのは、集合、関数、論理式といった離散数学の基礎が中心で、本書も付録 A に数学を置いています。それでも、プログラムではなく「何が起きてよく、何が起きてはいけないか」を書く作業は、コードを書く頭の使い方とは違い、最初は戸惑いやすい部分です。版元は本書のポイントとして、言語仕様を手を動かしながら学べることと、短時間で読み終えられることを挙げています。読むだけでなく、例の仕様を自分の手元で検査に回し、条件を変えるとどんな反例が出るかを試すことで、書き方が身に付いていく種類の本です。なお原著は 2018 年刊なので、手元で使うツールの版と本書の説明が細部で食い違ったときは、ツールの配布元の説明を合わせて確かめると進めやすくなります。

分散システムの設計者に向く理由と、向かない目的

版元が挙げる対象読者は、アーキテクト、デベロッパー、エンジニアです。特に合うのは、複数のサービスが同じデータを更新する仕組みや、再試行と重複処理が絡む業務フローを設計していて、レビューの議論だけでは抜けを潰しきれないと感じている人です。設計の段階で反例を手に入れられれば、作り込んだあとに不具合を追うよりも少ない手間で直せます。一方、TLA+ の理論的な基礎を論理学の側から深く学びたい場合は、Lamport 自身の著作や講義資料に当たるほうが目的に近く、コードの単体テストの書き方を学びたい場合は、テスト本の選び方 を参考に別の本を選ぶほうが向いています。設計そのものをテストしたいという動機がはっきりしている開発者にとって、身近な例から実用的な問題まで一冊で通して練習できる本書は、形式手法を業務に持ち込む最初の足場になります。