2019 Fiscal Year Research-status Report
Development of Verification Techniques for Equivalence of Programs via Rewriting Induction
| Project/Area Number |
18K11160
|
|---|
| Research Institution | Nagoya University |
|---|
Principal Investigator |
西田 直樹 名古屋大学, 情報学研究科, 准教授 (00397449)
|
|---|
| Project Period (FY) |
2018-04-01 – 2023-03-31
|
| Keywords | プログラム検証 / 項書換えシステム / プログラム変換 / 計算モデル / 帰納法 / 定理自動証明 / 補題生成 |
|---|
| Outline of Annual Research Achievements |
当初の研究計画における2年目の課題は（A）書換え帰納法の推論規則の適用戦略の開発（初年度から継続），（B）等式と不等式が混同した枠組みへの書換え帰納法の拡張，（C）対話型定理証明器Isabelle/HOL上での書換え帰納法の形式化（3年目まで）であった．また，初年度の研究により，（D）ビットベクトルを扱うLCTRS（BV-LCTRS）の停止性証明法の開発，（E）拡張性の高い検証ツールの再実装を加えた5つの課題に取り組んだ．
（A）については3年目に取り組む予定であった補題生成法の開発を前倒して実施し，補題生成と合わせて適用戦略について検討した．先行研究での方法では変数間の関係性を失い，成り立たない補題候補の等式へと一般化してしまうことがあるため，ラグランジュ補間を用いて変数間に成り立つ性質を発散等式の列から求めて制約に追加するアプローチを考案した．（B）については，不等式を扱うのではなく，不等式と等価な存在限量子付き等式に変換し，書換え機能法を存在限量子付き等式へ拡張するアプローチで行った．（C）については，単純な命令型言語であるIMPからLCTRSへの変換とその正当性まで形式化し，書換え帰納法によるプログラム検証に対する証明承認ツールの基盤となる理論の一部の形式化を終えた．（D）については，一重の標準的なforループを持つプログラムから変換して得られるBV-LCTRSの停止性を証明する定理を導き，その正しさを証明した．（E）については，標準でないライブラリを用いない方針のもとで実施した．入力ファイルの構文への拡張性についてはOcamlのlex/yaccを用いて実装し，LCTRSの基本データ型として整数，ブール，ビットベクトル ，それらの配列を扱えるようにした．書換え機能法は対話型での推論規則の適用の形式で実装した．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
本研究の目的の一つは論理制約付き項書換えシステムへの変換と帰納法に基づく証明体系を命令型プログラムに応用し，命令型プログラムの新たな検証法の枠組みを確立することである．また，2年目の目標は理論的な枠組みの拡張である．当初の研究計画の目標は予定通り達成できており，さらに初年度に明らかになったBV-LCTRSの停止性証明法の開発に取り組み，期待した成果を得た．補題生成法の開発についても3年目の実施予定を前倒しして取り組み，期待以上の成果の見込みがある．よって，2年目は予定していたよりも早く，そしてより多くの課題に取り組むことができ，本研究の目的を達成するための進捗として想定以上に目標を達成できている．
また，検証ツールを再実装したことも大きい．当初は既存ツールのCtrlを使用して研究を遂行する予定であったが，その拡張性の低さから研究遂行に支障をきたす恐れがあった．しかし，2年目に検証実験を行える状態まで再実装を終えることができた．3年目以降は再実装した検証ツールで予定通りに研究を遂行できる状態に至った．さらに再実装したツールはすべてのソースコードを自前で実装したため，デバッグ，拡張が容易である．よって，既存ツールを使用するよりも研究を加速させることが期待できる．
以上のことから本研究の進行状況は概ね順調であると言える．
|
| Strategy for Future Research Activity |
検証ツールを再実装し，対話的に書換え帰納法の推論規則を適用して証明を行うことによる実験は可能になったが，様々な例題で試行錯誤するには検証の自動化が必須である．そのために3年目には検証ツールの推論規則適用を自動化すること，補題生成機能を導入すること，停止性証明機能を充実させることが必要である．自動化の方法の一つとして，対話的証明支援系で採用されているような戦略記述による自動化を検討する．補題生成機能については2年目に提案したラグランジュ補間による手法を実装する．停止性証明機能については既存のツールを外部ツールとして呼び出して証明する方法，ビットベクトル の特徴に特化して証明する独自の方法を実装する．検証ツールの自動化に合わせて，ベンチマークによる実験を行い，推論規則の適用戦略，補題生成，停止性証明についてのヒューリスティックスを得るためのデータ収集にも取り組む．
並行プログラムをLCTRSで表現した際には，プロセスの数が固定でない場合はプロセスの集合を表す２引数関数記号を導入し，その関数記号が交換律・結合律（AC）を持つことを仮定した体系が自然である．よって，LCTRSの書換えを等式付き書換えに拡張し，並行プログラムを検証するための枠組みの構築を試みる．そのためにはLCTRSの書換え帰納法を等式付き書換えに対応するように拡張することも必要である．
2年目にLCTRSをIsabelle/HOL上で形式化した成果にもとづき，3年目にLCTRSの書換え帰納法の形式化にも取り組み，証明承認ツールで扱う証明の形式についても検討を行う．
|
