|
ポインタ操作やヒープ領域の確保や開放を含むプログラムに関するプログラム変換を形式的に導出可能な枠組みを、プログラムの段階的詳細化を行うための形式的な枠組であるrefinement calculusの拡張として与えた。この拡張では、従来の古典論理に代えて、ヒープメモリに関する言明を表現可能なseparation logicを用いてプログラムを述語変換子として表した。この手法により、ヒープやポインタに関する操作が、separation logicの論理演算子に対応する基本的な述語変換子の組み合わせに分解できることを明らかにした。これら基本的な述語変換子は、ヒープの確保と開放に対応するものであり、これらを用いて他のポインタ操作を表現できるだけでなく、これらがお互いに打ち消しあう性質を持つことを示した。このような基本的な述語演算子を用いて表されたプログラムに、いくつかの変換規則を繰り返し適用することにより、ヒープやポインタ操作を含むようなプログラムのプログラム変換がその正しさを保障した形で導出可能であることを示した。
この結果を、7月にフランスで開催された国際会議Mathematics of Program Consruction (MPC'08)において発表した。また、勝股審也氏とのプログラム変換に関する共同研究も国際雑誌Journal of Functional Programmingに掲載された。
|
