| 研究課題/領域番号 |
19K11891
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 審査区分 |
小区分60050:ソフトウェア関連
|
|---|
| 研究機関 | 東北大学 |
|---|
研究代表者 |
菊池 健太郎 東北大学, 電気通信研究所, 助教 (40396528)
|
|---|
| 研究期間 (年度) |
2019-04-01 – 2025-03-31
|
| 研究課題ステータス |
交付 (2023年度)
|
| 配分額 *注記 |
3,640千円 (直接経費: 2,800千円、間接経費: 840千円)
2022年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円)
2021年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円)
2020年度: 650千円 (直接経費: 500千円、間接経費: 150千円)
2019年度: 650千円 (直接経費: 500千円、間接経費: 150千円)
|
|---|
| キーワード | 書き換えシステム / プログラム検証 / 帰納的定理 / 合流性 / 局所十分完全性 |
|---|
| 研究開始時の研究の概要 |
本研究では、定理自動証明や代数的仕様記述の分野で用いられてきた書き換えシステムに基づく検証手法を、プログラムおよびプログラミング言語の性質を証明するために適した方向へ拡張し、ソフトウェアの信頼性を向上させる技術として役立てることを目的としている。具体的には、研究代表者らが近年開発を進めている新しい高階書き換え理論に基づいて、主に遅延評価の関数型プログラムの性質を可能な限り自動で検証するための枠組みを構築することを目指す。
|
| 研究実績の概要 |
研究期間の初年度に発表した論文により、帰納的定理の証明手法である潜在帰納法の適用のためには合流性と局所十分完全性が本質的であるということが明らかになっている。本年度の研究では、局所十分完全性に関する以下の成果・知見が得られた。
前々年度に国際会議で発表した導出システムによる判定手続きの実装に指導学生とともに取り組んだ。停止性を持たない項書き換えシステムに対する十分完全性や局所十分完全性の判定手続きの実装は、既存研究では与えられていない。本研究では、導出システムの推論規則を効率よく適用する順序等を考慮した判定手続きを、関数型プログラミング言語を用いて実装し、具体例に対して適切に動作することを確認した。
さらに、既存研究では判定の対象とされていなかった項も扱えるよう判定手続きを拡張することに取り組んだ。従来の手法では、例えば、リストの長さを計算する関数が引数として無限リストを表す項をとった時に、局所十分完全性が成立しなくなる。しかし、同じ関数が有限のリストを値として持つ項を引数としてとったならば、計算結果としてリストの長さを返すため、局所十分完全性が成立する可能性は残存する。本研究では、有限のデータを表すソートとそうではないソートの間に順序を導入することでソート付き項の概念を拡張し、従来は判定の対象とされていなかった項も扱うことを可能にした。これにより、局所十分完全性を判定できる項の範囲が著しく拡大した。また、上述の実装を変更することにより、この拡張された手続きに対する実装を与えた。
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
書き換えシステムに基づくプログラム検証手法を開発するために重要と考えられる合流性については、束縛変数を伴う書き換えシステムにおける成立条件に関する成果を発表してきた。また、局所十分完全性については、判定手続きの提案とその拡張・実装を行ってきている。以上のことから、研究はおおむね順調に進展していると判断した。
|
| 今後の研究の推進方策 |
合流性については、名目書き換えシステムに関してこれまでに得られた知見をもとに、束縛変数を伴う書き換えシステムに対する判定手続きの構築に取り組む。局所十分完全性については、引き続き関連する手法に対して調査を進め、関数型プログラミング言語のモデルとなる体系における類似の性質を判定する手法の構築に取り組む。以上を含めたこれまでの成果・知見に基づくプログラム検証手法を実際のプログラムの例に適用することにより、その有効性を明らかにする。
|
