2004 Fiscal Year Annual Research Report
| Project/Area Number |
16500071
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Research Institution | Hosei University |
|---|
Principal Investigator |
宮本 健司 法政大学, 工学部, 助教授 (40339502)
|
|---|
| Keywords | プログラム / データベース / プログラム検証 / 意味検索 / 型理論 |
|---|
| Research Abstract |
プログラムコードを蓄積/再利用する方法について報告する.
プログラムコードのデータベースは従来から提案されてきたがいずれも,蓄積プログラムに関する属性記述が限定されており,特に意味から検索することはできなかった.また蓄積データ自体も特定の言語で書かれたプログラム専用であるうえに得られたプログラムの安全性についての保証は何もなかった.
今回報告する方法は
1.所望の意味をもつプログラムを容易に検索できること(意味検索可能性)
2.検索の結果得られたプログラムが容易かつ安全に再利用できること(再利用可能性)
の2つを目的とする.
提案方法では,データ構造の集合論解釈と意味仕様に関する検証証明を蓄積プログラムに添付する.加えて,プログラム記述には「抽象コード」とよぶ,抽象的に計算を記述する方法を用いる.
今回は「抽象コード」用の言語として「帰納的定義つき型理論」を選びこれに対してホーア論理にもとづく検証系を新たに開発した.リスト型データを集合と解釈する機構および抽象コードで書かれたプログラムおよび証明(木)をXMLで保存する様式と,Java言語への翻訳規則を定義した.
これらによりクエリとして所望の仕様を集合論論理式で入力すればデータベース内の該当意味のプログラムを検索しJavaプログラムに翻訳して出力するシステムが実装可能となった.
蓄積用の検証証明作成は,現在手作業作成で行なっているが本方法の実用性を高めるには既存のプログラムの(半)自動データ化の技術の確立が急務であることがわかった.
実用的なプログラムの中には今回利用した型理論の記述力を越えるものも多くあり,型理論自体を蓄積データとして記述可能にする必要性が明らかになった.
|
