ランキング関数の回帰推定による関数型言語の停止性検証

村本, 大起, 佐藤, 亮介, 鵜林, 尚靖, 亀井, 靖高

プログラムの停止性検証は重要な研究課題の1つである．停止性検証を行う手法として，遷移不変条件となるランキング関数を推定するものが有力である．ここで，ランキング関数とはループまたは再帰ごとに値がつねに減少し，かつつねに正となる性質を持つ写像である．既存研究では，高階関数を含む関数型言語に対しSMTソルバを用いてランキング関数を推定し停止性検証を行っているが，末尾再帰関数のような制御フローに直接かかわらない引数を多く含むものに関しては正しい推定が難しく，簡単な書き換えによって検証できなくなるものが存在していた．本研究では，ランキング関数の推定方法に線形回帰を用いて，制御フローに関係のない引数を多く含むプログラムについてもなるべく検証ができるように改善を行う．提案する関数の停止性の検証手法は，まず仮のランキング関数を定める．そしてランキング関数が妥当であるかをチェックする．ランキング関数が妥当であれば検証成功．そうでない場合，得られた反例から引数の実際にとる値を取得する．得られた引数の値から新たなランキング関数を線形回帰で推定してランキング関数の妥当性検証へ戻り，妥当性検証が成功するまで繰り返し行う．また，本手法のプロトタイプとしてOCamlのサブセットを対象とした停止性検証器ツールを作成した．そして，ツールを用いて自動で検証できるものを調査した実験についても報告する．

Termination verification is one of the important research topics. One way to verify the termination of a program is to infer a ranking function, which is monotonically decreasing and is always positive. An existing method for verifying termination of higher-order functional programs via inference of ranking functions has difficulty with accurate inference of ranking functions for programs whose arguments do not relate directly to its control flow like tail recursive functions, and there are some simple transformed programs cannot be verified by the method. In this presentation, we improve the existing method by using linear regression in order to verify such programs as much as possible. Our approach follows: set temporary ranking function, check if ranking function is valid, success verification if ranking function is valid. Otherwise, generate an assignment of the value to the variable from the obtained counterexample, infer ranking function via linear regression, and return to verification of ranking function. In this presentation, we implement the prototype of our method and show preliminary experiments.

ランキング関数の回帰推定による関数型言語の停止性検証

書誌事項

この論文をさがす

抄録

収録刊行物

キーワード

詳細情報詳細情報について

書き出し

問題の指摘

ランキング関数の回帰推定による関数型言語の停止性検証

書誌事項

この論文をさがす

抄録

収録刊行物

キーワード

詳細情報 詳細情報について

書き出し

問題の指摘

詳細情報詳細情報について