klint第2版の概要

klint第2版は、KL1プログラムの実装方式非依存の解析情報を統合的に出力す る解析系である。第1版からの改良拡充によって、次のような機能を備えている。

1. 参照数解析機能

   klint第2版における参照数とは、データ構造中の特定の場所に出現するデータの 読み手が、単数に限られるか複数になりうるかに関する情報である。参照数解析 も制約充足問題として定式化することができ、近似的には単一化によって容易に 求めることができる[9]。

2. 型解析機能

   klint第2版における型とは、データ構造中の特定の場所に出現しうる関数記号の 集合のことである。整数、浮動小数点数、ストリング、ベクタ、非空リスト、空 リスト、上記以外の定数(0引数関数)、上記以外の関数(1引数以上)のうちのどの カテゴリのデータが各パスに出現しうるかを解析して出力する。この型情報も、 単一化に基づく解析によって求めている。

3. KL1特有の言語機能の取扱い

   klint第2版は、現KLIC処理系のほぼすべてのガードおよびボディの組込述語に対 応している。重要な特徴は以下の通りである。

   • ガードゴールの出力引数を扱える。Flat GHCの計算モデルでは 認めていない機能であるが、現実のKL1プログラムの多くがこの機能を用いてい るためである。
   • ベクタとその操作をサポートしている。引数にランダムアクセスする述語の呼 出しがあると、すべての引数が同じモード、型、参照数に制約される。
   • 構造体の引数にランダムアクセスする arg , set_arg を サポートしている。
   また、組込み述語は多相(polymorphic)述語としてサポートしており、異なる述 語呼出しは異なるモード制約や型制約をもつことができる。

4. 解析能力強化

   プログラム節に3回以上出現する変数はほとんど例外なく単方向通信に用いてい るという観察に基づき、non-binaryな制約の解析能力をklint第1版よりも強化し ている。つまり、最汎ではないが単純で実際的な解を具体的に求めることができ る。これにより、non-binaryな制約が解けないで解析が終了することがほとんど ない。