2016 Fiscal Year Annual Research Report
Construction of a self-extendable software verification system based on class theory
| Project/Area Number |
25280025
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
佐藤 雅彦 京都大学, 情報学研究科, 名誉教授 (20027387)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
外山 芳人 東北大学, 電気通信研究所, 教授 (00251968)
五十嵐 淳 京都大学, 情報学研究科, 教授 (40323456)
桜井 貴文 千葉大学, 理学(系)研究科(研究院), 教授 (60183373)
|
|---|
| Project Period (FY) |
2013-04-01 – 2017-03-31
|
| Keywords | 仕様記述・検証 / 証明支援系 / 型理論 / ソフトウェアの安全性 |
|---|
| Outline of Annual Research Achievements |
ソフトウェアの安全性を検証するための理論として、論理学の手法を用いて形式的体系性質の記述および検証を数学的に厳密な方法で行なう言語体系であるロジカル・フレームワーク(論理枠組)が提案されている。
形式的な計算体系であるプログラミング言語をロジカル・フレームワーク上で記述するとにより、ソフトウェアの求められる仕様を正確に記述し、与えられたソフトウェアがそ仕様を満足することを厳密に検証することが可能となる。さらにロジカル・フレームワーを計算機上に実装することができれば、これらの記述・検証の機械的に正確な検査が可能なり、ソフトウェアの品質面、安全面の信頼性が高まることが期待される。
本年度はフレーゲが考案した「概念記法」に注目し、それの現代的意義を考察して、ロジカル・フレームワークの言語設計に反映した。フレーゲは、言語のメタレベル、対象レベルの階層に留意して、文字の種類を複数用意し、階層の違いを明瞭に区別している。
我々のロジカル・フレームワークの特徴は、メタ言語を用いて、対象言語について引用したり、引用の一部にメタ言語を挿入できるというものである。フレーゲのアイデアはこの言語の特徴をコンピュータの上に実現するための有用な基盤になると考えている。
上のプランに基づきクラス理論の設計をし、並行してロジカル・フレームワークの実装を進めた。とくに、クラス理論については、名前の階層を各自然数に対してレベル付けをすることにより、どのレベルについてもさらに一段上のメタレベルの言語を利用可能にした。これによラムダ計算のメタ理論の証明を実装した。
|
| Research Progress Status |
28年度が最終年度であるため、記入しない。
|
| Strategy for Future Research Activity |
28年度が最終年度であるため、記入しない。
|
| Causes of Carryover |
28年度が最終年度であるため、記入しない。
|
| Expenditure Plan for Carryover Budget |
28年度が最終年度であるため、記入しない。
|
