本節ではMSSSの信頼性とMSSSで利用される部品を生成するMSFC生成の信頼性に ついてそれぞれ考察する．
9.2.1 MSSS の信頼性
MSSSは健全性の高い部品検索でMSFCを選択し，それらを結合することでソフトウェ アを合成する．ここで，リポジトリ内のMSFCは4.3節のように証明責務の証明により 信頼性が保証されていると仮定されるため，そのため，MSSSで得られるソフトウェアの 信頼性は部品選択，部品結合の信頼性で定まる．以下の節ではそれぞれの信頼性につい て考察する．
第9章 考察 129 部品選択の信頼性
MSSSにおける部品選択は6.2節の部品検索と6.3節の部品選択により行われる．部品 検索と部品選択の信頼性は以下のようにまとめられる．
1.部品検索は従来のコード生成手法における検索やパターン判定に比べて高い健全性 を持つ．
2.部品選択は証明責務が偽になることが明らかな部品の組合わせを排除する．ただし，
常に証明責務が真になるとは限らない．
3.数学的に判定できない部品選択の妥当性は部品選択において利用者が実装方法を選 択することで保証する．
従来のコード生成手法は意味付けを部品名や機能名に頼っており，名前付けが非妥当で あったり，名前の解釈を誤った場合には正しいコードが生成されない．これに対して6.2 節の部品検索では数学的な仕様であるモデル間で数学的に判定を行うため，非妥当な名 前付けや名前の誤解釈による誤りが生じない．ただし，仕様間の数学的判定は健全性が高 い反面で完全性の保証には仕様間の判定に定理証明を必要とし計算量爆発を招く．MSSS ではこの問題を細分化モデルの字面統一により仕様間の判定を字面一致で可能にするこ とで解決している．この部品検索の計算量低減は9.3節で説明する．
6.3節の部品選択では選択可否判定により合成ソフトウェアの証明責務が偽になる事が 明らかな組み合わせを排除することで合成ソフトウェアの信頼性を向上している．6.3.2 項で述べたように選択可否判定では型の文字列一致判定のみを行っており，型以外の制 約条件が矛盾する可能性がある．選択可否判定に定理証明を用いることで合成ソフトウェ アの証明責務が真になることを保証できるが，先行する定理証明に基づいた自動コード 生成手法が計算量の問題で実用化されていないことを考えれば計算量の低減を重視する ことは妥当と言える．
部品検索と選択可否判定はどちらもソフトウェアの数学的な側面だけで判定を行うた め，部品の組み合わせの信頼性は証明責務で保証できるものに限定される．この場合，証 明責務は真だが非妥当な組み合わせが生じうる．例えば，8.4.5項の部品選択可否判定例 では変数usersなどをデータベースに保存する部品CB10 と変数rentをファイルに保存する 部品CG3,CG5 の選択可否判定が真であることを示した．しかし，多くの場合には users と rent の両方がデータベースに格納されることが妥当である．MSSSでは6.3.3項の‘利 用者による実装方法の選択’でuser, rent の実装に用いるモジュールを選択することによ り妥当な部品の組み合わせを用意に選択することができる．
第9章 考察 130 部品結合の信頼性
互いに矛盾しない部品を再利用して得られるソフトウェアが高信頼であるためには, 再 利用手順自体が高信頼である必要がある. 6.4節の部品結合は制約条件の結合と操作の結 合に分けられる. 本手法では出力モデルと出力実装のプロパティ制約や不変条件を部品の 制約条件の論理積で生成する. これにより部品群が互いに矛盾する制約条件を持たない ならば, それらを論理積で結合した制約条件も矛盾しない. 6.4.2項の操作の結合では要 求モデルから得た細分化モデルを元通りに組み直すのと同様にその細分化モデルを仕様 として持つ細分化実装をモデル細分化手順を逆に辿るように結合する．部品検索で得ら れた部品群が要求モデルから得られた細分化モデルを仕様として持つことは6.2節の部品 検索において式(6.5) が成り立つことから保証される．また，細分化モデルと同様に細分 化実装の操作を合成するためには4.2.3項に示した副作用を解消する必要がある. 細分化 モデルの操作は全て同時代入であるため代入順序を考慮せずに結合することができるが，
細分化実装の操作は代入順序を持つため，結合順序によって得られる結果が異なる．こ れを解消するため，4.2.3項の細分化実装は代入文を‘大域変数を参照して計算結果を局所 変数に格納する参照部’と, ‘その局所変数を参照して大域変数への代入を行う代入部’ に 分割して持つ. これにより操作結合時に全ての参照部が代入部の前に実行されるよう結 合することで副作用を解消している.
8.4節のMSSSの適用例ではマイレージ付きレンタカーシステムを合成した．この例で
は‘要求モデルへの初期化の追加’と‘部品が割り当てられなかった細分化モデルに対する
部品追加’を行うことで合成ソフトウェアの証明責務が全て真になった．副作用を解消し た合成例を図8.22に示したが，この合成結果の副作用が解消されていることは証明責務 が全て真であることからも明らかである．ただし，図8.22の合成結果において同じよう
なWHILEループやIF文による判定を複数回行っている事からも分かるように，提案手
法によって得られる合成ソフトウェアは信頼性は高いが実行効率は低い．これは，本研 究の関心事が合成ソフトウェアの信頼性であり，実行効率の向上のために手法が複雑化 する事を避けたためである．このため，6.4.2項で与えた実装操作の合成手順は4.2.3項 の部品の定義で与えた副作用の解消に忠実である．また，実行効率の問題は合成ソフト ウェアにアルゴリズムの最適化を適用することで解消できると考える．
9.2.2 MSFC 生成の信頼性
4.3節ではB Method の枠組みに基づいて部品の信頼性を定義した．この様に信頼性を
証明責務という数学的な命題に基づいて定義することで手法自体の信頼性を定義に基づ いて評価することができる．本節では提案したMSFC生成の信頼性を部品の信頼性に基 づいて評価する．
第9章 考察 131 モデル細分化の信頼性
4.3節ではB Methodの証明責務に基づき細分化モデルの証明責務を定義した．さらに，
5.7節ではモデル細分化で得られる細分化モデルの証明責務が常に真であることの証明を 試みた. この結果, 初期化から得られる細分化モデルの証明責務は常に真になることが証 明された．また, 制約条件展開が任意の変数間の暗黙的な関係を全て推論できるならば操 作から得られる細分化モデルの証明責務は真になることが証明された．この‘制約条件展 開が任意の変数間の暗黙的な関係を全て推論できるならば’ という仮定は証明2において 理想的な推論器を仮定した事で生じる．しかし，現実には理想的な推論器は定理証明と 同様に停止性を保証出来ないため提案したモデル細分化手法では5.3節で示したように有 限個のルールを有限回適用することで近似的に推論を行っている．このため,モデル細分 化では得られた細分化モデルに対して証明責務の証明を行う．細分化モデルの証明責務
は B Method のモデルの証明責務と同じであるため,この作業には AtelierB[6] などの証
明支援環境が利用でき，自動証明器で証明できない証明責務のみを人手により証明する．
実装抽出の信頼性
実装抽出の信頼性は‘細分化実装と実装依存モデルの証明責務が真になること’ と定義 できる．MSFC生成の実装抽出では7.2.6項に示した証明責務最小化により証明責務が真 であることを保つよう証明責務を最小化する. このため, 実装抽出の信頼性は原理的に保 証されている. ただし,証明責務最小化は7.2.6項に示したように定理証明を完全に自動化 することが出来ないために作業者の負担軽減が問題となる. MSSSフレームワークではこ の問題を部品の細粒度化により解消している．仮定削減作業の定理証明は経験的に証明 責務のゴールが大きい程難しい．このゴールの大きさは仮の不変条件と操作抽出で得ら れた操作の事前条件で決まる. そのため, 操作抽出で得られる操作が小さく, その操作が 含む大域変数が少ない程, 仮定削減の定理証明は容易になる. 本手法では部品の粒度を小 さくしたことで部品群が大量に生成されるが,仮定削減の定理証明が容易であるため自動 定理証明が期待できる. 自動定理証明が失敗した部品に対しては作業者が証明を行うが, この証明作業も7.2.6項に示したように細分化元ソフトウェアで証明を行った者が証明を 行うことで作業負担を軽減できる. 証明の作業量と証明責務が偽である場合の作業量につ いては9.4節で考察する．また，5.7.2項の証明2では制約条件展開の推論能力が高いほ どモデル細分化の信頼性が向上することを示した. このため,細分化モデルの証明責務が 偽になる場合には制約条件展開を修正することでモデル細分化手法の信頼性が向上する．