6.2 部品検索
6.2.3 変数名統一
変数名統一は部品群の変数名を要求モデルの変数名に統一し，結合時に部品群を連動 させる．この処理は検索キーMK0 と, それに割り当てられた部品Gを入力として,MK0 の 変数xi に対応する部品Gの変数yiを特定し, yi の変数名をxiに合わせる．
以下の節では変数名統一を実装依存モデルの変数名統一と細分化実装の変数名統一に 分けて説明する．
第6章 モデル充足ソフトウェア合成 69 実装依存モデルの変数名統一
実装依存モデルの変数名統一では実装依存モデル群の変数名を検索キー，すなわち，要 求モデルの変数名に置換する．6.2項の部品検索時に式(6.5) が真になるよう部品の細分 化モデルの変数名を検索キーの変数名で置換し，それと同様に実装依存モデルの変数名 を置換することで行う．実装依存変数群には部品間での参照や代入を避けるために固有 の変数名を与える．
例として図6.3の各部品に対する変数名置換の結果を図6.5に示す．ここでは検索キー a, bに対する変数名置換を説明する．細分化モデルaの変数名を登場順にそれぞれ検索 キーの変数名に置換するとX1, X2, X3, X4 がそれぞれ maxPerson, persons, person, np に置換される．同様に細分化モデルbではX1, X2, X3 がそれぞれmaxPerson, persons,
personに置換される．よって実装依存モデルの変数に対しても同様の置換を適用する．ま
た，部品a, bの実装依存変数fileOpen は A, B をそれぞれ接頭語とし，部品に固有の変 数名A fileOpen, B fileOpenを与える．
細分化実装の変数名統一
細分化実装の変数名統一では部品結合時に連動して動作するように，細分化実装の変 数名を実装依存モデルの変数名に合わせて置換する．モデル実装間変数対応付け(4.4.3 項) により実装依存モデルのモデル変数と細分化実装の大域変数は1対1に対応する．こ こではモデル変数に対応する実装変数をリンク変数と呼び，モデル変数を用いてリンク 変数の変数名を統一することを考える．実装変数は具象変数，輸入変数，局所変数に分 類でき，それぞれ以下の様に置換する．この際， ‘輸入変数の置換’ ではモジュール別名 を共通化し，部品結合時に部品群を協調させる．また，リンク変数が等しい実装依存変 数名を共通化することで，実装依存変数を要求モデルで共通化できない問題を解消する．
1.具象変数の置換: モデル変数xKiのリンク変数viが具象変数ならばviをxKi iに置換 する．
2.輸入変数の置換: モデル変数xKiのリンク変数vi がモジュールM で宣言される場合，
輸入‘別名.モジュールM’ を‘xKi i.モジュールM’ に置換する．また，モジュール 変数等の参照も同様に置換する．複数の実装変数が1つのモジュールで宣言される 場合，適当な実装変数yを1つ選び，他の変数名はyと同様に置換する．この際，リ ンク変数が等しい全実装依存変数に共通の変数名を与える．
3.局所変数の置換: 細分化実装の局所変数には部品間で重複しない変数名を与える．本 稿では重複する局所変数名に部品名を付加する．
モデル実装間変数対応付けはモデル変数と実装変数の対であり，図6.3 の 部品a, b で は共に(X2, X2 i.val), (fileOpen, X2 i.fileOpen)と定まる．実装依存モデルの変数名統一
第6章 モデル充足ソフトウェア合成 70
maxPerson:1..1000
max(persons)<=maxPerson-1 A_fileOpen = TRUE persons : POW(0..maxPerson) A_fileOpen : BOOL
persons_i.val = persons A_fileOpen = persons_i.fileOpen persons_i.Set(0..maxPerson)
isEmp<--persons_i.isEmpty;
IF isEmp=TRUE THEN newID := 1 ELSE ... END;
np:=newID 実装依存モデルa 細分化実装a
belong_i.val = belong C_fileOpen = belong_i.fileOpen belong_i.PFun(0..maxPerson, 0..maxGrp)
belong_i.setVal(person, group) 実装依存モデルc 細分化実装c
maxPerson: 1..1000 maxGrp:1..1000
person: 0..maxPerson group: 0..maxGrp C_fileOpen = TRUE belong:POW( ... ) C_fileOpen : BOOL
persons_i.val = persons A_fileOpen = persons_i.fileOpen persons_i.Set(0..maxPerson)
persons_i.add(person) 実装依存モデルb 細分化実装b
maxPerson:1..1000
person: 0..maxPerson &
A_fileOpen = TRUE persons : (0..maxPerson) A_fileOpen : BOOL 部品a
部品b
部品c
Qa
Qb Ia
Ib
Ja
Jb Wa
Zb
Zc パラメタ制約
不変条件
事前条件
輸入 不変条件
定義部
参照部
参照部 パラメタ制約
不変条件
事前条件
輸入 不変条件
定義部
参照部 定義部 パラメタ制約
不変条件
事前条件
輸入 不変条件 検索キーa
ANY person WHERE
person:0..maxPerson not(person:persons) THEN
np:=person maxPerson:1..1000
max(persons)<=maxPerson-1 persons : POW(0..maxPerson) パラメタ制約
不変条件 事前条件 代入
persons := persons \/ {person}
maxPerson:1..1000
person : 0..maxPerson persons : POW(0..maxPerson) 検索キーb
パラメタ制約 不変条件 事前条件 代入
belong:=
belong\/{person |-> group}
maxPerson: 1..1000 maxGrp:1..1000
person: 0..maxPerson group: 0..maxGrp not(person: dom(belong)) belong :
POW(0..maxPerson*0..maxGrp) dom(belong) <: 0..maxPerson ran(belong) <: 0..maxGrp 検索キーc
パラメタ制約
不変条件
事前条件
代入
図 6.5: 変数名置換を適用した部品群
第6章 モデル充足ソフトウェア合成 71 では X2 を persons に置換したため，モジュールの別名 X2 i を persons i に置換する.
図6.3の部品a, b においてリンク変数が等しい実装依存変数としては fileOpenが挙げら れる．このため，B fileOpen を 部品Aに合わせてA fileOpen に置換する．局所変数の 置換では部品間で局所変数名の重複が生じないため，isEmpなどの局所変数名をそのま ま用いる．これにより，図6.5のように変数名置換後の部品が得られる．