| 講演名 | 2006-10-26 手続き型プログラムから書換え系への変換に基づくソフトウェア検証の試み 古市 祐樹, 西田 直樹, 酒井 正彦, 草刈 圭一朗, 坂部 俊樹, |
|---|---|
| PDFダウンロードページ |  PDFダウンロードページへ |
| 抄録(和) | 項書換えの分野では帰納的定理の証明手法として潜在帰納法や書換え帰納法などが広く研究されている.2つの異なる関数が任意の入力に対して同様の出力を返すことは帰納的定理として捉えられるので,帰納的定理の証明法は関数型プログラムの等価性の検証に利用できる.本研究では,項書換えにおける帰納的定理の証明法を利用して手続き型プログラムの等価性の検証を試みる.具体的には,手続き型プログラムから書換え系への変換を与え,その変換により手続き型プログラムの等価性を項書換え系の関数の等価性に帰着できることを示す. |
| 抄録(英) | In the field of term rewriting, inductionless induction and rewriting induction have been widely studied as methods for proving inductive theorems. Since equivalence of functions (that is, the output values are the same for the same input) can be represented as an inductive theorem, methods for proving inductive theorems are useful to verify the equivalence of functions in functional programming. In this paper, we try to take advantage of methods for proving inductive theorems in verifying procedural programs written in a subset of the C language with integer type. More precisely, we propose a transformation from procedural programs to rewrite systems and show that the transformation reduces the equivalence of procedural programs to that of functions in rewrite systems. |
| キーワード(和) | 項書換え系 / 帰納的定理 / 潜在帰納法 / プレスブルガー文 / 完備化 / プログラム変換 |
| キーワード(英) | term rewriting system / inductive theorem / inductionless induction / Presburuger arithmetic / completion / program transformation |
| 資料番号 | SS2006-41,KBSE2006-17 |
| 発行日 |
| 研究会情報 | |
| 研究会 | KBSE |
|---|---|
| 開催期間 | 2006/10/19(から1日開催) |
| 開催地（和） | |
| 開催地（英） | |
| テーマ（和） | |
| テーマ（英） | |
| 委員長氏名（和） | |
| 委員長氏名（英） | |
| 副委員長氏名（和） | |
| 副委員長氏名（英） | |
| 幹事氏名（和） | |
| 幹事氏名（英） | |
| 幹事補佐氏名（和） | |
| 幹事補佐氏名（英） | |
| 講演論文情報詳細 | |
| 申込み研究会 | Knowledge-Based Software Engineering (KBSE) |
|---|---|
| 本文の言語 | JPN |
| タイトル（和） | 手続き型プログラムから書換え系への変換に基づくソフトウェア検証の試み |
| サブタイトル（和） | |
| タイトル（英） | Approach to Software Verification Based on Transformation from Procedural Programs to Rewrite Systems |
| サブタイトル（和） | |
| キーワード(1)（和/英） | 項書換え系 / term rewriting system |
| キーワード(2)（和/英） | 帰納的定理 / inductive theorem |
| キーワード(3)（和/英） | 潜在帰納法 / inductionless induction |
| キーワード(4)（和/英） | プレスブルガー文 / Presburuger arithmetic |
| キーワード(5)（和/英） | 完備化 / completion |
| キーワード(6)（和/英） | プログラム変換 / program transformation |
| 第 1 著者 氏名（和/英） | 古市 祐樹 / Yuki FURUICHI |
| 第 1 著者 所属（和/英） | 名古屋大学大学院情報科学研究科 Graduate School of Information Science, Nagoya University |
| 第 2 著者 氏名（和/英） | 西田 直樹 / Naoki NISHIDA |
| 第 2 著者 所属（和/英） | 名古屋大学大学院情報科学研究科 Graduate School of Information Science, Nagoya University |
| 第 3 著者 氏名（和/英） | 酒井 正彦 / Masahiko SAKAI |
| 第 3 著者 所属（和/英） | 名古屋大学大学院情報科学研究科 Graduate School of Information Science, Nagoya University |
| 第 4 著者 氏名（和/英） | 草刈 圭一朗 / Keiichiro KUSAKARI |
| 第 4 著者 所属（和/英） | 名古屋大学大学院情報科学研究科 Graduate School of Information Science, Nagoya University |
| 第 5 著者 氏名（和/英） | 坂部 俊樹 / Toshiki SAKABE |
| 第 5 著者 所属（和/英） | 名古屋大学大学院情報科学研究科 Graduate School of Information Science, Nagoya University |
| 発表年月日 | 2006-10-26 |
| 資料番号 | SS2006-41,KBSE2006-17 |
| 巻番号（vol） | vol.106 |
| 号番号（no） | 326 |
| ページ範囲 | pp.- |
| ページ数 | 6 |
| 発行日 | |