| 研究課題/領域番号 |
16500071
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 補助金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
メディア情報学・データベース
|
|---|
| 研究機関 | 法政大学 |
|---|
研究代表者 |
宮本 健司 法政大学, 工学部, 助教授 (40339502)
|
|---|
| 研究期間 (年度) |
2004 – 2007
|
| 研究課題ステータス |
完了 (2007年度)
|
| 配分額 *注記 |
3,250千円 (直接経費: 3,100千円、間接経費: 150千円)
2007年度: 650千円 (直接経費: 500千円、間接経費: 150千円)
2006年度: 800千円 (直接経費: 800千円)
2005年度: 700千円 (直接経費: 700千円)
2004年度: 1,100千円 (直接経費: 1,100千円)
|
|---|
| キーワード | プログラム検証 / Web検索 / Hoare論理 / データベース / Web2.0 / 学習 / XML / プログラム合成 / 検索 / 仕様抽出 / 自動証明 / 再生産 / プログラム / 意味検索 / 型理論 |
|---|
| 研究概要 |
プログラムを例にとって、問題解決の方法など複雑かつ抽象的な知識を共有し再利用する仕組みについて研究を行なった。
このような知識共有メカニズムに一般的に要求される性質として、解決すべき問題ないしは仕様から所望の知識を特定/検索できること(検索可能性)、その解決方法の妥当性(検証可能性)得られた解決方法が具体的な問題に適用可能であること(適用可能性)、の3点を特定し、そのプログラムの領域における例としてプログラムのデータベースの実現ついて検討した。
1.検索可能性:プログラムをその仕様とともに蓄積し、仕様をキーとして蓄積データから検索することを考案した。具体的にはHoare論理にもとづく仕様記述を抽象コード断片に付与して蓄積することで実現する。
2.検証可能性:Hoare論理にもとづく仕様記述はプログラムの構文要素ごとに付与することで検証証明となり得ることを利用し、検索結果出力に証明を付与する。証明はプログラム利用者の検査器を通じて検査できる。これにより仕様を充足することの検証可能性を提供する。
3.適用可能性、抽象コードは変数名、型の調整を含めて所望の具体的コードに変換される。これにより具体的なプログラムとして使用可能になる。
以上を基本方法として、さらに次の拡張を行なった。適合するプログラムコードが蓄積されていなかったときに、Hoare論理の合成規則の逆にしたがって仕様を部分プログラムの仕様に分解し,得られるもの(部分仕様)を新たな検索キーとして検索するという動作を再帰的に繰返し、コードが見つかった場合には、そのコードを分解時の規則を用いて再構成し、当初の検索キーに適合するコードとして出力することを提案した.新たに得たプログラムを蓄積データとしてフィードバックすることで利用ごとに強化されるWeb2.0的特徴を具備し得る。
|
