CVS

center-name

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

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

Web版 トップ頁へ

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

  2. 概要一覧

▼ 話題別に探す
  1. 領域

  2. 形態

  3. 手法

  4. ツール

  5. 実施年度

事例 12: 相互再帰的に定義された文字列を翻訳処理するプログラムの検証


実施年度2003
概要 K&Rの教科書第5章の型宣言の文字列を翻訳するプログラムを定理証明支援系PVS 上で形式化し、プログラムが正しく動くことを証明した。
担当者 高木理、武山誠、渡邊宏
班名
寄与 文科省科振費
関連する事例

題材

領域 アルゴリズム、プログラム、
題材の詳細
Kernighan, B.W. and Ritchie, D.M., The C programming Language 2nd
Edition, Prentice Hall PTR,(邦訳: 石田晴久訳,プログラミング言語C ANSI規
格準拠, 共立出版)の第5章に紹介されているCの型宣言の文字列をテキスト表示
向け文字列へ変換するプログラム。文字列を入力し文字列を出力する。
形態 ソースコード、C言語で書かれたアルゴリズム
言語 C言語
規模 70行程度
題材の情報源 Kernighan, B.W. and Ritchie, D.M., The C programming Language 2nd Edition, Prentice Hall PTR,(邦訳: 石田晴久訳,プログラミング言語C ANSI規 格準拠, 共立出版)の第5章

検証のデータ

目的
形式化、定理証明の事例作成のため。
検証内容
アルゴリズムが正しく動作することで、簡略して書くと次の三つ。
(I) 入力データ(文字列)を読み取りながらプログラム実行させている途中、入
力ポインタが正しい位置を指している。
(II) 正しい入力データが入力されたとき,その値に対応する翻訳文(ある抽象
データ型の値)を返す。
(III) 正しくない入力データが入力されたときはエラー文を返す。

結果
入出力データ、プログラムを抽象化し、三つの検証項目をPVS上で形式化した。
さらに,(I)および(II)に相当する部分までをPVS上で証明し、
(III)については部分的な証明を行った。
(論文に掲載されている検証項目の形式化と証明は(II)に相当する部分まで。)

検証手法 定理証明、抽象化
モデル化法 手動、手動で抽象化
使用ツール PVS
スケジュール、
労力、時間など
一ヶ月程度
備考

情報源

算譜科学研究速報
(テクニカルレポ-ト)
PS-2005-009, PVSの紹介, 高木理、渡邊宏、武山誠, http://unit.aist.go.jp/cvs/tr-data/ps05-009.pdf
論文発表 高木理、渡邊宏、武山誠 対話型証明支援ツールPVSの紹介 コンピュータソフトウェア, Vol.22, No.3(2005), pp.37-57
口頭発表
知的財産
その他

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