6L-7
証明支援系を用いたMorrisの2分木走査アルゴリズムの実装の検証
○山田一宏，森口草介，渡部卓雄，西崎真也（東工大）
我々は，Morrisの2分木走査アルゴリズムのCによる実装を対象とし
て，証明支援系を用いた正当性の検証を試みた．本論文はその手法
と結果に関する報告である．Morrisのアルゴリズムは，ポインタの
書き換えを行うことで再帰やスタックを用いずに2分木走査を行う
方法のひとつである．また他のポインタ反転法と異なり節点に印を
付けるためのビットを設ける必要もないのが特徴である．我々は，
入力および走査結果についての仕様を事前・事後条件として与え，
C用の検証支援ツールであるCaduceusによって検証条件を生成した．
ループ不変条件は必要に応じて適宜与えた．生成された検証条件を
自動検証ツールSimplifyおよび証明支援系Coqを用いて証明した．