alloyの勉強

全体的に、情報が断片的で、全体像が分かりにくい

しつこくリンクを巡っておく必要がある

筆者本人が、体系的なdocumentを書くのが苦手か、

そもそもやってることが難しいから、誰が書くにしてもそうなってしまうか

community

やっぱ読んだほうが良かったなこれ

全部atom かrelation(orderd tuple)

それを、集合の関係を表現したり

さらにOO的な関係性をも示してる

すごい

RDBよりもよっぽど良い感じに関係を扱ってる感じ？

目的が違うが

tutorial中に登場するtips

３レベルの抽象

オブジェクト指向

集合論

atomと関係

code:als

sig S extends E {

F: one T

}

fact {

all s:S | s.F in T

}

これを３段階で説明してるが

最後のatomとrelationの説明が一番腑に落ちた

S is an atom (and so is E)

the containment relation maps E to S (among other things it does)

F is a relation from S to T

the containment relation maps S to s (among other things)

. composes relations

s.F composes the unary relation s with the binary relations F, resulting in a unary relation t, such that the containment relation maps T to t

集合論をどうやって表現してるかと言うと、

集合自体をatomで表しつつ

包含関係などを、atom間の某で実現している

Sという集合　という概念はあるが、Sの要素を列挙するわけではない

あくまで、atomを作ってて

Sを用いたいろんな記述をする上で、S atomとs atomをいろいろ対応付けするとかしてる

すべてはatom or relation

atomは１項の関係とみなせば、全部relation

Alloy 6で入ったmutable fields, 線形時相論理がわりとデカい変更

これが使えるなら、これ以前の時間を扱ったあらゆるexample, tutorialが古いコードになる

公式tutorialでさえ

全然更新されてないのでウーンという感じ

いまAlloy 6対応した本を書いてるんだっけ？

ということで、これは絶対理解しないといけない

別に、古いコードも動くのだが

古典論理と関係代数が分かってれば難しくなかったが、時相論理の操作が難しい

公式外

こっちのほうが一般的なドキュメントって感じ

読んだけど、こっちのほうがわかりやすい

この記事かいたひと

mutable fieldの説明もある

haslab

haslabはalloy 6で入った線形時相論理の拡張を作ってたとこっぽい

本で見た例が出てくる気がする

ある程度alloyを理解しないとむずそう

alloy4fun

crossing riverをmutable fieldで書き換えるのをやってる

途中で、そもそも頭の中の考え方を変えないといけないのが分かった

たぶんHaskellとかと近い

述語や事実を宣言的に述べるだけで良い

分岐などを手前で考えるより、富豪的に述語をつなげる

述語の内側で、ありえない状態を否定するように事実を宣言すれば良い

内部的にはSATソルバが頑張ってくれる

たとえば、Farmerがいる方からいない方へのmoveというのを

こうしない

code:alloy

let farmerSide = Farmer in s.far => s.far else s.near | ...

こうかく

code:alloy

Farmer in from // これでいい

some x in from {

///

}

}

あとは、こうかけば、farかnearの移動が記述できる

ほんとか？

動くが、適切な実践であるかはわからない