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