7.2 実装抽出
7.2.4 操作抽出
操作抽出は細分化モデルの代入VA0 と実装の代入VI を入力としてVA0 と等価な実装の 代入VI0を出力する. ここで, VA0 が非決定的値生成操作を細分化して得られる代入ならば VI は実装の非決定的値生成操作VAnyDefI であり,VA0 が非決定的値参照操作を細分化して 得られる代入ならばVI は実装の非決定的値参照操作VAnyRefI である. この抽出にはプロ
第7章 モデル充足細粒度部品生成 85
SELECT P1 THEN v := F1
WHEN P2 THEN v := F2 ...
WHEN Pk THEN v := Fk
IF P THEN X ELSE Y
IF P THEN X IF not(P) THEN Y P1 or P2 or ... or Pk => P
P1 or P2 or ... or Pk => not(P) otherwise
IF P THEN X ELSE Y 細分化モデルの制御構造 実装の制御構造
P1 or P2 or ... or Pkで代入が生じる
（Yは関与しない）
（Xは関与しない）
図 7.2: 実装の制御構造の抽出
グラムスライシング手法であるWeiserの手法を用いる. モデル細分化では条件分岐を分 割したが, Weiserの手法のスライシング結果は細分化モデルに含まれない遷移条件や代 入を含む. 本手法ではこの様な細分化モデルに反する実装を抽出しないためにモデル細 分化で抽出した遷移条件に対する実装の抽出(制御構造の抽出)とモデル細分化で抽出し なかった代入の特定(抽出しない文の特定)を行う. この結果に対してプログラムスライ シングを適用することで細分化モデルの代入VA0 に対する実装をVI から抽出する. 以下
の節では‘制御構造の抽出’, ‘抽出しない文の特定’, ‘プログラムスライシングの適用’ につ
いて説明する.
制御構造の抽出
制御構造の抽出は細分化モデルにおける遷移先が空でない遷移条件群P1, . . . ,Pk と実 装の代入文VIを入力として,P1, . . . ,Pk に対応する遷移をのみを実装した実装の代入文を 出力する. ここでは条件式がPであるIF文についてTHEN部を条件式Pの制御ブロック, ELSE部を条件式¬Pの制御ブロックと呼ぶ. 制御構造の抽出は実装のIF文において条件
P1, . . . ,Pkで実行されない制御ブロックを空にすることで行う. すなわち，図7.2のように
(P1 ∨ · · · ∨Pk)⇒P ならば条件式¬Pの制御ブロックを空にし，(P1 ∨ · · · ∨Pk)⇒ ¬P ならばP の制御ブロックを空にする．また，どちらでも無い場合，すなわちどちらの制 御ブロックも実行しうる場合には両方の制御ブロックを残す．これは細分化モデルで空 でないブロックに到達する条件において到達不可能な制御ブロックを実装操作から取り 除くことを意味する.
抽出しない文の特定
細分化モデルの代入VA0 とVA0 に対応する細分化実装VI0を考える. VA0 で変化する変数 群をXA,VI0におけるXAのリンク変数をXI とする. また,VA0 で変化しない変数群をYA, VI0におけるYAのリンク変数をYI とする. この時, 細分化モデルの代入VA0 と細分化実 装の代入VI0が対応するためには, VA0 におけるXAの変化と同様にVI0においてXI が変
第7章 モデル充足細粒度部品生成 86 化することが重要であるが, VA0 においてYAが変化しないのと同様にVI0においてYI が 変化しないことも重要である. このため, YI は ‘変化してはいけない大域変数(代入禁止 実装大域変数)’であり, YIを変化させないよう細分化実装の操作VI0を生成しなければな らない. これは代入禁止実装大域変数群YI への代入文f にマークを付け，後に行うプロ グラムスライシングにおいてマークが付いた代入文を抽出しない事で実現する. また, 代 入文f が操作呼び出しである場合, 1代入文で複数の値が変化する場合がある. このよう に1代入文で代入禁止実装大域変数YI とその他の変数v が同時に変化するとき, f の抽 出を抑制すると変数v が未定義になる. そのため,この様な未定義の変数を参照する文も プログラムスライシングにおける抽出を抑制する必要がある. 代入文f において値が未定 義である変数U(f), およびプログラムスライシングにおいて抽出しない文の集合Lとし たとき,それらは以下のように計算される.
抽出しない文の集合 L: 代入文f の直前が条件分岐である場合には直前に行われる代入 は複数ありえるが,これらの集合をprev(f)とする. 代入文f が代入禁止実装変数群 YI を定義する場合,またはf が未定義な変数群∩
g∈prev(f)U(g)を参照する場合はf をLに追加する. ただし, f が変数群XI に対する代入である場合は追加しない. こ れにより, 細分化モデルで変化する変数が細分化実装においても変化する.
未定義変数群 U(f): U(f)は∩
g∈prev(f)U(g)を引き継ぐ. これにより,条件分岐のいずれ かによって値が定まるならば未定義変数群から取り除かれる. f がLに含まれるな らば, f で定義される変数群をU(f)に加える. そうでないならばf で定義される変 数群をU(f)から取り除く.
プログラムスライシングの適用
本稿ではプログラムスライシングとして2.4.2項で紹介したWeiserの手法を用いる. た だし，先の ‘抽出しない文の特定’ で示したように本手法では代入禁止大域変数群を考慮
してWeiserの手法を適用する必要がある．そのため, Weiserの手法に対して抽出しない
文の集合L に含まれる文は抽出される文SC に加えない’ という拡張をする. Weiserの手 法は入力として代入文G,プログラム中の行i，注目する変数群V を入力とする．本稿で
はGを先の ‘制御構造の抽出’ で得られた代入文とし，i を実装操作の末尾，V を細分化
モデルで変化する変数群のリンク変数とする．これにより細分化実装の操作が得られる.
B Methodの実装は一般的な命令型言語と異なりWHILEループに不変条件を与える．
本手法では不変条件を考慮せずにWHILEループにWeiserの手法を適用する．WHILE ループの不変条件は後に行う証明責務最小化で実装の不変条件と同様に得る．この様に
WHILEループの不変条件をループ中の代入文とは独立して抽出するのは，WHILEルー
プの不変条件はループ中の代入文には影響を与えず，ループの停止性保証とループで生
第7章 モデル充足細粒度部品生成 87 成される値の特定に用いられるためである．