Study of database for programs
| Project/Area Number |
16500071
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
Media informatics/Database
|
|---|
| Research Institution | Hosei University |
|---|
Principal Investigator |
MIYAMOTO Kenji Hosei University, Facuhy of Engineering, Associate Professor (40339502)
|
|---|
| Project Period (FY) |
2004 – 2007
|
| Project Status |
Completed (Fiscal Year 2007)
|
| Budget Amount *help |
¥3,250,000 (Direct Cost: ¥3,100,000、Indirect Cost: ¥150,000)
Fiscal Year 2007: ¥650,000 (Direct Cost: ¥500,000、Indirect Cost: ¥150,000)
Fiscal Year 2006: ¥800,000 (Direct Cost: ¥800,000)
Fiscal Year 2005: ¥700,000 (Direct Cost: ¥700,000)
Fiscal Year 2004: ¥1,100,000 (Direct Cost: ¥1,100,000)
|
|---|
| Keywords | program / verification / Hoare Logic / database / Web2.0 / learning / XML / program construction / 検索 / 仕様抽出 / 自動証明 / 再生産 / プログラム / 意味検索 / 型理論 |
|---|
| Research Abstract |
The aim of this research is to establish a framework for sharing complex procedural knowledge.
Current Semantic Web technology provides a knowledge-sharing framework by sharing meta-level explicit semantics and adding tags indicating their meanings.
Semantic Web is supposed, however, for concrete data in specific domain and is not suitable for procedural knowledge such as problem solving.
The presented approach emphasizes reusability of structural knowledse composed of many components of rather few kinds. To be properly reused, this kind of knowledge requires additional care of being prepared specifiable, applicable, and validatable.
To investigate such mechanism, database of programs was desisned.
In storing programs, Floyd-Hoare verification proofs are appended along with their abstract syntax trees.
The searchins process descends the tree testins whether each node meets the requirement. If a node which meets the requirement is found, the subtree rooted from it is returned.
Receiving the subtree, the client program check the proof tree and instantiate it to concrete syntax with variable names accommodated.
As the result, the proposed database meets the above requirements:
1. Specifiablility : Logical meaning is used to specify the target program, not keywords or function names.
2. Applicability : Although stored in abstract form, retrieved programs are instantiated ready to use.
3. Validatability : The meaning of the retrieved program can be certified before actual use.
In addition to the above result, it was investigated how the availability is improved.
If the first search trial fails, the improved system repeatedly change the requirement so that, if the answer to the new requirement is found, answer to the original one can easily be construct from it.
By adding the newly constructed program back to the program store, the database can be fed automatically each time it is used. This self-feeding mechanism makes the database Web2.0.
|
Report
(5 results)
Research Products
(5 results)
-
-
[Journal Article]2006
Author(s)
山本航, 宮本健司, 関川浩, 白柳潔
-
Journal Title
京都大学数理解析研究所研究録 "Computer Algebra…Design of Algorithms, Implementations and Applications" 1514
Pages: 164-170
Related Report
-
-
-
