| 平成８年度 委託研究ソフトウェアの 最終成果報告書 |
並行論理プログラムのための強モード体系と制約ベースのモード解析は、プロ セス間通信プロトコルの整合性の保証や最適化に役立つだけでなく、デバッグ にも基本的な役割を演じると期待される。ほとんどの KL1プログラムはモード づけ可能、すなわち Moded Flat GHCプログラムであるが、Moded Flat GHCプ ログラムのモード解析は多数の単純なモード制約からなる制約充足問題であり、 素性グラフの単一化問題として効率良く解くことができる。しかしながら、実 際のプログラミングにおいては、モードづけできない、つまりモード制約が全 体として矛盾するプログラムを解析して、矛盾のもっともらしい「理由」をプ ログラマに呈示する機能も重要となる。この呈示機能は、モード宣言を与える ことなく実現できることが望ましい。
本研究で開発した kimaシステムは、モードづけできないKL1プログラムのため の静的デバッグツールである。基本アイデアは、全体として矛盾するモード制 約集合から矛盾する極小の部分集合を見つけ、その極小部分集合内の制約を課 したプログラム中の記号や記号出現を示すというものである。モード制約集合 に冗長性がある場合は、極小集合の中に入っていない制約を考慮することによっ て、バグの箇所をさらに絞り込むことが可能である。kimaシステムは、独立な 複数のバグを一回の解析で報告することもできる。大きなプログラムに対して は、kimaは述語を層化することによって探索空間を狭め、より直観的な説明を 生成しようとする。層化は、モード多相の導入にも基本的な役割を果たす。
www-admin@icot.or.jp