※上記の広告は60日以上更新のないWIKIに表示されています。更新することで広告が下部へ移動します。

更新日 2011-09-03
[ Alloy Analyzer ] / [ 抽象によるソフトウェア設計/付録 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. 297ms.
  No instance found. Predicate may be inconsistent. 0ms.

( b ) 村人を男(髭を剃る必要がある者)と女性(必要のない者)に分けた新たなモデルを作成し、今度は簡単な解があることを示せ

abstract sig Person{}
sig Woman extends Person{}
sig Man extends Person{shaves: set Man}
one sig Barber in Person {}
fact {
  Barber.shaves = {m: Man | m not in m.shaves}
  }
 
run {}for 4 Person

女性が床屋になってくれたことで解が現れた。


( c ) もっと抜本的な解がEdsger Dijkstraによって示された。それは、床屋がいない可能性を許容するというものだ。これに従って最初のモデルを書き直し、解が得られることを示せ

one sig Barber から one をとる。

sig Man {shaves: set Man}
sig Barber extends Man {}
fact {
  Barber.shaves = {m: Man | m not in m.shaves}
  }
 
run {}for 4 Man


( d) 最後に、元のモデルで複数の床屋がいるような変更を試して、やはり解が得られることを示せ

sig Man {shaves: set Man}
sig Barber extends Man {}
fact {
  -- 複数の床屋がいる
  #Barber > 1
  Barber.shaves = {m: Man | m not in m.shaves}
  }
 
run {}for 4 Man

なんだが、法規制の盲点をついた○○のようだ。。。






















|新しいページ|検索|ページ一覧|RSS|@ウィキご利用ガイド | 管理者にお問合せ
|ログイン|