Our society relies on computer systems, which are composed of many programs.Therefore, it is important to verify correctness of those programs. Currently,system developers rely on manual program inspection and testing to ensure that their programs work as per their specifications. However, manual inspection and testing may overlook potential bugs of programs. In contrast,formal verification methods can exhaustively verify correctness of programs, and are expected to play a central role in program verification. In the framework of type-based program verification, specifications are expressed as types, and type inference is used to verify that programs conform to those specifications.Dependent types are a special kind of types that may depend on values, and are useful for statically verifying detailed specifications of programs such as the absence of array bounds and pattern match errors. Compared to other formal program verification methods such as model checking and abstract interpretation,the method based on dependent types can straightforwardly deal with extended features of programming languages such as higher-order functions and recursive data structures.

For designing a type inference algorithm for a dependent type system, we need to put restrictions on the type inference algorithm since the typability problem of a dependent type system is usually undecidable. However, restrictions imposed by existing work are not desirable for program verification. For example, Dependent ML (DML) proposed by Xi et al. requires users to declare dependent types for all functions, so that the burden imposed on users is too heavy. The type inference algorithm for sized types proposed by Chin et al. fixes the shape of dependent types a priori, and tries to infer as precise dependent types as possible. Thus, verifiable properties and data structures are limited to predefined ones in their algorithm, and it may waste computational costs for inferring unnecessarily precise dependent types for program verification.

In this thesis, we propose a novel program verification method based on dependent types which solves the problems of the existing methods mentioned above. We introduce dependent types to a higher-order functional language with recursive data structures, and propose two type inference algorithms. The first algorithm infers dependent types which are precise enough to verify given specifications of a program on demand. The algorithm basically infers an output specification of a function from a call-site of the function, and propagates that specification backward to infer the input specification. We have implemented a prototype type inference system, and conducted two experiments. In the first experiment, our system successfully verified that insertion and merge sort programs always return an ordered list by automatically inferring dependent types of the auxiliary functions of these programs. Note that the type inference algorithm for sized types cannot verify such property since the algorithm can only infer the lengths of lists. DML requires users to write complex type annotations for verification of the sorting programs. In the second experiment, we have inferred dependent types of the standard list library functions for OCaml programming language by using call-sites of those functions collected from existing application programs written in OCaml. The results of the experiment indicate that our algorithm can infer preferable dependent types for not only program verification but also a documentation purpose.

One of the problems of existing type inference algorithms and our first algorithm described above is that if verification of a program fails, these algorithms cannot find out a reason of the failure automatically. Especially, the type inference algorithms cannot offer enough information to users for judging whether their programs are really incorrect: The type inference algorithms may reject a correct program due to the lack of analysis precision. In order to address the problem, in this thesis, we propose the second type inference algorithm which can find a counter-example against typability of an ill-typed program, namely a program input that leads to a run-time error, as an explanation of why the program is ill-typed. The algorithm can iteratively refine dependent types with interpolants until the type inference succeeds or a counter-example is found. We have implemented a prototype type inference system and conducted two experiments to evaluate the second type inference algorithm. In the first experiment,our system successfully verified that array programs obtained from DML sample programs cause no array bounds error without requiring type annotations. We then intentionally modified the array programs to obtain incorrect programs,which actually cause array bounds errors. We analyzed these programs with our system and successfully found counter-examples. In the second experiment,we successfully verified that insertion and merge sort programs always return an ordered list.

プログラムの形式的検証のために様々な手法が提案されているが、型に基づく解析は、プログラムの仕様を型として表現し、型推論によってプログラムが仕様を満たしているかどうかを自動的に検査する方法である。特に、値に依存できるように拡張された型である「依存型」を用いることにより、プログラムのより詳細な仕様を型として表現することが可能となる。しかし、依存型を含む型システムにおいては、型付け可能性は一般に決定不能であり、完全な型推論アルゴリズムは存在しない。

本論文では、高階関数や再帰的データ構造の表現可能な関数型言語に対して、依存型を含む型システムが導入され、その型システムのための二つの型推論アルゴリズムが提案され実装されている。

本論文の第1章では、以上で述べたような研究の背景と本論文の概要について述べられている。

第2章では、本論文の型システムによる解析の対象となる関数型言語が、その構文と操作的意味論とともに、説明されている。

第3章では、本論文の主題である型システムが詳しく述べられている。特に、前章の関数型言語の操作的意味論に対する型システムの健全性が証明されている。

第4章では、型推論のために、関数型言語のプログラムから、型に関する制約を生成する方法について述べられている。一般に、この制約を解くことにより、型推論が行われる。

以上の枠組みのもとで、第5章では、型推論の第一のアルゴリズムが述べられている。このアルゴリズムは、関数の呼び出しサイトから関数の仕様を推論し、それを後ろ向きに伝搬することによって、要求された仕様を検証するのに十分な程度に詳細な依存型を自動的に求めることができる。第5章では、このアルゴリズムのプロトタイプ実装および実際のプログラムを対象とした二つの実験についても報告されている。一番目の実験では、挿入ソートとマージソートを実装したプログラムが必ず整列されたリストを返すことを自動的に検証することに成功している。二番目の実験では、OCamlプログラミング言語のリスト操作ライブラリ関数群の依存型を、そのライブラリを呼び出している実際のOCamlプログラムを用いて推論した結果が述べられている。

第6章では、型推論の第二のアルゴリズムが述べられている。このアルゴリズムは、補間定理証明器を用いて、型推論が成功するか反例が見つかるまで徐々に依存型を詳細化する。特に、反例を出力することは、第一のアルゴリズムにはない優位点である。また、補間定理証明器を用いた詳細化を反復することにより、第一のアルゴリズムでは求められなかった型を推論することができる。第6章では、このアルゴリズムのプロトタイプ実装および実際のプログラムを対象とした二つの実験についても報告されている。特に、一番目の実験では、配列を操作するプログラムが配列境界エラーを起こさないことを、ユーザに依存型宣言を要求することなく検証できることが示されている。

第7章では関連研究、第8章では本論文の結論が述べられている。

以上をまとめると、本論文は、依存型を含む型システムに対して、二つの新たな推論アルゴリズムを開発することにより、実践的なプログラミング言語における依存型の応用可能性を、大きく広げたということができる。そして、この結果は、プログラムの形式的検証技術に対する十分な貢献と考えられる。

よって本論文は博士(情報理工学)の学位請求論文として合格と認められる。