Alloyとは
あなたの部署で、簡単なファイルシステムを設計しなければならなかったとしよう。
そしてあなたは、下のようなクラス図を描いてみせたとする。さて、この設計は正しいだろうか？
仕様記述言語Alloyは、そんな疑問に答えてくれるツールである。百聞は一見にしかず、このクラス図とほぼ等価なモデルをAlloyで書くと、次のような記述になる。
abstract sig オブジェクト {}
sig ファイル extends オブジェクト {}
sig フォルダ extends オブジェクト {
コンテンツ: set オブジェクト
}
run {}
最後の行を除いて、また“sig” というキーワードをclassに読み替えれば、書かれた内容はほぼJavaの文法から類推可能だろう。
そしてこのモデルを、Alloyの自動解析ツールである Alloy Analyzer（以下、「解析器」）にかけると、最後の行にある “run” （コマンド）にしたがって、次のような図を生成してくれる。
これは「インスタンス」と言い、元の記述を満たすような、システムのある1状態を捉えたスナップショットを表した図である。（UMLで言えば、オブジェクト図に相当する。) フォルダ1に着目してみると、フォルダの中にそのフォルダ自身が入っているような状態になっている。この状態を許すかどうかは設計者であるあなたの判断次第であるが、もしこれが意図していなかった状態であるなら、このような状態が起こらないようにモデルを見直し、修正をかければよい。そして再び解析器にかければ、修正した仕様を満たす、また別のインスタンスをツールが提示してくれる。
ここでは非常に簡単な例を紹介したが、必要に応じて細かな制約をモデル中に記述することができるし、また ”run” の代わりに “check” というコマンドを使って、モデル検査のような検証をしてみることも可能である。こうして、モデリングの結果がきちんと設計者の意図通りになっているかをAlloyは保証してくれる。
『抽象によるソフトウェア設計』（「Alloy本」）
Alloyは、MITのDaniel Jackson教授によって開発された。いわゆる「形式手法」と呼ばれるものの1つであるが、特に実用性と学習コストの低さを意識し、形式手法に関する知識があまりない人でも比較的簡単に手をつけられることを目指している。
そして、そのJackson教授によって記された書籍 “Software Abstractions” を筆者らの手で翻訳したのが、オーム社より7月に刊行された『抽象によるソフトウェア設計 －Alloyではじめる形式手法－』（右図）である。本書を手にとって頂ければ、Alloyの使い方、Alloyを使ったモデリング手法について、一通り習熟できるようになっている。
また、単にAlloyの解説というだけにとどまらず、高信頼なソフトウェアの設計とはどうあるべきか、Jackson教授の思いの丈が随所に綴られている。これまで読者の方々から「技術書である前に、読み物として面白い」という感想を多くいただいたのは、我々にとってもうれしい驚きであった。
筆者らの翻訳には、もう1つ大きな特徴がある。本書は未発売の、原書改訂版の内容をいち早く取り込み、Alloyの最新版であるAlloy 4に完全対応している。筆者らはJackson教授と密に連絡を取り、原書の改訂と同時並行で翻訳を進めた。
追加情報
さて、Alloyに関して新しい情報がいくつかあるので、残りの紙面を使って皆さんにお知らせしたい。
まず、翻訳書のPDF版が11月7日より、オーム社eStoreにて発売された（http://estore.ohmsha.co.jp/titles/978427406858P より購入可能）。電子ブックリーダーを活用されている方は、こちらでの購入もご検討いただきたい。
また、先にも述べた原書改訂版であるが、2012年2月の発売が決定した。日本語版、原書第１版は赤い表紙であるが、改訂版はライトグリーンの表紙が目印である。MIT Pressの公式サイト（http://mitpress.mit.edu/catalog/item/default.asp?ttype=2&tid=12880）で予約可能であるほか、Amazonでも今月から予約可能になっている（http://www.amazon.co.jp/dp/0262017156）。
[12/7 追記] その後確認したところ、公式発売日に先駆けて11月から原書改訂版が流通しているとの事である。公式サイト、Amazonからも既に購入可能である。
そして解析器Alloy Analyzerについてである。本記事の例のように、現在の解析器のバージョン（Alloy Analyzer 4.2RC 2011-09-14）ではUnicodeでの識別子が使えるようになり、日本語を使った仕様が記述可能になっている。Alloy Analyzer 4ホームページ（http://alloy.mit.edu/alloy4/）よりダウンロード可能である。
本書のサポートは、筆者らによるサポートページ（https://sites.google.com/site/softwareabstractionsja/）のほか、メーリングリスト（http://groups.google.com/group/alloy-jp）で行っている。特にメーリングリストでは、本書サポートにとどまらず、Alloyの利用方法一般に関して、時に活発な議論を行っている。本書入手の折にご活用いただきたい。