研究課題
例外の発生と例外の補足を許すようなプログラムに関するプログラム変換を形式的に導出可能な枠組みとして、4値論理に基づくrefinement calculusを提案した。Refinement calculusは、プログラムあるいはプログラムの仕様から最終プログラムを段階的な詳細化(プログラム変換)によって導くための洗練された枠組みであるが、古典論理をその基礎としておりプログラムが正常に終了するかどうかの区別しかできない。実際のプログラムでは、実行時エラー(例えばゼロ除算など)によって実行を異常終了させたり、異常終了を補足して正常実行に復帰する仕組みが用意されているが、これらは従来のRefinement Calculusでは扱うことができなかった。今年度の研究では、古典論理に代えてArieliとAvronによる4値論理を用いることによって正常終了と異常終了を区別して扱うことを可能とし、これによって上記のような実行時エラーやエラーからの回復機構をもつプログラムについてプログラムの段階的な詳細化を形式的に導出することが可能となった。この結果を、9月にポルトガルで開催された国際シンポジウムLogic-Based Program Synthesis and Transformation (LOPSTR 2009)と国内研究集会において発表した。国際シンポジウムで発表した内容はシンポジウムのpost-proceedingsのselected paperとして出版される。
すべて 2010 2009
すべて 雑誌論文 (1件) (うち査読あり 1件) 学会発表 (1件)
19th International Symposium, LOPSTR 2009, Revised Selected Papers (Lecture Notes in Computer Science) 6037(掲載決定)
