2009 Fiscal Year Annual Research Report
形式的に検証可能なプログラム変換フレームワークの構築
| Project/Area Number |
20500011
|
|---|
| Research Institution | Kyoto University |
|---|
Principal Investigator |
西村 進 Kyoto University, 大学院・理学研究科, 准教授 (10283681)
|
|---|
| Keywords | プログラム理論 / プログラム変換 / 形式的証明 |
|---|
| Research Abstract |
例外の発生と例外の補足を許すようなプログラムに関するプログラム変換を形式的に導出可能な枠組みとして、4値論理に基づくrefinement calculusを提案した。Refinement calculusは、プログラムあるいはプログラムの仕様から最終プログラムを段階的な詳細化(プログラム変換)によって導くための洗練された枠組みであるが、古典論理をその基礎としておりプログラムが正常に終了するかどうかの区別しかできない。実際のプログラムでは、実行時エラー(例えばゼロ除算など)によって実行を異常終了させたり、異常終了を補足して正常実行に復帰する仕組みが用意されているが、これらは従来のRefinement Calculusでは扱うことができなかった。今年度の研究では、古典論理に代えてArieliとAvronによる4値論理を用いることによって正常終了と異常終了を区別して扱うことを可能とし、これによって上記のような実行時エラーやエラーからの回復機構をもつプログラムについてプログラムの段階的な詳細化を形式的に導出することが可能となった。
この結果を、9月にポルトガルで開催された国際シンポジウムLogic-Based Program Synthesis and Transformation (LOPSTR 2009)と国内研究集会において発表した。国際シンポジウムで発表した内容はシンポジウムのpost-proceedingsのselected paperとして出版される。
|
