2009 Fiscal Year Annual Research Report
計算と論理の融合によるバグのないソフトウェア構築環境に関する研究
| Project/Area Number |
19300007
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
佐藤 雅彦 Kyoto University, 情報学研究科, 教授 (20027387)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
五十嵐 淳 京都大学, 情報学研究科, 准教授 (40323456)
中澤 巧爾 京都大学, 情報学研究科, 助教 (80362581)
山本 章博 京都大学, 情報学研究科, 教授 (30230535)
湯浅 太一 京都大学, 情報学研究科, 教授 (60158326)
|
|---|
| Keywords | 自然枠組 / ソフトウェア開発 / ソフトウェア検証 / メタ言語 / メタ理論 / 式の理論 / 抽象操作 |
|---|
| Research Abstract |
本研究では,プログラムの正しさを保証するための検証システム,および,その検証自体の正しさを保証するメタ理論に関する議論をともに行なうことができるフレームワークの実装に向けて,自然枠組(Natural Framework, NF)の設計と構築を行なっているが,本年度は,NFを実装するためのプログラミング言語の設計を行なった.より具体的には以下のとおりである.
昨年度までに,NFのための理論的基盤を与えるために,とくにその構文論的基礎を与える式の理論に関する考察を行なってきたが,本年度はこの中で得られた知見をもとに,NFをコンピュータ上で実現するためのプログラミング言語設計を行なった.この言語の中核部分で必要となる数学的対象は,それぞれ,ある基本的な「概念」(concept)を満足するものとして特徴づけられ,そのため抽象化の操作を必要としない帰納的な記号操作でこれらの数学的対象が構成できることを示した.
今後は,この設計をもとに実装を行ない,このプログラミング言語の上でNFを実現し,プログラム検証およびそのメタ理論に関する議論をコンピュータ上の同じ枠組みで行なえる環境が構築されることが期待される.
|
