僕が形式手法を学び始めたときに読んだ10冊

後輩に形式手法を学び始めたときに読んだ本を紹介すると約束したので、せっかくなのでブログに書くことにした。
形式手法を学び始めたのは2004年だから、今から始める場合はまた違ったラインナップになるだろうけど。
※「2012年に形式手法を学び始めるならこの7冊 - masaterukの日記」を書きました。

1冊目。

プログラミングの科学 (情報処理シリーズ)

出会いはこの本。僕の人生を変えてしまった本だ。この本に出会ったときの衝撃は今でも覚えている。命題と述語からはじまり、ホーア論理、そしてプログラムの作り方が解説してある。「プログラムの作り方」を解説している本は少ない。Twitterでもつぶやいたけど、assertの使い方を教えてくれたのもこの本だった。現在は入手困難だけど、何とか手に入れて読んでほしい。

2冊目。

ソフトウェア開発のモデル化技法

仕様記述言語VDM-SLの本。VDMはツールもあるので、モデルを書きながら読み進めるといいだろう。この本でよく覚えているのは「第1章　序章」。序章を読んで、何となく内容を理解したつもりになっていたけど、実は全然理解していなかったってことに後で気づいたのを覚えている。”仕様”や”設計”ってソフトウェア開発しているとなじみのある言葉だから軽く読み流してしまうんだけど、そうやって読んでいるといつまでも理解が深まらない。本は一言一句大切に読むべきということを学んだ本。なお、VDMのモデルをみて「これなら直接プログラム書くのと変わらない」と思ったらまだまだだと思った方が良い。

3冊目。

ソフトウェア仕様記述の先進技法 Z言語

こちらはZの本。上の2冊を読んでいれば割とすんなり読めるかな。この本には、仕様とプログラムが満たすべき関係と詳細化についての解説がある。今ならBメソッドをやった方がいいのだろうか。この本を読んでた頃、ZやVDMで自分たちが開発しているシステムのモデルを書いて、最弱事前条件を計算していたりしたっけ。

4冊目。

コンピュータサイエンス入門〈2〉論理とプログラム意味論

リアクティブシステムについて日本語で学べる貴重な本。これも絶版なのか…。リアクティブシステムとは、外部環境とやりとりしながら動き続けるシステムのこと。作られるソフトウェアの多くがリアクティブシステムと言えるだろう。リアクティブシステムのプログラム、意味論、時相論理による仕様記述と検証について学べる。薄いけど内容が濃く、何度も読み直した（読み直さないと理解できなかった）本。

当時は、上記4冊がいわゆる必須科目と言われていた。この4冊は何度も読み返した。

5冊目。

論理学をつくる

論理学の本。どの本もだいたい命題と論理から説明してあるんだけど、どうもそのあたりの理解が怪しいので買った本。戸田山先生の本はとても分かりやすて独学に向いている。これはまだ買える。良かった。

6冊目。

オブジェクト指向入門 (ASCII SOFTWARE SCIENCE Programming Paradigm)

オブジェクト指向の名著。ZやVDMで書くモデルと自分たちが開発しているオブジェクト指向ってどういう関係にあるか分からなくて、オブジェクト指向を特定のプログラム言語によらずに勉強したくて読んだ本。まぁ、Eiffelって言語なんだけどw 説明が明解でわかりやすい。形式仕様記述を学んだあとだと契約による設計は非常になじみやすい。形式手法に興味なくてもオブジェクト指向やるんだったらこれは読んでほしい。

7冊目。

ホーアCSPモデルの理論

ホーアのCSPの本。マルチスレッドやマルチプロセスといった並行システムのモデルの本。CSPを使えば、並行に動作するプロセスを組み合わせたときに全体としてどういう振る舞いになっているか？を計算でき、仕様を満足しているか検証できる。しかも、証明で。パフォーマンスが求められるシステムではマルチスレッド、マルチプロセスになることは避けられないだろうし、オブジェクト指向システムをオブジェクトが相互作用するシステムと捉えることもできるので、CSPの適用範囲は広いのではないかと見ている。逆に、こういったモデルなしに並行システムを検証する事は不可能だろう。

8冊目。

計算機プログラムの構造と解釈

SICP。今さら紹介するまでもないんだけど、自分の印象はプログラミングに関する概念を一通り学べる本といったところ。当時、CやC++などの手続き型言語しか知らなかったので、高階関数や遅延評価、継続といった概念には「へぇ」って思った。決して仕事で使わなくても、こういう概念を知っていると知らないとでは生み出すプログラムが違うんじゃないだろうか。

9冊目。

SPIN Model Checker, The: Primer and Reference Manual

モデル検査器SPINの本。これまた自分の人生を変えた本。はじめて現場で適用したのがSPINだった。マルチプロセスでやりとりするプロトコルの設計をまかされて、「こりゃ大変じゃ」と思って、まだデッドロック検出（SPINはデフォルトでデッドロック検出をしてくれる）とassertしか使えない状態でPromelaで書き始めた。書いて検査すると非常に優秀なレビューアといっしょにペアモデリングをやっているような感覚がある。モデル検査は実際の現場で適用しやすいと思う。SPINを徹底的に学びたいならこの一冊だろうな。

10冊目。

Software Abstractions: Logic, Language, and Analysis

Alloyの本。形式的に仕様を表現して、その仕様を満足するプログラムを作ったとしても、仕様が自分が欲しているものと異なっているとせっかくのプログラムも意味がない。だから書いた仕様が自分が欲しい物なのかを確認したい。Alloyはそれができるツール。自分が記述したモデルを満たす例を示してくれる。こういうツールは容赦がなくて、「そういうつもりじゃないんだよ」って言いたくなるような例をいっぱい示してくれる（そういうときは仕様の記述が足りないからバグとなりうる）。この本は、第２版の訳本『抽象によるソフトウェア設計−Alloyではじめる形式手法−』が出ているので、今やるなら訳本を読めば良い。

以上、10冊。