Alloy Analyzer はじめの一歩（二度目のチャンスは逃さない。）

Alloy Analyzer Alloy for RDB

モデリング検査ツール Alloy Analyzer を使いたい！のエントリ。第二回目。

先回はシンプルな『親子関係』をモデリングしました。
その際の fact（＝モデル定義から導かれる静的なタイプの制約を書くところ）
が、明らかに場当たり的な記述だったんで、もっと適切な書き方は無いかと探したところ、
ありました！すばらしい資料が。やったあ。宝の山ですよ。
カリフォルニア大サンタバーバラ校の、Tevfik Bultan 先生によっておこなわれた
『Formal Models for Web Software』という講座の記録です。
CS 290C Spring 2013 Home Page
Lectures 7 から 10 あたりまでが正に僕の関心事です。
WEBで見つかるAlloyの資料って、ちょっとアカデミックに過ぎる傾向があると思ってるんですが、
この講座の趣旨は実にpracticalで、好ましいです。

で、親子関係モデルの fact は以下のように書くようにしました。

One to Many

module father_and_son
sig Dad {
  son: set Son
}
sig Son {
  dad: one Dad
}
fact RelDadSon {
  // 相互的な参照には必須
  // 「"父を持つ子"の、親子関係を反転させると、それは"子を持つ父"に等しい」
  Dad <: son = ~(Son <: dad)
}

run {} //for 5

One to One

module father_and_one_son
sig Dad {
  son: lone Son
}
sig Son {
  dad: one Dad
}
fact RelDadSon {
  // 相互的な参照には必須
  // 「"父を持つ子"の、親子関係を反転させると、それは"子を持つ父"に等しい」
  Dad <: son = ~(Son <: dad)
}

run {} //for 5

  • "~" という記号はAlloyでは、反転を意味します。
  • "<:" という記号は、フィルタでして、ここでは右辺が左辺の値域を制限していることを示します。

なのでこのfactの制約を自然言語で書くと
「"親を持つ子"の、親子関係を反転させると、それは"子を持つ親"に等しくなる。」
といったところでしょうか。

もうちょっと説明がいりますね。
Alloy上の、モデルのインスタンスは、プログラマがイメージするモデルインスタンスとちょっと違うようです。
Alloy上の、モデルのインスタンスは、単なるバリューオブジェクトとして考えるより
「(実体化された)関係そのもの」
として考えるのがよさそうに思います。そういう、ちょっとした発想の切り替えはやっぱり要りますね。

AlloyのEvaluatorのウィンドウを開いて何かしら式をタイプすれば、IDEのデバッガのように使えるので、
実際に値をインスペクトしながら見ていきましょう。

例えば、この図のような状態ときは、

まず

Son <: dad

は、
「dadという"関係" を実現している、Son のインスタンス群」
を示しています。これがEvaluator上では、下記のように表現されるわけです。

{Son$0->Dad$1, Son$1->Dad$0, Son$2->Dad$0}

使われてる記号の意味をすべて理解していなくても、こうして実体が見られれば、なんとなく分かります。
要は、単なるSon型のバリューオブジェクトじゃなくて、"関係"の情報を持っている。そしてのその"関係"の情報は、
Sonオブジェクトの内部に属性として持っているわけでは無い、ってのもポイントかな？きっと。

で、その反転である、

~(Son <: dad)

は、

{Dad$0->Son$1, Dad$0->Son$2, Dad$1->Son$0}

あ、なるほど、こうなるんですね。
「関係」の「反転」って具体的に何なんだ、ということが、Evaluator上で見る事で初めて、しかし明快にわかります。
これを見て、反転した Son <: dad は、Dad <: son に等しい、ということが、すぐに腑に落ちました。


ところでこの fact、一目見て理解しやすいか、というと、、、う〜ん、そうではない。。。
先回、「普段使っているRDBと同じようにAlloyを使いたい」という内容の希望を書いたんですが、
こんな fact の書き方は、その希望には適ってませんね。発想のパラダイムが、RDBをただ利用するときのそれとはは明らかに違います。
まあ、それこそがAlloyの本質でもあるのでしょうけれど、、、、"関係指向"って呼び方でいいんでしょうか？
このへんの考えかたのヒントは、この、id:pokarim さんのエントリ
「属性と関係」のつづき - Conceptual Contexture なんかが、有難かったです。

じゃあ先回書いたのバージョンの fact のほうがましか、といえば、それはノーだと思う。
エンジニアとしての嗅覚がまちがいなくそう答えている。
というような自己矛盾を早速かかえてしまいましたが、

それよりも、せっかくTevfik Bultan 先生のすばらしい資料がいっぱい手に入ったんで、
しばらくはこの資料に沿って勉強しようと思います。