|
GHC(Guarded Horn Clauses)をはじめとする並行論理プログラミング言語は、簡潔な通信・同期機構と柔軟な記述力とを特徴とするが、その実用化を図るには、プログラミング支援と処理効率の両面から、プログラムの静的解析技法がきわめて重要となる。
研究代表者はこれまでに、GHCプログラムの情報の流れ(モード)を論じるためのモード体系と、静的モード解析技法を提案し、その理論的側面を整備してきた。本研究では、この静的モード体系に対し、新たに応用的側面から検討を加え、その有用性をさまざまな角度から実証した。
1. モード解析システムの実装-並行論理型言語KL1のためのモード解析システムklintを、KL1言語自身で実装した。現実のプログラムに適用することによってシステムの評価・拡充を繰返し、複雑なKL1プログラムに対応できる実用的なシステムとした。
2. モード体系の下での記述能力の検証-klintシステム自身をはじめとする実用規模の並行論理プログラムの解析を通じ、静的モード体系を備えた並行論理型言語の記述力が十分であることを明らかにした。
3. デバッグへの応用-モード体系はプログラムの誤りの静的検出にも非常に有効である。そこで、モードづけできないプログラムの誤りを効率よく解析するアルゴリズムを提案し、実装を行なった。本技法は制約に基づく静的体系一般に適用可能なものとなった。さらにプログラム誤りの自動修正の方法を提案し、その修正能力を確認した。
4. 静的モード体系を利用した処理系の改善-モード解析情報に、データ型やデータ参照数についての解析情報を併用することにより、タグ判別をはじめとする動的な判断の多くが省略でき、手続き型言語で直接記述した場合と大きく変わらない性能が得られることを明らかにした。
|
