CVS

center-name

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

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

Web版 トップ頁へ

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

  2. 概要一覧

▼ 話題別に探す
  1. 領域

  2. 形態

  3. 手法

  4. ツール

  5. 実施年度

事例 16: Hoare論理の健全性のAgdaによる検証


実施年度2006
概要 Hoare論理の健全性証明をAgda上で実行した.
担当者 木下佳樹,高橋孝一,田辺良則,湯浅能史
班名 PML
寄与
関連する事例

題材

領域 論理
題材の詳細
Hoare論理
形態 定理の証明
言語 Agda記述言語
規模 約940行
題材の情報源 教科書等.例えば 林晋, プログラム検証論, 情報数学講座8, 共立出版

検証のデータ

目的
Hoare論理の健全性証明がAgda上で実行できることを確認すること.
検証内容
Hoare三つ組み p{c}q が証明可能であり,モデルS1でpが成立し,cによってS1が
S2に遷移すれば,S2でqが成立する.
結果
定理が証明された.
検証手法 対話型検証
モデル化法
使用ツール Agda
スケジュール、
労力、時間など
明確な記録無し.打合せなどを除き,実働は1ヶ月くらい.
備考

情報源

算譜科学研究速報
(テクニカルレポ-ト)
論文発表
口頭発表 第三回システム検証の科学技術シンポジウム「形式的体系の定理証明支援系上で の実現法」
知的財産
その他

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