2010 Fiscal Year Self-evaluation Report
Development of formally verifiable framework for program transformation
| Project/Area Number |
20500011
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Single-year Grants |
|---|
| Section | 一般 |
|---|
| Research Field |
Fundamental theory of informatics
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
NISHIMURA Susumu Kyoto University, 大学院・理学研究科, 准教授 (10283681)
|
|---|
| Project Period (FY) |
2008 – 2011
|
| Keywords | プログラム理論 / プログラム変換 / 形式的証明 |
|---|
| Research Abstract |
プログラム変換は以前から研究されてきているテーマであるが、これまで提案されてきた個々の変換手法が本当に正しいかどうかは必ずしも明らかではない。特に、プログラム変換の対象をポインタ操作・大域的制御・並行計算プリミティブなどの実際のプログラムに含まれるものにまで拡張したときについては研究が進んでいない。正しさが必ずしも保証されないということは、プログラム変換を適用することによってプログラムがうまく動かなくなってしまう可能性があるということであり、これは高度な安全性の要求される分野においては絶対許されないことである。
本研究は、プログラム変換が正しいこと、すなわち意図したプログラムの動作がプログラム変換の前後で変化しないことを保証するため、プログラム変換工程の形式的検証のためのフレームワークを定理証明支援系等の上に構築することを可能とするような理論的基礎を確立することを目的とする。このような目的を達成するため、プログラム単体の意味(プログラムの動作)および変換前後のプログラムの対応関係を厳密に定義し、これらを形式的に記述できるようにする。このため、本研究では、形式的技法(formal methods)の分野で仕様からプログラムを導出するための詳細化と呼ばれる技法を基本とし、これをプログラム変換の過程において適用することによってプログラム変換の正しさを保証するフレームワークを構築する。具体的には、詳細化技法の基礎となっている述語変換子意味論を、従来の古典論理による形式化から拡張することによって、上記のような実際的なプログラミング概念に対応する。
|
