Finite Testing with Correctness Guarantee for Polymorphic Programs

2023 Fiscal Year Research-status Report

• Project/Area Number: 23K11044
• Research Institution: The University of Tokyo
• Principal Investigator: 森畑 明昌 東京大学, 大学院総合文化研究科, 准教授 (10582257)
• Project Period (FY): 2023-04-01 – 2028-03-31
• Keywords: テスト / 多相型 / 関数型言語 / 型パラメトリシティ

Outline of Annual Research Achievements

本研究の目標は、多相型プログラム（複数の型に対して動作しうるプログラム）に対してテストを効果的に行う手法の開発である。多相型プログラムでは、そのプログラムが動作しうる型が原理的には無限にあり得るので、どの型の入力をテストすれば良いのかの判断が難しい。この状況に対し、本研究では、特定の型、特に真偽値型のみでテストを行っても、プログラムの誤りを必ず発見できる（これを本研究では「有限テスト」と呼ぶ）ためにはどうすれば良いかを明らかにしたい。
本年度で特に取り組んだのは以下の3点である。
(1) 直接の先行研究（Bernerdyら'10, Christiansenら'11, Houら'22）の手法の有用性と限界を詳しく調査した。これらの手法では、真偽値型ではなく、自然数型（またはそれに類する型）によってテストを行う。この調査によって、本研究で探求する手法は既存手法とは直交するものであること、既存手法ではテストが事実上不可能になる例があること、などが明らかになった。
(2) 関数型言語Haskellの標準ライブラリに含まれる多相型プログラムを調査し、実用的な多相型プログラムでの有限テストの可能性を調査した。この調査によって、原理的には過半の多相型プログラムが有限テスト可能であること、しかしそれを機械的に確かめる手法は非自明であることが明らかになった。
(3) (2)での調査結果をふまえ、単純な手法では有限テストが難しいプログラムを、より有限テストに適したプログラムに変換するプログラム変換を開発した。
これらの成果は、対外発表に向けて、現在論文を執筆中である。

Current Status of Research Progress

2: Research has progressed on the whole more than it was originally planned.

Reason

多相型プログラムを有限テストする上での基盤となる理解が得られたと考えている。特に、Haskellの標準ライブラリの調査は、関数型言語で典型的に現れる多相型がどのようなものであるか、それに対して有限テストする際の難しさがどのような点にあるかについて、具体的かつ精度の高い分析となったと考えている。

Strategy for Future Research Activity

まずは国内の研究集会などで発表し、関連研究や今後の発展の可能性について調査する。その後、国際学術学会・国際学術雑誌での発表・出版を目指す。

Causes of Carryover

本年度中には研究成果を対外発表するにいたらか無かったことが最大の原因である。よって、次年度使用額は、次年度以降順調に研究が進捗すれば自然に解消されると考えている。