既公開のklintシステム第1版に実装されているモード解析と同様、制約充足の技 法に基づいて型とデータ参照数を解析する技法を検討した。
本研究で採用した型の概念は次のようなものである。関数記号(定数を含む)の集
合Funcを、重なりをもたないいくつかの集合F1,...,Fnに分類し
ておく。そしてプログラムの型を、データ構造中の特定箇所を示すパスの集合か
ら2
への関数として定式化する。これによって、複雑な
データ構造の構成要素の型も扱うことができる。このように定義した型情報が、
モード解析と同様の方法で計算できることを実装によって示した。
また参照数とは、データ構造中の特定の場所に出現するデータの読み手が、単数 に限られるか複数になりうるかに関する情報であり、記憶管理の最適化に重要な 役割を演じる。参照数情報は、近似的には単一化によって容易に求めることがで き、データの単一参照性がそれで保証できる場合も多いが、より詳細な解析情報 が必要となる実際的例題もあることがわかった。そのような例題に対処するには、 単一化による解析では不十分であるが、含意演算子を用いた制約式を考えること によって制約ベースの定式化の中で扱えることを示した。