| 研究課題/領域番号 |
18K11160
|
|---|
| 研究機関 | 名古屋大学 |
|---|
研究代表者 |
西田 直樹 名古屋大学, 情報学研究科, 准教授 (00397449)
|
|---|
| 研究期間 (年度) |
2018-04-01 – 2023-03-31
|
| キーワード | プログラム検証 / 項書換えシステム / プログラム変換 / 計算モデル / 帰納法 / 定理自動証明 / 補題生成 |
|---|
| 研究実績の概要 |
当初の研究計画における3年目の課題は（A）書換え帰納法の推論規則の適用戦略の開発（初年度から最終年度まで継続），（B）補題等式の自動生成法の開発（3年目から最終年度まで），（C）LCTRSの書換え帰納法の等式付き書換えへの拡張（3，4年目）（D）対話型定理証明器Isabelle/HOL上での書換え帰納法の形式化（2，3年目）であった．また，2年目の並行プログラムの排他制御の検証に関する研究成果を踏まえ，（E）LCTRSによる並行プログラムのモデル化，(F）ビットベクトルをデータとして扱うLCTRSの停止性証明法の開発にも取り組んだ．
（A）については2年目に前倒しで（B）に取り組んで検討しており，（B）と合わせて，これまでに自動証明に成功していないプログラムの例に対して，自動で適切な補題を生成し，等価性証明に成功する補題生成法と適用戦略を提案した．具体的には証明を発散させる等式の列の特定の場所に注目して点列を抽出し，ラグランジュ補間を用いて等式を一般化する方法である．その手法では成り立たない補題等式を生成してしまうが，途中の証明の失敗を利用して適切な補題に修正する証明戦略を開発した．
（C）については循環証明システムと書換え帰納法を比較する課題に取り組み，等式付き書換えへの拡張の必要性を確認した．実際の拡張については4年目に取り組む．
（D）についてはLCTRSの形式化に取り組み，完了した．書換え帰納法の形式化は想定以上に難易度の高い課題であることがわかり，4年目に持ち越して実施する．
（E）については排他制御を含むプログラムからLCTRSへの変換を提案した．変換の正しさの証明のために並行実行の意味論を定義する簡易プログラミング言語SIMPの並行版を推論規則で定式化した．その意味論に対して4年目に変換の正当性を証明する．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
本研究の目的の一つである書換え帰納法に基づく検証法の開発については，これまでに自動証明できていないプログラム例に対して自動証明に成功する手法の開発に成功した．これは当初，3年目終了時に予定していた目標を達成している．また，並行プログラムからLCTRSへの変換については前倒しで研究を実施しており，期待して成果を得た．
Isabelle/HOL上での形式化についてはLCTRSの形式化を完了した一方で，LCTRSの書換え帰納法の形式化は完了しなかった．これは想定していた以上に難易度が高かったためである．よって，4年目以降も継続する．
以上のことから本研究の進行状況は概ね順調であると言える．
|
| 今後の研究の推進方策 |
本研究ではプログラムをより忠実に表現できるモデルとしてビットベクトルをデータとして扱うLCTRSを採用する．一方，ビットベクトルをデータとして扱えるLCTRSツールはまだ開発されていない．そのため，そのようなツールの開発は研究成果を評価するためにも急務である．そこで4年目以降にはビットベクトルを扱うLCTRSを対象とした検証ツールの開発を加速し，研究を推進させることを図る．具体的には，3年目に提案したビットベクトルを扱うLCTRSの停止性証明法を実装し，そのようなLCTRSに対して書換え帰納法による検証の実験・評価を行う．
Isabelle/HOL上での形式化については研究グループに所属する学生とともにIsabelle/HOLの理解を深め，複数名で取り組むことにより研究を推進する．具体的には，既に形式化したコードを見直し，書換え帰納法の形式化の観点から必要に応じて改良する．また，書換え帰納法の正当性証明そのものも形式化に適した証明を再考する．
|
| 次年度使用額が生じた理由 |
コロナ禍のため成果発表の場がすべてオンラインとなり，出張がなかったため旅費が発生しなかった．その分，2021年度に発表のための出張の回数，人員が増加することを見越して繰り越した．一部はツール開発・デモ用のノートPCの購入に使用し，残りの経費を2021年度後半に成果発表や研究打ち合わせのための旅費として使用する予定である．
|
