CVS

center-name

AIST
 センター長挨拶Policy Statement研究テーマ研究活動研究成果Technical Reports書籍共同研究集会支援English
 研修コースニュースレター ・CVS Staff ・アクセス 採用情報  ・お問い合わせ ・更新履歴 ・プレスリリース ・カレンダーHOME 

◆ サブ メニュー ◆
Web版 システム検証の事例報告集

Web版 トップ頁へ

▼ 一覧から探す
  1. 項目一覧

  2. 概要一覧

▼ 話題別に探す
  1. 領域

  2. 形態

  3. 手法

  4. ツール

  5. 実施年度

事例 19: リスト反転アルゴリズムのAgda-MLAT連携による検証


実施年度2006
概要 AgdaとMLAT ver.1の連携によりリスト反転アルゴリズムを検証した。
担当者 湯浅 能史, 武山 誠, 関澤 俊弦, 田辺 良則, 高橋 孝一
班名 抽象化ツール研究開発班、対話型検証班
寄与
関連する事例 事例 17:Deutsch-Schorr-WaiteマーキングアルゴリズムのAgda-MLAT連携による検証

題材

領域 ポインタ操作アルゴリズム(手続き型)
題材の詳細
リスト反転アルゴリズム
形態 アルゴリズム, 疑似コード
言語 PML, PML on Agda
規模 10行程度
題材の情報源 特になし

検証のデータ

目的
Agda-MLAT連携のテスト
検証内容
プログラム実行後に:
1. リスト構造が維持される
2. 要素の脱落がない
3. 新しい要素が加わらない
4. 隣り合った要素の順番が逆転する
の4項目を示した。
結果
成功。しかしMLATの性能上、この例題が限界に近いことがあきらかになる。
より大きな(または複雑な)アルゴリズムを検証するためには, MLAT、特に
充足可能性判定器の改良が必要との認識にいたった。(参考 ->
Deutsch-Schorr-WaiteマーキングアルゴリズムのAgda-MLAT連携による検証)
検証手法 演繹手法と自動証明の組み合わせ。対話型検証とモデル検査。
モデル化法 なし
使用ツール Agda, MLAT
スケジュール、
労力、時間など


備考

情報源

算譜科学研究速報
(テクニカルレポ-ト)
論文発表
口頭発表 日本ソフトウェア科学会第23回大会(2006.9.14) 第三回 システム検証の科学技術シンポジウム (2006.10.30)
知的財産
その他 日本ソフトウェア科学会第23回大会予稿集

産総研ホーム >  組織 >  研究センター >  システム検証研究センター
Copyrights (C) 2005-2010 AIST Research Center for Verification and Semantics, All Rights Reserved.