Alloy
視覚的なフィードバックを得られるので初学者に易しい
開発チーム
Project director
参考
>#WIP
Alloyのあるきかた
公式tutorialをざっとやる
(Alloy4なので一部syntax errorになる)
Alloyの概要を掴む
細かい文法知識を入れる
Alloy6の変更点等を知る
実際に書いてみる
Alloy4の頃のコードをAlloy6で書き直してみてみると良さそう
その後、モデルや時相論理等など本題のところを深ぼっていく
syntaxの理解があやふやなままで厳密な記述を仮説的に読み取ってもあまり意味がなさ気なので
>Alloy はZ 記法などの他モデル規範形式仕様言語と同様、手続きの機能仕様やデータの静的な構造の表現を目的とする。基礎となるロジックとして1階関係論理(First Order Relational Logic) を導入し、言語の意味定義を簡単化した.1階関係論理は1階述語論理と同等であり，その論理式の真偽判定を自動化することは原理的に不可能である。そこで，有限スコープ仮説を導入して，有限モデルに限定した範囲で自動検査する、命題論理式に変換することで，真偽判定を制約充足問題に帰着し、SAT ソルバを用いる方法を採用した。
ググっても一階述語論理しか出てこないな
英語だとちょっとだけひっかかる
> 一般に1階述語論理をソフトウェアの仕様記述に適用する場合、再帰的な定義を取り扱えないことが問題となる。(..中略..) 木造で非循環（Acyclic） なことを表現する場合、親子関係を推移的に辿る必要がある。2 項関係の推移閉包を表現できればよい。1階述語理に推移閉包オペレータを追加した推移閉包論理（Transitive Closure Logic) 83)と同様，Alloy は1階関係論理に推移閉包オペレータを加えた。
記述の順序は関係ない
comment
Instance
traceとも呼ばれる
ModelというのはInstanceの集合、と捉える
Modelの具体例がinstanceってことかな
Modelを定義してrunすると、指定した探索範囲下で有効なinstanceを自動的に見つける
その結果がAlloy Visualizerで見れるやつ
insntaceが見つからなかった場合は、
与えられた探索範囲内でmodelの制約を満たす状態が存在しないということを意味する
Modelが矛盾してるか、探索範囲が適切でないか
instanceが見つかった場合、
見つかったね、というのはわかるが、それが正しいかどうかはまだわからない
instanceを実際に見た上で判断が必要(?)
>An instance (..) is an infinite sequence of states
これは良くわからん
間がModelを書いて、Alloyがinstnaceを提示してくれた後のアクションはどういうものだろうか
まだ簡単な例しか見てないけど
modelに対して、想定してなかったinstanceが返ってきた時、
「君のmodelは、こういう例も包含する(ぐらい甘い)けど、それでもok?」と問われてる感じか
想定しているケースは包含してるが、不要な例も包含してるよ、という
後者のことをcounterexamples (反例)と呼んでる
それを見た上で、もっと厳格な仕様にしよう、となるのか
modelに対して、instanceが得られなかった時
単純にmodelが矛盾してるので修正するしかない
こちらはわかりやすい気がする
Relation Logic
alloypred noRefferedTo (x: Composite) {
no c: Composite | x in c.children
}引数として与えたCompositeをchildlenから参照するようなcが存在しない
alloypred onlyRoot {
no c: Composite - Root | noRefferedTo[c]
}Root以外のCompositeは、述語noRefferedToを満たさない
Composite - Root で、「Root以外のCopmosite」を表す要は、RootだけnoRefferedToを満たすということ
二重否定なので分かりづらい
alloypred singleWholeNG {
all x: Component | one c: Composite | x in c.children
}∀x, ∃cに対して
x in c.children ということ定数
none 空集合
論理演算子
not and F and G and H を {F G H} とかける or 含意を意味する
p implies A else B は とも書ける3項演算子みたいなもの
p ? A : B と同じ入れ子にもできる
同値
2つの項がbooleanであるときの
= と同じ P iff Q は、P,Q両方がtrue、P,Q両方がfalseのときに、trueになる濃度
# で、その関係が持つタプルの数を得られるe.g.
#g.address e.sum 整数の集合
e の総和