研究課題
基盤研究(C)
プログラム変換は以前から研究されてきているテーマであるが、これまで提案されてきた個々の変換手法が本当に正しいかどうかは必ずしも明らかではない。特に、プログラム変換の対象をポインタ操作・大域的制御・並行計算プリミティブなどの実際のプログラムに含まれるものにまで拡張したときについては研究が進んでいない。正しさが必ずしも保証されないということは、プログラム変換を適用することによってプログラムがうまく動かなくなってしまう可能性があるということであり、これは高度な安全性の要求される分野においては絶対許されないことである。本研究は、プログラム変換が正しいこと、すなわち意図したプログラムの動作がプログラム変換の前後で変化しないことを保証するため、プログラム変換工程の形式的検証のためのフレームワークを定理証明支援系等の上に構築することを可能とするような理論的基礎を確立することを目的とする。このような目的を達成するため、プログラム単体の意味(プログラムの動作)および変換前後のプログラムの対応関係を厳密に定義し、これらを形式的に記述できるようにする。このため、本研究では、形式的技法(formal methods)の分野で仕様からプログラムを導出するための詳細化と呼ばれる技法を基本とし、これをプログラム変換の過程において適用することによってプログラム変換の正しさを保証するフレームワークを構築する。具体的には、詳細化技法の基礎となっている述語変換子意味論を、従来の古典論理による形式化から拡張することによって、上記のような実際的なプログラミング概念に対応する。
すべて 2011 2010 2009 2008 その他
すべて 雑誌論文 (2件) (うち査読あり 2件) 学会発表 (3件) 備考 (1件)
19th International Symposium, LOPSTR 2009, Revised Selected Papers (Lecture Notes in Computer Science) vol.6037
ページ: 113-127
Journal of Functional Programming vol.18(5-6)
ページ: 781-819
http://www.math.kyoto-u.ac.jp/~susumu/mpc08pvs/index.html
