2011 Fiscal Year Annual Research Report
バグのないソフトウェア構築環境に関する研究の新展開
| Project/Area Number |
22300008
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
佐藤 雅彦 京都大学, 情報学研究科, 教授 (20027387)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
五十嵐 淳 京都大学, 情報学研究科, 准教授 (40323456)
中澤 巧爾 京都大学, 情報学研究科, 助教 (80362581)
山本 章博 京都大学, 情報学研究科, 教授 (30230535)
湯浅 太一 京都大学, 情報学研究科, 教授 (60158326)
|
|---|
| Keywords | 自然枠組 / ソフトウェア開発 / ソフトウェア検証 / メタ言語 / メタ理論 / 式の理論 / 抽象操作 |
|---|
| Research Abstract |
本研究では,プログラムの正しさを保証するための検証システム,および,その検証自体の正しさを保証するメタ理論に関する議諭をともに行うことのできるフレームワークの実装に向けて,自然枠組(Natural Framework, NF>の設計と構築を行っている.本年度は,NFを実装するためのプログラミング言語のプロトタイプの実装を行った.より具体的には以下のとおりである.
この言語の中核部分で必要となる数学的対象は,それぞれ,ある基本的な「概念」(concept)を満足するものとして特徴づけられるという重要な性質をもつ.このような対象を「第一種の数学的対象」と呼び,その対象の集りがつくる数学的構造についての研究を前年度に引き続き研究した.このような対象の多くは,単射的な帰納的定義により比較的容易に構築することができる.しかしながら,命題や証明を第一種の数学的対象として構築するのには単射的でない帰納的定義が必要になる.今年度は,命題や証明同士の等しさが決定可能であるという基本性質を満足した上で.これらを第一種の数学的対象として定義することに成功した.
今後は,この設計をもとに言語の実装を行い,このプログラミング言語の上でNFを実現することが期待される.
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
懸案であった,命題や証明を第一種の対象として把握し,等しさの決定手続きを与えることにも成功した.
|
| Strategy for Future Research Activity |
プログラミングの仕様がほぼ確定したので,今後は効率的な実装を行ない,その上で自然枠組を構築する.
|
