『形式手法入門』
https://gyazo.com/c2a2153ab418e167f3b6291af3931b9f
2012/4/20
パラ読みした感じ4章あたりが一番興味あるところだろうmrsekut.icon
Alloyの入門書だが、文法に対する解説がなさすぎる
それぐらい自分で調べろハゲタコってことなのかな
tutorialには簡単な文法の話もある
Alloyの入門書ではないのかmrsekut.icon
割とAlloyの知識を前提しているようにも読める
別でAlloyの知識を得てから戻ってくるか
1章 論理で考える
この本では「数理論理」のことを「ロジック」と呼ぶ
複雑さに対処する方法としての抽象化
数理論理学の専門的な知識を要すると工学面での広がりがないので支援ツールを用意した、という経緯らしい
1.2
↑こういう俯瞰図を提示してくれるだけでもありがたいmrsekut.icon
2章 指先で考える
性質を発見することと、それをAlloyとして記述することの2点のムズカシサがあるなmrsekut.icon
Compositeパターンの例でも3つの性質を挙げられているが、その性質の発見がまず難しいし、それを論理式で表現するのも難しい、
また単に慣れてないのでそれをAlloyとして表現するのも難しい
後者は、初めて別のパラダイムに触れたときの感覚に近い
前者はたぶんそもそも難しい
check prop2 for 5
queueやstackの表現
図2.6全然意味がわからない
コード見たらわかった
これなるほど
code:alloy
pred push (s1, s2: Stack, v: Value) {
some e1: Entry | e1.value = v && e1.next = s1.root && s2.root = e1
}
s1とs2を、Stackの状態として述語として表現する
生成される図の意味がわからない
https://gyazo.com/17f189ef58695747e5992d786a11efb2
サンプルコードにミスが多すぎるなmrsekut.icon
3章 機能仕様を論理で考える
4章 リファインメントを検査する
5章 オブジェクト指向デザインを検査する
6章 振る舞い仕様を検査する
7章 プログラム検査を論理で考える
付録A モデル規範形式手法の流れ
形式仕様記述言語
証明支援ツール