CVS

center-name

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

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

Web版 トップ頁へ

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

  2. 概要一覧

▼ 話題別に探す
  1. 領域

  2. 形態

  3. 手法

  4. ツール

  5. 実施年度

事例 13: たし算かけ算プログラムのコンパイラの正当性証明


実施年度2005
概要 整数上の加法と乗法演算のプログラムをスタック操作列へ変換するコンパイラの 正当性をAgda上で検証した.事例自体は対話型証明検証コース初級編の 総合演習とした.
担当者 永山操,西原秀明,武山誠
班名 研修コース班
寄与
関連する事例

題材

領域 プログラム,アルゴリズム,コンパイラ
題材の詳細
整数上の加法と乗法演算プログラムからスタック操作列へ変換するコンパイラ
形態 ソースコード
言語 Agda
規模 150行程度
題材の情報源 対話型証明研修コース(4日目)のスライド

検証のデータ

目的
対話型証明支援系Agdaを利用した検証の事例開発
検証内容
コンパイラの正当性
プログラムを直接評価した値とコンパイル後のスタック操作列を実行して得られ
る値が等しい.
結果
正当性の証明ができた.
検証手法 対話型検証
モデル化法 直接手で Agda プログラムを書いた.手動
使用ツール Agda
スケジュール、
労力、時間など
数時間,演習は1日分
備考

情報源

算譜科学研究速報
(テクニカルレポ-ト)
論文発表
口頭発表
知的財産
その他

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