プログラム抽出法の新展開　－－　証明自動化と高性能の両立

点击翻译按钮获取中文摘要

(1) 前年度に引き続き FLOPS 2018 の採録論文の論文誌版の改訂を行い、Science of Computer Programming (Elsevier) に採録となった。当該改訂の過程で、表現の問題のみならず技術的な面での改善を行った。特に顕著なものとしては、「定理証明器 Coq の効率的な有限ドメイン関数ライブラリ」（情報処理学会論文誌 プログラミング）で提案したMathematical Components の方式・習慣に従って書かれた既存の形式証明ライブラリを、それを使う証明との互換性を維持しつつ変更する技法を、理論的裏付けがより明らかな形で改善したことが挙げられる。(2) 前年度に引き続き、各種量化子除去アルゴリズムの形式検証に向けて、Mathematical Components ライブラリに order ライブラリを取り込み、numeric domain/field の補題を整理した。これらの変更はすでに Mathematical Components 1.11.0 の一部としてリリースされている。また、それらに加えて区間に関する定義や補題の一般化に取り組み、束上の区間の集合が包含関係、共通部分、凸包について束をなすこと、また同様に全順序集合上の区間の集合が分配束をなすことを証明した。これによって、区間の包含関係に関する命題を、束論の問題に帰着して示すことが可能となった。(3) 上述の(2)の過程で Mathematical Components の代数構造の階層に新しい構造を追加する上での技術的問題を見出し、packed classes の形式で記述された代数構造の階層の実装上の誤りを検出するアルゴリズムを提案し、それを実際に使える検証ツールとして実装した。また、より高レベルな代数構造の定義の記述から packed classes の形式での定義を自動生成するためのツールの開発を行った。