オブジェクト指向言語の実行時エラーを事前に静的に検出する方法のひとつとし
て、
クラス集合型検査法が提案されている。これは、型概念のないオブジェクト指向言語
TinyObjectを対象とし、クラス名の集合を型として導入して型検査を行う方法であ
る。
しかしながら、TinyObjectは基本的な機能を持つが型の概念を持たない。
本研究では、TinyObjectに基本型(整数型と論理型)とその演算を導入して拡張する
とともに、従来の型検査法を、クラス集合型および基本型のいずれかを型割当の解と
して
出力するように修正する。また、TinyObjectプログラムの動作モデルである
TinyObject
Machine(以下ではTOMと呼ぶ)を拡張し、TinyObjectプログラムPからその実行を表す
TOM M_Pへの変換を定める。そして型推論アルゴリズムがプログラムPに対する解とし
て
型割当を返したとき、M_Pが正しく動作すること、すなわち型推論アルゴリズムが
健全であることを証明する。