2007 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)と呼ばれる枠組を提案しており,これを元にして,計算と論理を融合した自然枠組を設計・実装することを目指している.本年度はとくに自然枠組の基盤となる,対象を記述するための式の理論に関する理論的考察を行ない,以下の成果を得た.1.メタ変数(meta variable)の概念を形式化した.目標とする自然枠組において,プログラムなどの対象を,メタな立場から引用し,議論する枠組は必須である.このようなメタ言語中で用いられる引用において重要な役割を果たすメタ変数の概念を形式的に扱うために,階層的な対象を取り扱うための形式的体系を提案し,その性質を調べた.
2.目標とする自然枠組を記述する言語は必然的に形式的な言語になるが,その形式的言語(対象言語)を人間が理解するためには,最終的には自然言語をメタ言語として用いる必要がある.通常は,この対象言語とメタ言語は異る言語であるとされている.しかし,この見方とは対照的な,対象言語をメタ言語の部分言語とみなす見方が可能であることを提案し,その有用性を指摘した.
|
