付録A 練習問題続きます。終わるのかなこれ。 A.1.11 地下鉄をモデリングする 路線 line にある駅の集合が S abstract sig Station { line: set Station } sig S extends Station {} { S = line } line には切れ目がない run C { all disj x, y: S, z: S | y…

付録A 練習問題続きます。 A.1.10 アドレス帳の制約と式 まず不変条件を記述 abstract sig Name { address: set Addr + Name } sig Alias, Group extends Name {} sig Addr {} fact { -- 循環がないこと(addressの推移閉包に自分が含まれない) no n: Name | …

付録A 練習問題続きます。 A.1.9 閉包推移を公理化してみる 閉包推移は一階論理で公理化できない。のでできないのだけどやろうとして失敗してみるというもの -- 推移被覆 pred transCover (R, r: univ -> univ) { r in R -- R は r を含む R.R in R -- R は…

付録A続きます。 A.1.6 スパニング木 ここに書いてある定義だけではスパニング木の仕様はよくわかりませんでしたがこういうことかな pred isTree (r: univ -> univ) { r.~r in iden no iden & r no x: univ | univ in x.^r } pred spans (r1, r2: univ -> un…

付録A続きます。 A.1.5 木を特徴付ける 単射的である(親ノードは1つ)というのすぐ出てきたのですが、循環を防ぐための ^ 演算子(推移閉包)を使う書きかたがなかなか出てきませんでした pred isTree (r: univ -> univ) { r.~r in iden -- 単射的 no iden & r …

付録A続きます。 A.1.2 関係計算・述語論理式 単射的 (r.~r in iden) は以下の述語論理式で表現できる all x, y: univ | no z: univ | x -> y in r and x != z and z -> y in r 全域 (univ in r.univ) は以下の述語論理式で表現できる all x: univ | some y:…

今日から付録Aを読みます。 A.1.1 二項関係の性質 「推移的」と「非反射的」はそれぞれ削ると他の性質を満たすことができる A.1.2 関係計算・述語論理式 「非空的」は例として挙がっているとおり some x, y: univ | x -> y in r 推移的 (r.r in r)は以下の述…

今日は 6.4.6 履歴変数からです。 固定サイズメモリモデルの抽象モデル準拠の証明はそのままだとできない。固定モデルは初期状態から全てのアドレスが任意の初期値への対応を持つため unwritten という「既にそのアドレスに書き込みされたか」というフィール…

今日は 6.4.4 抽象化関数の簡単な紹介からです。 具体的なメモリモデルから抽象的なモデルの関連付け 具体的なモデルでの操作が抽象的なモデルの操作に対応していることを示す 抽象化関数 具体的なモデルでの状態を抽象的なモデルの状態に対応付ける関数(alp…

今年最初の朝読書です。今年はもうちょっと多く読めるといいなぁ。今日は 6.4 メモリの抽象化のところからです。 メモリを Addr と Data のアトムの対応付けとしてモデル化する パラメータ付きモジュールにして Addr, Data のシグネチャはパラメータとして受…