Java Stream APIによるストリー厶操作の停止性検査のための型システム

摘要

本論文では，Stream APIを用いるJavaプログラム中の停止しないストリーム操作を検出するための型システムを提案する.Java Stream APIを用いることでデータ集合に対する操作を宣言的に記述できる.Stream APIには多くのストリーム操作があり，ストリーム中の要素が有限個のストリームと無限個のストリーム双方に対して適用できるが，いくつかの操作は無限個の要素を持つストリームに対して停止しない可能性がある.本論文で提案する型システムは無限個の要素を持つストリームに対して停止しない操作を検出できる.型システムの健全性を証明し，型システムに基づく型検査器をChecker Frameworkを用いて実装した.