(4) KL1 プログラム開発支援ツール

［中間報告］

(1) 研究進捗状況

本研究は、並行論理プログラムのデータの流れや通信プロトコルに 関する性質を静的に解析するモード解析を中核技術として、それを 静的デバッガやスタイルチェッカ等に応用することを目的としてい る。これまでに、この中核となるモード解析アルゴリズムの基本部 分を実装し、それを用いてKL1プログラムの解析実験を行なってき た。また、モード解析システムの実用性向上のため、モードづけで きないプログラムの解析法を検討してきた。

(2)現在までの主な成果

モード解析システムの基本部分を実装した。これは、KL1プログラ ムから、それが課するモード制約集合を抽出するモード制約生成系 と、抽出したモード制約の無矛盾性を検査しつつ、プログラムのモー ドグラフを構成するモード制約充足系からなる。

システムはまだ開発途上であるが、すでにモード制約充足系自身 (規則数190)を含む、かなり大きな現実的プログラムの解析が可能 なレベルに達している。モード制約充足系自身の解析によって、

• 現実的なKL1プログラムが課する制約の種類や数、
• 現実的なKL1プログラムの性質(各変数の出現数、通信プロトコルの複雑さなど)、
• 現実的プログラムから得られるモードグラフの形状的特徴

などに関してさまざまな知見が得られた。

システムの実用化のためには、モードづけできない、つまりモード 制約が矛盾するプログラムに対して、その理由を解析する機能も重 要となる。プログラムの構造に即した順序でモード制約を解いてゆ くことにより、矛盾の理由を効率良く特定できる見通しが得られた。 また、複数の矛盾を一回の解析で検出する見通しも得られた。

(3) 今後の研究概要

モード制約生成系については、モード制約を、プログラムの構造に したがってグループ化して出力する方式に変更する予定である。ま たモード制約充足系については、特にベクタ操作の解析を実装する ことと、モードづけできないプログラムの解析に必要となる、グラ フ複写機能を実装することが重要課題である。

(4) 今年度目標成果（イメージ）

本年度末までに klint 第１版を完成させ、公開する予定である。 klint 第１版は、モードづけ可能な（well-modedな）プログラムに 対して、そのモードグラフを人間および機械に読める形で出力する。 モードづけできない（ill-modedな）プログラムに対しては、でき るだけ適切なエラーメッセージを出力する。