2008 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の基礎となる「式の理論」を与えるために、抽象(abstraction)操作について考察した.
数学を形式的に記述するときに変数による抽象操作は必須となる基本的な操作である.この操作は,与えられた変数xと表現Mから,表現abs(x, M)を構成する操作であり,その結果はMのxによる抽象と呼ばれる.この操作の「逆操作」は具体化(instantiation)と呼ばれ,抽象Aを表現Nで具体化した結果はinst(A,N)と書かれる.抽象と具体化の間には以下の関係がある:
Inst(abs(x,M),N)=[N/x]M.
本研究では,これらの性質をもつ抽象操作を実現する具体的な新しい方法を提案した.この手法はNFの「式の理論」に組み込まれ,NFにおける抽象操作の理論的基盤を与えることが期待されるが,本手法自体はNFに限らない,一般の抽象操作を表現できるものである.
|
