Alloy 本

土曜に Amazon のお急ぎ便で注文したら、日曜の夜に届いた。
日曜は暇がなかったので、今日、帰宅してから早速 Alloy Analyzer をダウンロードして、テキストに取りかかる。（単なる jar なので java -jar ですぐ動く。）

下図の左側ペインのようにコードを書き込んで、[Execute]>[Show Metamodel]を実行すると、、、

、、、このようなダイアグラムが得られる。

このダイアグラムは、四角形の配置を変えたり、色やフォントを変えたりして、ある程度見せ方を好きなように変えられるようだけど、どうもダイアグラムはそれほど本質的なものではないっぽい。

まあ、1時間ほどいじっただけだし何も理解できてないけど、上の上の図で左側のペインに書いてある Alloy コードがやっぱり主役っぽい。
これに述語（pred）やファクト（fact）をちょっと書き足しては、それに対してアサーション（assert）をちょっと付け加えて、そしたら実行して右側のペインで確認して、って流れになる模様。そうだとしたら、どこか TDD に似ていてとっつきやすい。

とは言っても、関心の重点は実装ではなくむしろ仕様であって高い抽象レベルで仕様をモデリングする事が目的の技術らしい。
ちなみに、抽象度をレベル分けするときに、伝統的に分析レベル、設計レベル、実装レベルなんて言ったりするけど、Alloy と同じ雰囲気で、なおかつレベルの違う他言語を持ってくると、分析レベル：Alloy、設計レベル：LePUS3、実装レベル：Coq てな感じに当てはまるんじゃないかと思う。

まあ、いきなりいろんな事をやり始めなくても、とりあえず Alloy だけでも、例えば金融システムのビジネスルールとかに適用して、仕様バグを取り除くような事は、結構すぐにでも始められそうな予感。