2007 Fiscal Year Annual Research Report
| Project/Area Number |
16500071
|
|---|
| Research Institution | Hosei University |
|---|
Principal Investigator |
宮本 健司 Hosei University, 工学部, 准教授 (40339502)
|
|---|
| Keywords | プログラム検証 / 検索 / Hoare論理 / データベース / Web2.0 / 学習 / XML / プログラム合成 |
|---|
| Research Abstract |
前年度までに得られた方法はプログラムを仕様とともに蓄積し,所望の仕様を問い合わせとして蓄積データとしてのプログラムを検索/取得するものであった.
しかしながらこの方法では(1)検索にヒットするコードは蓄積されたコードがそのまま論理的仕様に完全に合致するものだけに限られる。この結果、蓄積したプログラムを組み合わせ、少し加工することで所望のプログラムが得られるはずであるにも関わらず、仕様に直接適合しないがゆえに棄却されてしまうという問題が生じる.利用度の観点からは、そのままでは仕様に適合していなくでも、わずかの加工で所望の論理的仕様に適合するようになるプログラムを見い出して、再利用する方法が望まれる。
また(2)検証証明つきのプログラムデータを手動のみで入力して完備することは困難かつ非能率的である。プログラム資源を人手による証明にもとづくデータのみに依存する非効率を改善し、利用を重ねること自体によって自動的データを拡充できる学習機構が望まれる。
(1)の問題点に対する解決策として,適合するプログラムコードが蓄積されていなかったときに、Hoare論理め合成規則の逆にしたがって仕様を部分プログラムの仕様に分解し,得られるもの(部分仕様)を新たな検索キーとして検索するという動作を再帰的に繰返し、コードが見つかった場合には、そのコードを分解時の規則を用いて再構成し、当初の検索キーに適合するコードとして出力することを提案した.
(2)の問題点に対する解決策として,(1)で得られる出力を蓄積データに追加することで利用そのものによって蓄積データ拡充することを考案した.適合するプログラムの検索に失敗した場合、仕様のみを未解決デニタベースに登録し登録情報を周知する機構と、未解決要求に対する解としてのコードの送信を受け付け、正しさを検査のうえ解決済コードとしてコードのデータベースに登録する機構を考案した.
|
