以上のようにFO8Mの構造の分析に従い、FO8Mの理論とFO8Mで用いられるデー タ構造の定義を行った。また、それぞれのデータが持つ性質をデータ構造上に成立する定 理として定義した。実装の例では、オブジェクトモデルの構成要素を例にとり解説した が、基本的に他のモデルでも同様の構造を持つため、同様の方針で構築できる。最終的 に、FO8M の理論をHOL上に構築でき、FO8Mのモデルに関する検証フレームワーク が実装できた。
第
6章
検証フレームワークを用いた検証例
この章では、簡単な例題を用いて、構築した検証フレームワークにおける、モデルの検 証の例を示す。モデルの表現に関しては、FO8Mの定義は青木のFO8Mの仕様書に従う。
6.1
例題
例題として、簡単な電気スタンドを考える。その仕様は以下に従う。
スイッチを1つとライトを1つ持つ。
スイッチはトグル式で押すごとにオン状態とオフ状態が切り替わる。
スイッチがオン状態になるとライトが付き、オフ状態になるとライトが消える。
この電気スタンドの分析モデルを次節以降で示す。各分析モデルにはOMTの表記と、
FO8Mの表記、そして検証フレームワークでの表記で示す。
6.1.1
基本オブジェクトモデル
FO8Mの表記による基本オブジェクトモデル
l ight =(Stand;(Bl ub;Switch))
Stand
Blub Switch
status turn push
status
図6.1: OMTの記法で記述したオブジェクトモデル
Bulb =((status);(tur n))
Switch=((status);(push))
検証フレームワーク上の表記による基本オブジェクトモデル
(--`AGGR_MAP (AGGRID "light")
(AGGR (CLASSID "Stand")
[ (CLASSID "Bulb");
(CLASSID "Switch")]) `--)
(--`CLASS_MAP (CLASSID "Stand")
(CLASS [ ]
[ ]) `--)
(--`CLASS_MAP (CLASSID "Bulb")
(CLASS [ (ATTRID "status") ]
[ (FUNCID "turn") ]) `--)
(--`CLASS_MAP (CLASSID "Switch")
(CLASS [ (ATTRID "status") ]
[ (FUNCID "push") ]) `--)
ON OFF
pushbutton / poweron switchon pushbutton /
poweroff switchoff STDswitch
ON OFF
poweron / φ turnon poweroff /
φ turnoff STDbulb
図6.2: OMTの記法で記述した動的モデル
6.1.2
基本動的モデル
FO8Mの表記による基本動的モデル
STDswitch = (State;Evt
in
;Evt
out
;Act;Cond;Tr ans;OFF)
wher e State=fON;O FFg
Evt
in
=fpushbuttong
Evt
out
=fpoweron;power offg
Act=fswitchon;switchoffg
Cond=fg
Trans=
f(OFF !ONjpushbutton[]=pow eron switchon])
(ON !OFFjpushbuttoff[]=power off switchoff])g
STD bulb = (State;Evt
in
;Evt
out
;Act;Cond;Trans;OFF)
w here State =fON;OFFg
Cond=fg
Trans=
f(OFF !ONjpoweron[]= turnon])
(ON !O FFjpoweroff[]= turnoff])g
検証フレームワークの表記による基本動的モデル
(--` STD_MAP (STDID "STDswitch")
STD [(STATEID "ON");(STATEID "OFF")]
[(EVENTID "bushbutton")]
[(EVENTID "poweron");(EVENTID "poweroff")]
[(ACTID "switchon");(ACTID "switchoff")]
[]
[(ST (STATEID "OFF") (STATEID "ON")
(DEF_EVT (EVENTID "pushbutton"))
(CONDID "") (DEF_EVT (EVENTID "poweron"))
(ACTID "switchon"));
(ST (STATEID "ON") (STATEID "OFF")
(DEF_EVT (EVENTID "pushbutton"))
(CONDID "") (DEF_EVT (EVENTID "poweroff"))
(ACTID "switchoff"))]
(STATEID "OFF") `--)
(--` STD_MAP (STDID "STDbulb")
STD [(STATEID "ON");(STATEID "OFF")]
[(EVENTID "poweron");(EVENTID "poweroff")]
[]
[(ACTID "turnon");(ACTID "turnoff")]
[]
[(ST (STATEID "OFF") (STATEID "ON")
(CONDID "") (EMPTYEVENT)
(ACTID "turnon"));
(ST (STATEID "ON") (STATEID "OFF")
(DEF_EVT (EVENTID "poweroff"))
(CONDID "") (EMPTYEVENT)
(ACTID "turnoff"))]
(STATEID "OFF") `--)
power
switch bulb
図6.3: OMTの記法で記述した機能モデル
6.1.3
基本機能モデル
FO8Mの表記による基本機能モデル
((switch;bul b);power)
検証フレームワーク上の表記による基本機能モデル
(--` DATAFLOW (PROCESS_NODE (PROCESSID "switch"))
(STORE_NODE (STOREID "bulb"))
(DATAID "power") `--)
6.1.4
統合モデル
FO8Mの表記による統合モデル。
状態遷移図の統合写像
Switch7!STDsw itch
Bul b7!STDbul b
アクション式
Sw itch:status :=Switch:push(Switch:status)
Bulb:status:=Bul b:turn(Bul b:status)
アクション式の統合写像
switchoff 7!Switch:status:=Sw itch:push(Switch:status)
switchon7!Sw itch:status :=Switch:push(Switch:status)
turnon7!Bul b:status:=Bul b:turn(Bulb:status)
アクターの統合写像
switch7!((Sw itch:status);(Switch:push))
データストアの統合写像
bulb7!((Bul b:status);(Bul b:turn))
検証フレームワークの表記による統合モデル 状態遷移図の統合写像
(--` ISTD (CLASSID "Switch") (STDID "STDswitch") `---)
(--` ISTD (CLASSID "Bulb") (STDID "STDbulb") `---)
アクション式
(--` ASSIGN_AO (CA (CLASSID "Switch") (ATTRID "status"))
(REF_FO (CF (CLASSID "Switch") (FUNCID "push"))
(REF_AO (CA (CLASSID "Switch") (ATTRID "status"))))
`--)
(--` ASSIGN_AO (CA (CLASSID "Bulb") (ATTRID "status"))
(REF_FO (CF (CLASSID "Bulb") (FUNCID "turn"))
(REF_AO (CA (CLASSID "Bulb") (ATTRID "status"))))
`--)
アクション式の統合写像
(--` IACTION (ACTID "switchon")
(ASSIGN_AO (CA (CLASSID "Switch") (ATTRID "status"))
(REF_FO (CF (CLASSID "Switch") (FUNCID "push"))
(REF_AO (CA (CLASSID "Switch") (ATTRID "status")))))
`--)
(REF_AO (CA (CLASSID "Switch") (ATTRID "status")))))
`--)
(--` IACTION (ACTID "turnon")
(ASSIGN_AO (CA (CLASSID "Bulb") (ATTRID "status"))
(REF_FO (CF (CLASSID "Bulb") (FUNCID "turn"))
(REF_AO (CA (CLASSID "Bulb") (ATTRID "status")))))
`--)
(--` IACTION (ACTID "turnoff")
(ASSIGN_AO (CA (CLASSID "Bulb") (ATTRID "status"))
(REF_FO (CF (CLASSID "Bulb") (FUNCID "turn"))
(REF_AO (CA (CLASSID "Bulb") (ATTRID "status")))))
`--)
アクターの統合写像
(--` IPROCESS (PROCESSID "switch")
([(CAE (CLASSID "Switch") (ATTRID "status"))],
[(CAE (CLASSID "Switch") (ATTRID "push"))]) `--)
データストアの統合写像
(--` ISTORE (STOREID "bulb")
([(CAE (CLASSID "Bulb") (ATTRID "status"))],
[(CAE (CLASSID "Bulb") (ATTRID "turn"))]) `--)
6.1.5
検証例
この節では、前節までで示されている分析モデルを例にして、検証フレームワークによ る実際の検証手順を示す。-は検証フレームワークでのプロンプトを示す。
基本オブジェクトモデルにおけるBulbクラスがStandクラスの部品クラスかどうかを 検証する。
まず、集約関係式をモデル情報として証明の前提とし、証明したい事項を結論として証 明のゴールを設定する。ここで、gはHOLの証明のゴールを設定する関数である。
[ (CLASSID "Bulb");
(CLASSID "Switch")]) ==>
(IS_COMPONENT (CLASSID "Bulb") (CLASSID "Stand"))`;
val it =
Status: 1 proof.
1. Incomplete:
Initial goal:
(--` (DEFINE_AGGR (AGGR (CLASSID "Stand")
[ (CLASSID "Bulb");
(CLASSID "Switch")])) ==>
(IS_COMPONENT (CLASSID "Bulb") (CLASSID "Stand"))`--);
: proofs
まず、証明のゴールの形を変形する。
- e STRIP_TAC;
OK..
1 subgoal:
val it =
(--`IS_COMPONENT (CLASSID "Bulb") (CLASSID "Stand")`--)
____________________________
(--`DEFINE_AGGR
(AGGR (CLASSID "Stand") [CLASSID "Bulb"; CLASSID "Switch"])`--)
: goalstack
つぎに、集約関係の部品関係IS COMPONENTの定義で書き換えを行う。
- e (REWRITE_TAC [IS_COMPONENT_DEF]);
OK..
1 subgoal:
____________________________
(--`DEFINE_AGGR
(AGGR (CLASSID "Stand") [CLASSID "Bulb"; CLASSID "Switch"])`--)
: goalstack
モデル情報で示される情報より、項の具象化をおこなう。
- e (EXISTS_TAC
(--`AGGR (CLASSID "Stand") [CLASSID "Bulb"; CLASSID "Switch"]`--));
OK..
1 subgoal:
val it =
(--`DEFINE_AGGR
(AGGR (CLASSID "Stand") [CLASSID "Bulb"; CLASSID "Switch"]) /\
MEMBER (CLASSID "Bulb")
(AGGR_COMP
(AGGR (CLASSID "Stand") [CLASSID "Bulb"; CLASSID "Switch"]))`--)
____________________________
(--`DEFINE_AGGR
(AGGR (CLASSID "Stand") [CLASSID "Bulb"; CLASSID "Switch"])`--)
: goalstack
集約関係の部品関係の定義AGGRCOMPとリストに対して、その要素かを調べる
MEM-BERの定義を用いて書き換えをおこなう。
- e (REWRITE_TAC [AGGR_COMP,MEMBER_DEF]);
OK..
1 subgoal:
val it =
(--`DEFINE_AGGR
(AGGR (CLASSID "Stand") [CLASSID "Bulb"; CLASSID "Switch"])`--)
____________________________
(AGGR (CLASSID "Stand") [CLASSID "Bulb"; CLASSID "Switch"])`--)
: goalstack
これで、仮定より証明できた。
- e (ASM_REWRITE_TAC []);
OK..
Goal proved.
|- (DEFINE_AGGR (AGGR (CLASSID "Stand")
[ (CLASSID "Bulb");
(CLASSID "Switch")])) ==>
(IS_COMPONENT (CLASSID "Bulb") (CLASSID "Stand"))
: goalstack
よって、BulbクラスがStandクラスの部品クラスであるということは、モデル情報と、
FO8M理論の定義より導くことができることを明らかにできた。
検証は、基本的のこの手順を繰り返すことで目的の定理を得る。
証明の書き換えに用いた定義
val IS_COMPONENT_DEF =
new_definition("IS_COMPONENT_DEF",
--`IS_COMPONENT (c:ClassID) (p:ClassID) =
?(iexp:AggrExp). DEFINE_AGGR iexp /\
(MEMBER c (AGGR_COMP iexp)) `--);
val AGGR_COMP =
save_thm ("AGGR_COMP", mk_thm([], --`!(x:ClassID)(y:^AGGR_CLASS list).
AGGR_COMP (AGGR x y) = y`--));
rec_axiom = list_Axiom,
def = --`(MEMBER (x:'a) [] = F) /\
(MEMBER (x:'a) (CONS (h:'a) t) =
((x = h) \/ MEMBER x t))`--};