2012 Fiscal Year Annual Research Report
バグのないソフトウェア構築環境に関する研究の新展開
| Project/Area Number |
22300008
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
佐藤 雅彦 京都大学, 情報学研究科, 名誉教授 (20027387)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
山本 章博 京都大学, 情報学研究科, 教授 (30230535)
五十嵐 淳 京都大学, 情報学研究科, 教授 (40323456)
中澤 巧爾 京都大学, 情報学研究科, 助教 (80362581)
|
|---|
| Project Period (FY) |
2010-04-01 – 2013-03-31
|
| Keywords | ソフトウェア検証 / クラス理論 / ソフトウェアの安全性 / 型理論 / 項書換 |
|---|
| Research Abstract |
本研究は、ソフトウェアの安全性および品質の保証に対する社会的要求に応えることを目的とし、平成22年度から平成24年度にかけて研究を行なってきた。本研究では、この目的を達成するためには、バグのないソフトウェアの構築環境の実現が必須であるとの認識の基で研究を進めてきた。平成24年度は最終年度であり、以下のように研究を実施、成果をあげることができた。
(1) 自然枠組(Natural Framework, NF)の理論基盤の深化。これまで、NF で扱う数学的対象は、ヒルベルトの有限の立場で言うところの有限的対象に限ることにし、これらの対象を「第一種の対象」と呼んできた。本年度は、さらに、これら第一種の対象をどれもある特定のクラスに属する対象として分類することが有用であることを示すことができた。
(2) NF 実装言語 Ez の改良。NF を実装するため、本研究では新しいプログラミング言語 Ez を設計、開発してきた。本年度は、(1)で導入したクラスを第一種の対象として直接 Ez のデータとして処理できるようにした。これにより、ソフトウェアを検証するための論理体系を自然に実現できるようになった。
(3) λ項のデータ構造の研究。抽象化(abstraction)により構成される構造体は計算と論理のいずれにおいても基本的な対象であり、λ項を用いて自然に実現できることが知られている。しかし、λ項をデータ型として表現し、その上での帰納的な推論を自然な形で記述できるようにする方法は従来知られていなかった。これについて、海外の2名の研究者の協力を得て、λ項のデータ型を提案し、用な性質を証明することができた。
|
| Current Status of Research Progress |
Reason
24年度が最終年度であるため、記入しない。
|
| Strategy for Future Research Activity |
24年度が最終年度であるため、記入しない。
|
