4.5.1 検証効率について
状態遷移図ベースの検証法と，本論文で提案するコラボレーションベースの検 証法の決定的な違いは，オブジェクト数に関する検証のスケーラビリティである．
状態遷移図ベースの検証法においては，複数のオブジェクトにまたがる性質を証 明する際は，状態遷移図の合成をとる必要がある．合成により状態爆発が起こっ てしまった場合は検証すること自体が不可能となる．段階的振る舞い近似法のよ うな状態数を削減する手法を用いたとしても，その効率はオブジェクト数の増加 に伴い急激に悪化する．一方，コラボレーションベースの検証法では最初から合
成システムの無限の状態を一つの変数として扱っており，任意の数のオブジェク トに対応することが可能である．そのため，オブジェクト数の増加が効率悪化に 直接つながることはなく，検証自体不可能となることもない．オブジェクト数の 増加に対応できることは，多くのオブジェクトにより構成される大規模システム を検証する上で重要である．また，コラボレーションベースの検証法では，メソッ ド 呼び出しというオブジェクト間の協調動作を直接捉える視点でシステムの振る 舞いを定義できるため，段階的振る舞い近似法のように，合成された状態遷移図 から協調動作に関わる状態遷移図を抜き出すオーバーヘッド もない．
ただし，状態を一変数で扱うことによるデ メリットもある．それは，コラボレー ション，つまり，一変数上に適用される関数適用列を一括して証明対象としなけ ればならず，ユーザにかかる証明の負担が大きくなることである．4.1で述べた青 木らの手法では，複数の状態を考慮する分，個々の状態で実行されるアクション は単純化し ，各状態遷移に対応する帰納段階の証明はほぼ自動的に行うことがで きる．
証明の複雑さは定理証明の大きな問題であるが，それに対応するためには，高 級なタクティックの実装，及び，証明の整理法の研究が必要である．タクティック とは，HOLのGoal-Oriented Proofにおける分解規則であり，MLによって既存の タクティックからより強力なタクティックを実装することができる．この機能を利 用してオブジェクト指向理論に特化した高級タクティックを実装することにより，
証明ステップを削減することができると考えられる．証明の整理法としては，メ ソッド を単位として補題を作成する方法が有効であると考えられる．これは，複 数のコラボレーションが同一のメソッドを共有していることがあるためであり，そ のメソッド に関して補題を蓄積しておけば，複数の証明に再利用することができ る．この点を考慮して，証明方法論を明確にする必要がある．
4.5.2 コラボレーションの計算モデルについて
本論文では，コラボレーションをシステムの状態の上の関数として定義してい るが，現段階でその具体的な計算モデルまでは定義していない．コラボレーショ ンをHOLに実装する際は，高階述語論理の範囲で任意のものが定義できてしまう
のが現状である．開発者にとって理解しやすい高級な計算モデルを定義し，HOL 表現との対応付けを定義する必要がある．コラボレーションの定義法に制限が与 えられれば，その定義の構造に基づいた，より詳細な証明方論法が明確になる．現 時点では，コラボレーションをシーケンシャルなオブジェクト指向プログラムと して定義し ，ホーア論理に基づく検証条件自動生成ツールを実装することを考え ている．なお，コラボレーションの意味論に関する研究としては，UMLシーケン ス図をイベントトレースの集合として解釈する方法[23]や，UMLコラボレーショ ン図をグラフ変換規則として解釈する方法[24]がある．
4.5.3 並行性について
personとcounterの例題は，personオブジェクトが能動的なオブジェクトで あり，counterオブジェクトは受動的なオブジェクトであった．言い換えれば，動 作の始点になるのは常に personオブジェクトであり，counterオブジェクトは
personオブジェクトによるメソッド 呼び出しがあってはじめて動作する．このよ
うなコラボレーションはシーケンシャルな実行の流れであり，関数適用列として 容易に表現することができる．しかし ，実際に存在するシステムの中には，分散 システムのように，複数の能動オブジェクトが存在し，それらが自立的に動作す ることにより構成されるものが数多く存在する．そのようなシステムについての 不変表明を証明するためには，並行性の概念を扱えるようにする必要がある．
第 5 章
検証支援ツール
本章では，HOLライブラリobjLibとして実装したオブジェクト指向理論の検 証ツールについて述べる．ライブラリは以下の 2つの機能を提供する．
• オブジェクト指向理論の自動生成
• オブジェクト指向理論のシミュレーション実行環境の自動生成
それぞれ，ML関数mk_theory_script,mk_theory_simuratorとして実装される
（ 図5.1）．
mk_theory_script mk_theory_simurator
図 5.1: objLibの機能
まず，両関数の共通の入力となるクラスモデルについて述べる．次に，理論生 成機能，実行環境生成機能それぞれについて述べる．
5.1 クラスモデル
クラスモデルは特定の形式に従ってファイルに記述される．図5.2は図2.1の例 のクラスモデルを記述したファイルfigure.cmである．
class fig
attr x holtype : int | 0 mltype : int | 0 attr y holtype : int | 0 mltype : int | 0
class rect extends fig
attr w holtype : num | 0 mltype : int | 0 attr h holtype : num | 0 mltype : int | 0
class crect extends rect
attr c holtype : color | black mltype : color | black
図 5.2: クラスモデルファイルの例
クラスの宣言は，
class C extends S
の形式によって行う．これはCがクラスSを継承するクラスであることを表す．
属性の宣言は，
attr X holtype : HT | HD mltype : MT | MD
の形式によって行う．これは，名前がX，HOLにおける型とデフォルト値がそれ ぞれHT,HD，MLにおける型とデフォルト値がそれぞれMT, MDであることを表す．
HOLにおける型とはオブジェクト指向理論における型であり，MLにおける型と はシミュレータによりML上で実行する際の型である．属性w, hの宣言において，
num型はMLには存在しないため，intで代用している．