2005 Fiscal Year Annual Research Report
| Project/Area Number |
16500071
|
|---|
| Research Institution | Hosei University |
|---|
Principal Investigator |
宮本 健司 法政大学, 工学部, 助教授 (40339502)
|
|---|
| Keywords | プログラム / データベース / プログラム検証 / 意味検索 / 型理論 |
|---|
| Research Abstract |
プログラムのデータベースの検索利用モデルの研究・実験に先だって実験用データベースの構築が急務である.今年度は既存のプログラム資源を再利用してプログラムコードのデータベースを構築する方法について検討した.
本研究が提案するプログラムのデータベースの利用モデルはHoare論理による検証を基礎としており,検証の証明を仕様からの検索に利用するものである.データベース構築時にはしかし,証明を手作業で添付するには膨大な手間がかかり現実的ではない.既存のコード資源に関しては,仕様書は通常存在せずあったとしても満たしている保証はない.そこで既存のコード資源を再利用して仕様保証プログラムのデータベースを構築するには,
(1)コードから自動的に仕様を抽出し,同時に
(2)その正しさを保証する検証証明を得る
必要がある.ただしここで要求する仕様は製作意図としての本来の仕様ではなく検索時に利用できる程度の弱いものでよい.
本研究では部分プログラムごとにHoare論理で保証できるだけの仕様を割り当てこれを再帰的に累積することでもとのプログラム全体の仕様を推定する方法を検討した.現在までに複合文,条件文について仕様推定方法が得られており,現在繰返し(while)文についていわゆるループ不変量の抽出方法を検討している.本方法はまた型推定とも関係があることが指摘されており検討を始めている.プログラム検証は本来厳密な要求仕様を与えて充足性検査をすることが目的であり検索という見地から応用を検討されたことはなかった.この見地からすれば検索用仕様に限定することである程度自動化できる可能性が出てきた.その一方で現在の方法で推定して得られた仕様は予想よりも複雑なものになり得ることが明らかになった.
|
