プログラム変換を用いたポインタ操作プログラムの検証にむけて：Morrisの二分木走査アルゴリズムによるケーススタディ

摘要

ポインタ書き換えを伴うプログラムのプログラム変換にもとづく検証のケーススタディとして，Morrisの二分木走査アルゴリズムの正当性を扱った．本稿ではその際に用いたプログラム変換手法とその具体的な適用手法について報告する．