3 0 0 0 OA 証明支援系を用いたMorrisの2分木走査アルゴリズムの実装の検証
- 著者
- 山田一宏 森口草介 渡部卓雄 西崎真也
- 雑誌
- 第73回全国大会講演論文集
- 巻号頁・発行日
- vol.2011, no.1, pp.505-506, 2011-03-02
我々は,Morrisの2分木走査アルゴリズムのCによる実装を対象として,証明支援系を用いた正当性の検証を試みた.本論文はその手法と結果に関する報告である.Morrisのアルゴリズムは,ポインタの書き換えを行うことで再帰やスタックを用いずに2分木走査を行う方法のひとつである.また他のポインタ反転法と異なり節点に印を付けるためのビットを設ける必要もないのが特徴である.我々は,入力および走査結果についての仕様を事前・事後条件として与え,C用の検証支援ツールであるCaduceusによって検証条件を生成した.ループ不変条件は必要に応じて適宜与えた.生成された検証条件を自動検証ツールSimplifyおよび証明支援系Coqを用いて証明した.
2 0 0 0 部分継続にもとづく移動コード記述: 定義と操作的意味
- 著者
- 渡部卓雄
- 出版者
- 一般社団法人情報処理学会
- 雑誌
- 情報処理学会研究報告
- 巻号頁・発行日
- pp.61-66, 1997
- 被引用文献数
- 1
分散・移動計算機環境における, 移動可能プログラムを記述するための一般的な言語機構を提案する. 基本的なアイデアは, 計算状態の一部を表現する部分接続(partial continuation)をプログラム中で一級オブジェクトとして明示的に扱うことにある. 並行計算系における継続(continuation)の扱いは一般に繁雑になるが, エクステントを限定した部分継続を得る言語機能を用いることにより, 遠隔コード実行の様々なパターンを記述できる. 本機構は手続きクロージャ, あるいはそれと等価な機構を持つ様々な逐次言語に導入可能であり, ユーザ向けのモバイルエージェント記述スクリプト言語だけでなく, システムプログラム記述言語にも適用可能である. 本稿では操作的意味について延べる.