Finite Testing with Correctness Guarantee for Polymorphic Programs

• Project/Area Number: 23K11044
• Research Category: Grant-in-Aid for Scientific Research (C)
• Allocation Type: Multi-year Fund
• Section: 一般
• Review Section: Basic Section 60050:Software-related
• Research Institution: The University of Tokyo
• Principal Investigator: 森畑 明昌 東京大学, 大学院総合文化研究科, 准教授 (10582257)
• Project Period (FY): 2023-04-01 – 2028-03-31
• Project Status: Granted (Fiscal Year 2023)
• Budget Amount: ¥2,990,000 (Direct Cost: ¥2,300,000、Indirect Cost: ¥690,000); Fiscal Year 2027: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000); Fiscal Year 2026: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000); Fiscal Year 2025: ¥260,000 (Direct Cost: ¥200,000、Indirect Cost: ¥60,000); Fiscal Year 2024: ¥390,000 (Direct Cost: ¥300,000、Indirect Cost: ¥90,000); Fiscal Year 2023: ¥520,000 (Direct Cost: ¥400,000、Indirect Cost: ¥120,000)
• Keywords: テスト / 多相型 / 関数型言語 / 型パラメトリシティ / 多相プログラム / 木変換器

Outline of Research at the Start

ソフトウェアに対するテストとは，実際に様々な入力で動作させてみて，意図せぬ挙動を
しないか確認する手法である。テストは現代のソフトウェア開発の根幹をなしている。しかし，1つのプログラムが様々な型の値に対して動作する（多相性をもつ）場合，あらゆる型の入力を試すことはできないため，テストが難しい。この問題を解決するため，多相性をもつプログラムに対し，有限種類の入力をテストするだけで正しさが検証できるための条件の解明を目指す。具体的には，有限種類の型に対する型検査を多相性をもつプログラムへのテストで代替することを考えている。

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

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