2013 Fiscal Year Annual Research Report
クラス理論に基づく自己拡張可能なソフトウェア検証体系の構築
| Project/Area Number |
25280025
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (B)
|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
佐藤 雅彦 京都大学, 情報学研究科, 名誉教授 (20027387)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
外山 芳人 東北大学, 電気通信研究所, 教授 (00251968)
桜井 貴文 千葉大学, 理学(系)研究科(研究院), 教授 (60183373)
五十嵐 淳 京都大学, 情報学研究科, 教授 (40323456)
|
|---|
| Project Period (FY) |
2013-04-01 – 2017-03-31
|
| Keywords | クラス理論 / 型理論 / 証明検証 / ソフトウェアの安全性 |
|---|
| Research Abstract |
ソフトウェアの安全性を検証するための理論として，論理学の手法を用いて形式的体系の性質の記述及び検証を数学的に厳密な方法で行なう言語体系である ロジカル・フレームワーク (論理枠組) が提案されている．形式的な計算体系であるプログラミング言語をロジカル・フレームワーク上で記述することにより，ソフトウェアに求められる仕様を正確に記述し，与えられたソフトウェアがその仕様を満足することを厳密に検証することが可能となる．さらにロジカル・フレームワークを計算機上に実装することができれば，これ
らの記述・検証の機械的に正確な検査が可能となり，ソフトウェアの品質面，安全面の信頼性が高まることが期待される．
変数の束縛機構は，プログラミング言語とくに関数型言語における基本的な研究課題であり多数の研究者により長年研究がされてきている．今年度の研究では，最近得られた map と skeleton を用いた変数の束縛表現について，この表現を単純型付 λ計算について適用するとどうなるかを考察した．その結果，この計算体系に関して，従来証明が非自明であった「文脈の水増し(weakening)規則が許容される規則であること」を自然に証明できことが確認できた．
またロジカル・フレームワークの基礎となるクラス理論の実装についての考察を行った。新しく得られた知見としては、数学的対象として、伝統的な論理学では考察の対象とされていなかった、自己が動的に変化する対象をクラスのインスタンスとして取り入れる必要があることがわかった。
|
| 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 |
変数の束縛機構について新しい知見が得られたことを踏まえて、クラスのインスタンスの実装の方法を再検討する予定である。
クラス理論の全体構想は固まりつつあるので、更に理論的な検討を加えながら、体系の実装についての設計を詳細化する。
|
