著者

山田一宏 森口草介 渡部卓雄 西崎真也

雑誌

第73回全国大会講演論文集

巻号頁・発行日

vol.2011, no.1, pp.505-506, 2011-03-02

---

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