2012年に形式手法を学び始めるならこの7冊

前エントリー「僕が形式手法を学び始めたときに読んだ10冊 - masaterukの日記」のラインナップはあまりに入手困難なものばかりだったので、2012年に始めるならということで改めて選んでみた。

１冊目。

VDM++によるオブジェクト指向システムの高品質設計と検証 (IT architects’ archive)

VDM++の本。形式手法を学び始めるならこの本から始めると取っ付きやすいのではないかと思う。高級言語をつかった陽関数定義（実行可能形式）でモデルをがんがん書いて、シミュレーションとテストでモデルを洗練していくやり方は実際の現場にあっているように思う。関数型プログラム言語をひとつやふたつやったことある人なら、すいすいモデルをかけるんじゃないだろうか。

2冊目。

抽象によるソフトウェア設計−Alloyではじめる形式手法−

Alloyの本。前回のエントリーで紹介した通りなんだけど、訳本は第2版をベースにしていて中身も充実。上記のVDM++の本では陽関数定義でがんがん書いていくけど、Alloyでは陰関数定義でモデルを記述する。陰関数定義は、陽関数定義とは違って単に関係を記述する。方程式で例えるとx = から始まるような解を書く必要はなく方程式のままにしておくような書き方（だから解の公式を知らなくてもモデルが書ける）。関係しか記述しないと実行可能ではないのでVMD++のようにシミュレーションできないように思えるが、Alloyはそのモデルを例を示す事でシュミレーションを可能にする。形式的仕様記述の腕を上げたいならAlloyがおすすめ。

3冊目。

SPINモデル検査入門

Spinの本。これも今では日本語で解説している本がたくさん出ている。残念ながら全部目を通していないので自分が読んだ物の中から一冊選んだ。この本は、Spinをつかってモデル検査ができるようになることを目的とした本。裏側にある理論や機構については最小限にとどめツールを利用する事に主眼を置いた本。最初に始めるにはホルツマンの本ではなくこの本で良いのかもしれない。モデル検査は学べばすぐにでも現場で使える技術。

4冊目。

オブジェクト指向入門 第2版 原則・コンセプト (IT Architect’Archive クラシックモダン・コンピューティング)

メイヤーさんのオブジェクト指向入門第2版。残念ながら第2版は未読。第一版の内容をさらに充実させているだろうから間違いないと思う。契約による設計（Design by Contract）を学ぶんだったらこの本以外はないと思うし、契約による設計がソフトウェアの品質をぐっとあげてくれるだろうと思うので、やっぱり避けられない一冊。

5冊目。

Bメソッドによる形式仕様記述―ソフトウェアシステムのモデル化とその検証 (トップエスイー実践講座)

Bメソッド。これも未読。今からやるならリファインメント（詳細化）はおさえておきたい。やるならBメソッドかEvent-Bになるだろう。ちゃんとやるならどっちもやることになるだろうけど、「最初は日本語の本で始めたい」というならこの一冊かな。

6冊目。

Concurrent and Real-time Systems: The CSP Approach (Worldwide Series in Computer Science)

CSP。実は前エントリーで紹介したホーアの本「ホーアCSPモデルの理論」より読みやすい。CSPをやるならこの本から初めて"The Theory and Practice of Concurrency"に進むのが良いのかな。もう一度言うと、マルチスレッドやマルチプロセス、またはネットワーク越しにメッセージをやりとりするシステムを作っているならCSPはやっておいた方がいい。

7冊目。

Logic in Computer Science: Modelling and Reasoning about Systems

ここまでホーア論理を解説している本がなかったので最後にこれを選んでみた。自分は未読なんだけど一時期自分のまわりですごく流行った本。これで基本的なところをおさえるのがいいと思う。英語が苦手ならば、Coqを触りながら「ソフトウェアの基礎」を読み進めるのもいいかもしれない。

ということで、今回は以上7冊。