2007 Fiscal Year Final Research Report Summary
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
|
| 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.
|
