Alloyを勉強する日記(1)
とりあえず教科書が届いたのでざっくり読んでみた。
ここからどうやって勉強していくかなー。とりあえず既に存在しているソフトウェアをモデリングしてみて、自分がどこまでできてどこでつまずくかを確認してみるか。んー、じゃ、Gitをモデリングする。
とりあえずコミットオブジェクトがあるんだよな。コミットオブジェクトは1個のツリーオブジェクトを持っていて、ツリーオブジェクトは0個以上のブロブオブジェクトを持っている、と。
とりあえず「いくつ持ってる」って制約は保留して、3つの種類のオブジェクトだけ作る。あと、「制約を満たすものを表示する」という命令である「run」を書く。教科書p7のpred showはひどいネーミングだなぁ。
module nhiro/etude1
sig CommitObj {
tree: TreeObj
}
sig TreeObj {
blobs: BlobObj
}
sig BlobObj {
}
pred always_success {}
run always_successで、とりあえずshowして眺めてみる。
ふむふむ。それっぽい。
blobが2個でtreeが3個なのになんで右上の囲みにtree: 2, blobs: 3って表示されてるんだろう、としばらく考えたが、これは「関係」の個数なんだな。了解。
次は保留してた数の制約とかを書こう。こういうのは「多重度制約」と呼ぶらしい。p.72。コミットオブジェクトは1個のツリーオブジェクトを持ち、ツリーオブジェクトは1個以上のブロブオブジェクトを持つ。(なお今回はAlloyの勉強なのでGitが実際にこうなっていることを保証するものではない)
sig CommitObj {
tree: one TreeObj
}
sig TreeObj {
blobs: some BlobObj
}
できたできた。
親コミット
じゃあ次は「コミットオブジェクトは1個以上の親コミットを持つ」を実装してみよう。(まあ頭の良い人はすでにこの仕様がバカだと気づいているかもしれないけど、テストドリブンはやっぱり失敗してみないとね)
sig CommitObj {
tree: one TreeObj,
parent: one CommitObj
}
予定していたシナリオと違う失敗の仕方をしたｗｗ
まず「TreeObj」の後のカンマを忘れてシンタックスエラー。それは直した。で得られた結果が上の画像。うむ、親コミットは自分自身ではダメだな。えっと、それはどう書くんだっけ。
これをどこに書くのか(parent: の行に書くのか、pred always_successを書き換えるのか、factを作るのか)について確信が持てないが、まあfactを追加してみた。
fact {
all x: CommitObj | x.parent != x
}
ああー、そうですね、はい。自分の親もその親も自分ではダメ。えーと自分xに対してparent関係を繰り返し適用した集合を作って、自分がその中にいない、って言えばいいのだな。
そういう時に使うのは推移的閉包。 ^r = r + r.r + r.r.r + ... (p.60)
fact {
all x: CommitObj | x not in x.^parent
}
あー、たしかに。コミットオブジェクトがない、ってのはありだな。予定していたシナリオと違うｗ
(余談だがこれを実装するときに「x.^parent = x」と「x.^parent in x」という失敗をした。)
オブジェクトの個数の制約
コミットオブジェクトがいくら以上、というのはどう書けばいいか？？
factで「#CommitObj > 5」と書いてみたらインスタンスが見つからないと言われてしまった。runはforでいくつのインスタンスに対して実験するかを指定できるんだがそれのデフォルトの値ではCommitObjを5個以上、それぞれにTreeObj、BlobObj、とくっつけて大量になってしまうのかな。とりあえずTreeとBlobをコメントアウトして、runにforを指定するようにしてみた。
module nhiro/etude1
sig CommitObj {
parent: one CommitObj
}
fact {
// all x: CommitObj | x not in x.^parent
}
fact {
#CommitObj > 5
}
pred always_success {}
run always_success for 10
ちゃんとウジャウジャでるようになった。じゃ、これでコメントアウトしているfactを復活させてみる。
Executing "Run always_success for 10" Solver=sat4j Bitwidth=0 MaxSeq=0 SkolemDepth=1 Symmetry=20 5743 vars. 110 primary vars. 8718 clauses. 119ms. No instance found. Predicate may be inconsistent. 57ms.
なんか「頑張ってみたけど成立する例が見つからなかった」と言っている。やっと意図した失敗にたどり着いた…。自分の書いたコードが意図したとおりに仕様を表現していて、その仕様にバグがあるのか、それとも自分の記述にバグがあるのか、というのが若干わかりにくいですな。まあ、慣れかな。
さてなんでこれが失敗するかというと、ありがちな境界値のバグがあるわけですよ。一番最初のコミットオブジェクトは親を持たない。それをどうやって表現するかって言うと、えーと。
コミットオブジェクトを分類する
コミットオブジェクトには「最初のコミットオブジェクト」と「それ以外のコミットオブジェクト」があり、後者だけは1個以上の親を持っている、と。extendをつかうんだな。あと、コミットオブジェクトはその両者以外のものが存在しない。だからabstractだな。ref. p.16 階層の導入。
abstract sig CommitObj {}
sig FirstCommitObj extends CommitObj {
}
sig OtherCommitObj extends CommitObj{
parent: one CommitObj
}
あー、そうね。FirstCommitObjは0個または1個しか存在してはいけない。あと今気づいたけど「1個以上の親を持つ」のつもりだったのにoneって書いてあるから「ちょうど1個の親を持つ」になってるじゃん。「1個以上」を表現するのはsomeか。
abstract sig CommitObj {}
sig FirstCommitObj extends CommitObj {
}
sig OtherCommitObj extends CommitObj{
parent: some CommitObj
}
fact {
all x: CommitObj | x not in x.^parent
}
fact {
#CommitObj > 5
}
fact {
#FirstCommitObj < 2
}
うわーー、ま、まあ間違ってはいないけど、現実的なGitリポジトリだと「大部分のコミットオブジェクトについて、親は1つ」なんだなぁ。でもそれってあくまで「大部分は」なので制約じゃないなぁ。どうやって表現するんだろうなぁ。
とりあえず親を2個以下に制約してみる。
だいぶましになったけど、やっぱこれじゃ不足だなぁ。かといって1個以下に制約したらマージが無くなっちゃうし。あ、そうか、親を2個持っているコミットの個数を制約すればいいのか。どうすんだそれ。えーと、集合と述語が与えられて、その集合から述語を満たすものだけを取り出すことが出来ればいいのか。
(演算子の章を眺めているが見つからない)
(本をあたまから読み直している。結構時間が掛かっている)
あっ、そうか内包表記を使うのか。 ref. p.273。「一つ以上の親をもつコミットオブジェクトの集合」は{x: CommitObj | #x.parent > 1}だな。というわけで「親が1個より多いコミットは1個だけ」って制約をつけてみる。
fact {
#{x: CommitObj | #x.parent > 1} = 1
}
できたできた。
これを悩んでいるときに思ったんだけど、FirstCommitObjを作ったのと同じようにabstract OtherCommitObjにして「親が1個のコミットオブジェクト」と「親が2個以上のコミットオブジェクト」を作ることでも解決できるよなぁ、でもそれをやりだすとシグネチャだらけになってキモいし、どんどん実際の実装からかけ離れていくよなぁ、ということで避けたかったのです。で、この制約が内包表記で実現できたってことは、さっきのFirstCommitObjを作るハックも同じように解決できるはず。よしやってみよう。
module nhiro/etude1
sig CommitObj {
parent: set CommitObj
}
fact { // 自分の先祖に自分がいない
all x: CommitObj | x not in x.^parent
}
fact { // 親は2個以下
all x: CommitObj | #x.parent =< 2
}
fact {
#CommitObj > 5
}
fact { // 親を複数持つコミットオブジェクトは1個だけ
#{x: CommitObj | #x.parent > 1} = 1
}
fact { // 親を持たないコミットオブジェクトは最大1個だけある
#{x: CommitObj | #x.parent = 0} =< 1
}
pred always_success {}
run always_success for 10できたできた。めでたしめでたし。
まとめ
教科書の第2章はコードを読まずに操作だけ眺めて、いくつかのAlloyのコードを見て雰囲気を掴んでから3章：論理系と付録B：Alloy言語リファレンスを読んだほうがわかりやすいのではないだろうか…。ここまでやった今でも2章の#n.(b.addr)とか#Name.(b.addr)とかの記法はパッと見て意味がつかめない。この手の研究をしている人にとっては第2章があると他の手法との違いがわかりやすいのか？？
今回やってないこと。runの代わりにcheckを使って「assertが失敗するケース」を探す。両側から狭めていかないと片手落ちだからね。アリティ3以上の関係とかさっぱりイメージできない。どう使うのか。これはAlloyカーネルにコンパイルされる際に2項関係を関数でつなぎあわせたものに変換されるのか？変換されたAlloyカーネルのコードが見たいがそれはどうするのか？none, univ, idenは使ってない。いつ必要になるんだろう。集合演算子も使ってない。あ、inだけ使ったか。関係演算子9種類のうち結合と推移閉包は使った。転置はまあわかる。定義域制限・値域制限・オーバーライドが何に使えるのかピンと来ないので使う例を考えたい。論理演算子もnotしか使ってないな。ま、それはいいか。
あと「親が複数あるコミットは1個だけ」って制約だけに関しては、Gitの仕様ではなくて、実例を探させる上で重点をおいて欲しい範囲に探索範囲を持っていくためのアドホックな条件なのだからコードの上でちゃんと区別するべきだなーと思った。ふむ、そういうばあいにpredを使うのかな。
とりあえずこんな感じ。ご飯の時間だ！
