抽象によるソフトウェア設計／付録 A 練習問題解答例 - Model Base

Model Base内検索 / 「抽象によるソフトウェア設計／付録 A 練習問題解答例」で検索した結果

Alloy Analyzer
抽象によるソフトウェア設計／付録 A 練習問題解答例形式仕様記述ツールAlloy Analyzerの解説本「Software Abstractions」の邦訳「抽象によるソフトウェア設計－Alloyではじめる形式手法」が出版されたので、これを機会に書籍の付録にある練習問題に(興味のある箇所をつまみ食い的に)挑戦してみる。 ⇒抽象によるソフトウェア設計／付録 A 練習問題解答例　　　　　　 Today - Yesterday -
A.1.7 リングを特徴付ける
...zer ] / [ 抽象によるソフトウェア設計／付録 A 練習問題解答例 ] sig Node{ next set Node } pred isRing (){ next.~next in iden -- 単射的 Node - Node in ^next -- 循環可能 } run isRing for exactly 4 Node
A.1.8 無向グラフの非循環性を定義する
...zer ] / [ 抽象によるソフトウェア設計／付録 A 練習問題解答例 ] sig Node {adjs set Node} pred acyclic () { adjs = ~adjs -- 非反射的 no iden adjs -- 全域的 Node in adjs.Node } run acyclic for 4
トップページ
...lyzer 抽象によるソフトウェア設計／付録 A 練習問題解答例形式仕様記述ツールAlloy Analyzerの解説本「Software Abstractions」の邦訳「抽象によるソフトウェア設計－Alloyではじめる形式手法」が出版されたので、これを機会に書籍の付録にある練習問題に(興味のある箇所をつまみ食い的に)挑戦してみる。 ⇒抽象によるソフトウェア設計／付録 A 練習問題解答例　　　　　　 Today - Yesterday -
A.1.6 スパニング木
...zer ] / [ 抽象によるソフトウェア設計／付録 A 練習問題解答例 ] open util/graph[V] as gr -- 頂点の集合Vと辺の集合Eの定義 some sig V{ E set V } -- 辺を持たない頂点は除外しておく fact{ V in E.univ + univ.E } pred isTree (r univ - univ){ gr/tree[r] } pred spans (r1, r2 univ - univ){ r2 = E -- 部分グラフ r1 in r2 -- すべてのノードを通る univ.r2 + r2.univ in univ.r1 + r1.univ } pred show (r, t1, t2 univ -...
A.2.3 囚人の割り当て
...zer ] / [ 抽象によるソフトウェア設計／付録 A 練習問題解答例 ] ( a ) 安全な割り当てを表現する述語safe を完成させ、安全な割り当てとそうでない割り当ての両方の例を生成せよ -- 二人の囚人が異なるギャングのメンバーであった場合、 -- その二人が同じ監房に入ることはない pred safe () { all disj i1,i2 Inmate | let G1 = members.i1, G2 = members.i2 | { -- 二人はギャングのメンバーである some G1 and some G2 -- 二人は同じギャングのメンバーでない G1 not = G2 } = no ( i1.room i2.room ) } ...
A.1.2 関係計算・述語論理形式
...zer ] / [ 抽象によるソフトウェア設計／付録 A 練習問題解答例 ] 本文3.5.2から察するに、"述語論理形式"とは限量子Qを含む Q x e | F の形式のことを指していると思われる。関係rの各性質(非空的、推移的、非反射的、、、)について、 A.1.1の記述と自分で考えた述語論理形式の記述が同値になるか否かの検査記述を以下のように書いてみた。 assert ReformulateOK { all r univ- univ { -- nonempty (some r) iff (some x, y univ | x- y in r) -- transitive (r.r in r) iff (all x, y, z univ | (x- y i...
A.3.3 床屋のパラドックス
...zer ] / [ 抽象によるソフトウェア設計／付録 A 練習問題解答例 ] ( a ) 解析器を使い、モデルが実際に矛盾していることを示せ sig Man {shaves set Man} one sig Barber extends Man {} fact { Barber.shaves = {m Man | m not in m.shaves} } run {}for 4 Man 村人4人の世界でインスタンスは発見されなかった。 Executing "Run run$1 for 4 Man" Solver=minisat(jni) Bitwidth=4 MaxSeq=4 SkolemDepth=1 Symmetry=20 116 vars. 19 primary vars. 167 clauses....
A.3.1 驚くような三段論法
...zer ] / [ 抽象によるソフトウェア設計／付録 A 練習問題解答例 ] Doris Day の歌 Everybody loves my baby but my baby don’t love nobody but me. この歌をいくつかの制約で形式化し、Gries の推論をアサーションにせよ。 Doris Day の歌の主張を述語DorisDay 、「私は私の彼だ」を述語I_am_my_baby、Geriesの推論を示す述語Gries は以下となる。 pred Greies{ DorisDay = I_am_my_baby } "私"や、"私の彼"、"好き"などの構造を以下のように定義すると、 sig Person{ -...
抽象によるソフトウェア設計／付録 A 練習問題解答例
[ Alloy Analyzer ] A.1 論理の問題 A.1.1 二項関係の性質 (省略する) A.1.2 関係計算・述語論理形式 A.1.3 モデリング時の関係的性質 A.1.4 ナビゲーションのリファクタリング A.1.5 木を特徴付ける A.1.6 スパニング木 A.1.7 リングを特徴付ける A.1.8 無向グラフの非循環性を定義する A.1.9 推移閉包を公理化してみる A.1.10 アドレス帳の制約と式 A.1.11 地下鉄をモデリングする A.2 単純なモデルを拡張する A.2.1 電話のスイッチング接続 A.2.2 アドレス帳の不変条件を保存する A.2.3 囚人の割り当て A.3 古典的パズル ...
A.1.5 木を特徴付ける
...zer ] / [ 抽象によるソフトウェア設計／付録 A 練習問題解答例 ] 木の有向グラフを作るにあたって頂点と辺の定義を準備する。 -- 頂点の集合Vと辺の集合Eの定義 some sig V{ E set V } -- 辺を持たない頂点は除外 fact{ V in univ.E + E.univ } 発見的に木を作ってみるまずは、始端は１つだけであるという性質だけを与える。 pred isTreeH(r univ - univ){ let -- ノード NODE = r.univ, -- 始端 START = NODE - univ.r |{ -- 始端は唯一存在する(ルートノードのこと) one START } } こんな...
A.4.1 状態機械の定義
...zer ] / [ 抽象によるソフトウェア設計／付録 A 練習問題解答例 ] 状態機械は、1 つ以上の初期状態と、各状態から次状態への遷移についての関係を持つ。状態機械のAlloy モデルを構築し、制約を追加して解析器に解かせ、以下の様々な状態機械の例を生成せよ。 Wiki Pedia の有限オートマトンで紹介されている数学モデルの表現を参考にして、この問が設定する状態機械を記述してみる。状態機械は単純であり、定義の構成要素は以下の３つのみとなる。 S,s0,δ S は有限であって空でない状態の集合 s0 はSの要素でもある初期状態の集合 σ は状態遷移関数 σ S→P(S) 　ただしP()は冪集合(イベントの集合Σは要素が１つなので、σ S×Σ→P(S) を σ S→P(S)　とした) ...
A.2.1 電話のスイッチング接続
...zer ] / [ 抽象によるソフトウェア設計／付録 A 練習問題解答例 ] ( a ) 述語を１つ追加してコマンドを起動することで、モデルをシミュレーションせよ通話と接続に関する基本的なルールを述語basic で定義し、つまらないインスタンスを避けるための環境設定を述語environment で定義した。 sig Phone { requests set Phone, connects lone Phone } pred basic{ -- 通話に関する根本的な制約 -- 非反射的 no iden connects -- 接続要求に関する根本的な制約 -- 非反射的 no iden requests } pred environment{ -- 接続要...
A.1.3 モデリング時の関係的性質
...zer ] / [ 抽象によるソフトウェア設計／付録 A 練習問題解答例 ] これらは、問題領域の用語解釈によって答えが変わってくる。 ( a ) sibling：同じ両親を持つ子供の間の兄弟関係議論領域を"ある両親から生まれた子供たち全員"と考える。一人っ子のケースは除外する。以下、兄弟関係rに制約を与える性質を検討すると、 (ここでは、姉や妹も兄や弟と呼ぶことにする) 同じ両親から生まれた子供のペアは兄弟関係なので、rは非空的でない自分自身のことを自分の兄弟とは呼ばないので、rは非反射的自分の兄(or弟)にとって自分は兄弟なので、rは対称的自分の兄の弟が自分の場合、自分自身を兄弟と呼ばないので、rは推移的でない(rが非反射的かつ対称的なら、同時に推移的になれないので、推移...
A.3.6 外科医のグローブ
...zer ] / [ 抽象によるソフトウェア設計／付録 A 練習問題解答例 ] 設問ある外科医が3 人の患者を手術しなければならないが、2 組のグローブしかない。二次汚染はあってはならない。つまり、外科医はどの患者の血と接触してもならないし、どの患者も他の患者の血と接触してはならない。外科医は手術に両手を使う。この外科医はどうすべきか？この問題をAlloy で表現し、解析器を使って解を見つけよ。モデル化の方針求められているのは "外科医はどうすべきか？" なので、"外科医がすること"のイベント列を提示すればよい。書籍の2.4 や6.1.3で紹介されているように、util/ordering ライブラリモジュールを用いて全順序関係となる○○列の存在を宣言する。この問では、特定...
A.1.11 地下鉄をモデリングする
...zer ] / [ 抽象によるソフトウェア設計／付録 A 練習問題解答例 ] ( a ) 路線line にある駅の集合がS である "路線line上の駅の集合はSである" という述語を定義する。路線lineの各区間の始端の集合は line.univ 、各区間の終端の集合は univ.line となる。路線lineの駅の集合は始端と終端の和集合となる。 pred stations[line univ- set univ, S set univ]{ let Points = univ.line+line.univ | S = Points } ( b ) line には切れ目がない "路線lineには切れ目がない" という述語を定義する。路線の走...
A.4.2 状態機械の模倣関係
...zer ] / [ 抽象によるソフトウェア設計／付録 A 練習問題解答例 ] ( h ) トレースを定義した状態機械のAlloy モデルを作成し、状態機械の例と関連するトレース集合をいくつか生成してみよモデル化の方針まず、遷移ラベルと状態は以下のように定義する。 sig A{} abstract sig State{} この設問で考えさせられたのはトレースの表現であった。設問内の定義によれば状態機械のトレースとは、初期状態からはじまる遷移ラベルからなる有限列ということである。これを算出するには、状態機械がたどった遷移の履歴(これを経路と呼びたい)、から遷移ラベルを抽出すればよい。いま状態機械の遷移の表現を A - State - State とするなら、状態機械の経路の...
@wiki全体から「抽象によるソフトウェア設計／付録 A 練習問題解答例」で調べる