あろい
最近爆発的に盛り上がっているAlloyをやってみる。どこでとかは知らないけれども爆発的に盛り上がっている事は間違いない。
今現在 6:17 リアルタイムに色々書いて行く。
そもそもあろいって何?
全く分からない。全くっていうのは、情報が何も無いという事です。勝手に予測する。
爆発的に盛り上がるのがプログラミング言語の筈は無い。プログラミング言語とかは大体殺し合いなのでそんな事は無い。どうでも良い。多分言語言語したものでは無いと思う。
そうであって欲しい。
調べる
http://alloy.mit.edu/community/
ふーむ。まさちゅーせっちゅ！！か。あれ、まさちゅーちぇっちゅでしたっけ。。。
なにやらアナライザがあるらしい。アナライザってなんや！！多分まぁなんか補助ツールでしょう。多分GUIGUIしてるんでしょうね。
そんでもって、現在はメジャーヴァージョンで4らしいです。
チュートリアル
http://alloy.mit.edu/alloy4/tutorial4/
まずはチュートリアル読め...な??
いいえチュートリアルを読む前に適当にほじくり回す方が良い筈です。
ここから入手する。Javaで開発されてるんですね。
ああなんか、SATとか書いてる。Logicかな。SATベースな実装?
モデルチェッカ??
わけわからんからTutorialを読むでござる。
Lesson 0
"lead by mistake" 何格言みたいなこと言ってるワケ?嘘です意味分かりません。
なんか調子載って作っちゃったモデルとかいうものには往々にしてミステークがあって、実際にチュトリアルとしてはどんなミステークがあるかはっきりさせつつ、何でそんなんが出て来たのかも見ましょうね、という感じらしい。
Alloyは仕様記述言語・・・だという事なのかな。
で、checkは常にfiniteなscope(scope は sizeらしい。意味が??)に対して全探索的に行われる。counter example(反例)となるようなモデル(モデルっていうか、インスタンス??)を決して逃しはしない...と。
うーんそこでSATなのかな。SATはまぁ良く知りませんが、Prologの実装の時にもちょびと見たなぁ。
"infinite model"っていうのが分かりませんね。
それと、「ダサい」仕様記述言語みたいな感じじゃなくて割と気軽に(プログラマ的な意味で)書けるという所がウリなのかしら。
finite scope check と infinite modelの関係が...。
Operational と Declarativeの違いも分かりません。makeとかrecognizeとか日本語でおk
Lesson1
なんでasyclicがpassするのかが分からない。頭痛が痛い。
意味が分かったカモ
まず、sig FSObjectから全てのFSObjectは0個もしくは1個の親(parent)を持つ「必要がある」。いや義務か。親の型はDir
0 or 1なのは、keyword "lone"の所為ですね。
で sig DirとしてDirにはcontentsというメンバがあって、それはFSObjectの集合であると。
で、contentsに関するfactが存在していて、これが何を要請しているかというと、あるDirのインスタンスdのcontentsの要素それぞれは、そのparentとしてdirを持つという事。
じゃあ sig Rootを作らずにcheckを走らせてみると、通常RootとなるようなDirを含むモデルがcounter exampleとして吐かれる。
問題なのは
「factとしてはcontentsがparentを持つとしか書いてないのに、何勝手にそういうモデルが作られるわけ?」← loneなんだから、勝手にRootみたいなmodelも作られる筈[だけど落ち着いて考えると、1つの時のケースがcounterに成ってるわけで、全仕様を満たして初めておkになるんだから、こっちの方が本当は正しいんだなぁ。] <=> 仕様から起こりうるものが想定している事象(この場合はassert)を満たさない時が１つでもあったら困る。
なんかごちゃごちゃ書いてるけど、今の所sigがデフォルトの知識で、factが例外と言った方が良いんでしょうね多分。
「おいィ?お前らは閉世界仮説(CWA.書いてない事は偽 Prologはコレですね。多分)の方が好きじゃないのか?」なので多分これはCWAに成ってますね。Rootを書かなかった時はsigから構築出来て、それがassertアボソ
「お前それで良いのか?」
とか独りでやってたんですけど、でもFSObjectはDirを持つんだよ！！これがFSObjectだよ！！って書いてるんだから、そうなのかなぁ・・・。
とすると、factっていうのは優先度的に高い、という事ですかね。
なんかこの辺がDeclarativeな感じがする。
で、ここで
sig FSObject { parent: Dir } // loneを抜き取ったので、全てのFSObjectはparentを持つ必要がある。としてもcounter exampleは見つからなかった。
「じゃぁよぉone sig Root extends Dir { } { no parent }のnoってのは何なんだぁ??」
分かりません。デフォルト論理かな?
In the "appended fact" (in braces after the signature body)
英語とかマジ空気だな
"appended fact syntax"とか書いてある。
sig name {
// fields of the signature
}{
// appended fact constraints
}
sig Person {
closeFriends: set Person,
friends: set Person
}{
closeFriends in friends
}
これは
sig Person {
closeFriends: set Person,
friends: set Person
}
fact {
all x:Person | x.closeFriends in x.friends
}
これと等しいらしい。
ああていうか、そうか。factを追加するっていうのは、sigにより作られた世界を非単調にするのも否めないぞみたいな感じなんですね。
そりゃそうか。否めないっていうか、割と何も考えてない。でそれをlogicな言葉にするとそうなりますね。
"less than or equal to one"でloneらしい。格好いい。
If you don't understand why something does (or does not) follow from the model, then you don't understand your subject matter enough.
understandってどのくらいなんだろう。証明とか出来れば良いのかな。ていうか証明出来れば上出来か。
でも結局分かったつもりに成ってたらどうしようも無いし・・・。でもまぁその"つもり"はSAT的にfiniteなspaceを調べれば分かるか。
とは言え、割と手狭な範囲だけしか見れない気がするんだよなぁ・・・。SATだと。
つまり、適当な戦略の元に証明する方が証明出来る空間は広そうな(SATに対する現実時間を考えると)気がするんですけど、実際の所どうなんだろう。でも複数のcounter exampleを作るとかだったら、やっぱりSATのが良いのかな。
チュートリアル飽きた
のでなんかやろうと思ったけど、一番最初のチュートリアル読んだぐらいではちょっとAlloyであれやこれやが分からないので、凄く簡単そうなのをやってみたら凄く簡単だった。
//3つの人形 A,B,Cがある。
//この問題は、それぞれの人形の髪の色を考えるものである。
//3つの人形の髪の色はそれぞれ異なっており、髪の色はBrown Blond Black
//Cの髪はBlackでもBlondでも無い というのと Aの髪がBlackで無い事が分かっている
sig Color { }
one sig Brown extends Color { }
one sig Blond extends Color { }
one sig Black extends Color { }
fact { Brown + Brond + Black = Color }
sig Dall { hair : Color }
one sig A extends Dall { }
one sig B extends Dall { }
one sig C extends Dall { }
fact { all a : Dall | all b : Dall | a != b => a.hair != b.hair }
fact { C.hair != Black and C.hair != Blond }
fact { A.hair != Black }
pred show() { }
run show for 0簡単過ぎて駄目ですね。
ていうかsignatureをexntendsしたものでやってのけるって・・・なんか型レベルっぽいっていうか・・・値レベルって感じじゃないよなぁ・・・。
sig Person { a : Doll , b : Doll }
one sig P extends Person { }
one sig Q extends Person { }
one sig R extends Person { }
fact { P + Q + R = Person }
fact { all p1 : Person | all p2 : Person |
p1 != p2 => p1.a != p1.b and p1.a != p2.a and p1.a != p2.b and
p1.b != p2.a and p1.b != p2.b }
fact { Q.a = C or Q.b = C }
fact { (R.a.eye = Ao and R.a.hair = AshBlond) or (R.b.eye = Ao and R.b.hair = AshBlond) }
fact { one p : Person | (p.a = D and p.b.eye = Midori) or (p.b = D and p.a.eye = Midori) }
fact { one p : Person | (p.a.eye = Heiz and p.b.hair = Kuro_) or (p.a.hair = Kuro_ and p.b.eye = Heiz) }
sig Doll { eye : EyeColor , hair : HairColor }
one sig A extends Doll {}
one sig B extends Doll {}
one sig C extends Doll {}
one sig D extends Doll {}
one sig E extends Doll {}
one sig F extends Doll {}
fact { A + B + C + D + E + F = Doll }
fact { E.hair != LightBrown }
fact { C.hair = Blond }
fact { one d : Doll | d.eye = Ao and d.hair = AshBlond }
sig EyeColor {}
one sig Kuro extends EyeColor {}
one sig Cha extends EyeColor {}
one sig Ao extends EyeColor {}
one sig Midori extends EyeColor {}
one sig Heiz extends EyeColor {}
one sig Gray extends EyeColor {}
fact { Kuro + Cha + Ao + Midori + Heiz + Gray = EyeColor }
fact { all a : Doll | all b : Doll | a != b => a.eye != b.eye and a.hair != b.hair }
sig HairColor {}
one sig Brown extends HairColor {}
one sig LightBrown extends HairColor {}
one sig Blond extends HairColor {}
one sig AshBlond extends HairColor {}
one sig Kuro_ extends HairColor {}
one sig Aka extends HairColor {}
fact { Brown + LightBrown + Blond + AshBlond + Kuro_ + Aka = HairColor }
fact { one p : Person | p.a = A and p.b.eye = Kuro }
fact { one p : Person | p.a = B and p.b.hair = Brown }
fact { one p : Person | p.a.hair = LightBrown and p.b.eye = Cha }
pred show {}
run show for 1uniqueになった。ちなみにこの2つの出典はブルーバックスの論理パズル101です。
取りあえず、one sig 〜 なのは、全てインスタンスみたいな感じで使ってます。つまり、SuperClassから見たSubClassっていうのは、普通のプログラミングにおけるTypeとそのInstanceみたいな感じになってて・・・。悲しい。
色々と訂正
さかいさんからコメント貰って、その通りなんですが、CWAとかは違いますね。
そもそも、Alloyのアプローチとしては「記述された仕様」を「充足するモデル」がガンガン作られて行って、それがassertに引っかからないかみたいな感じだと思うので、なんかCWAとかその意味で見ると違うよなーみたいな。
上の例だと(というかまだ私はAlloyで他に何が書けるかとか知らんのですが)sigとfactを満たすものから作られたモデルが、acyclicというassert(これは正しいと信じられるモノ)を満たさない時にcounter exampleとなるので。
モノと、その関係を述べて行って(その意味で、Object OrientedとAlloyのチュトリアルに書いてたんだろうか)、assertは「分からない事を聞く」んじゃなくて「そうであるべき」という事を投げてるのでなんかそういう意味でアプローチは違うから、更にそういう意味からCWAとかでは無い??
