WEKO3
-
RootNode
アイテム
制約付き項書換え系の潜在帰納法を利用した手続き型プログラム検証の試み
https://ipsj.ixsq.nii.ac.jp/records/16440
https://ipsj.ixsq.nii.ac.jp/records/16440443d4f46-0b7c-4159-aaf1-65f0c062ec57
| 名前 / ファイル | ライセンス | アクション |
|---|---|---|
IPSJ-TPRO0102009.pdf (431.7 kB)
|
Copyright (c) 2008 by the Information Processing Society of Japan
|
|
| オープンアクセス | ||
| Item type | Trans(1) | |||||||
|---|---|---|---|---|---|---|---|---|
| 公開日 | 2008-09-26 | |||||||
| タイトル | ||||||||
| タイトル | 制約付き項書換え系の潜在帰納法を利用した手続き型プログラム検証の試み | |||||||
| タイトル | ||||||||
| 言語 | en | |||||||
| タイトル | Approach to Procedural-program Verification Based on Implicit Induction of Constrained Term Rewriting Systems | |||||||
| 言語 | ||||||||
| 言語 | jpn | |||||||
| キーワード | ||||||||
| 主題Scheme | Other | |||||||
| 主題 | 通常論文 | |||||||
| 資源タイプ | ||||||||
| 資源タイプ識別子 | http://purl.org/coar/resource_type/c_6501 | |||||||
| 資源タイプ | journal article | |||||||
| 著者所属 | ||||||||
| 名古屋大学大学院情報科学研究科 | ||||||||
| 著者所属 | ||||||||
| 名古屋大学大学院情報科学研究科 | ||||||||
| 著者所属 | ||||||||
| 名古屋大学大学院情報科学研究科 | ||||||||
| 著者所属 | ||||||||
| 名古屋大学大学院情報科学研究科 | ||||||||
| 著者所属 | ||||||||
| 名古屋大学大学院情報科学研究科 | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Graduate School of Information Science, Nagoya University | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Graduate School of Information Science, Nagoya University | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Graduate School of Information Science, Nagoya University | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Graduate School of Information Science, Nagoya University | ||||||||
| 著者所属(英) | ||||||||
| en | ||||||||
| Graduate School of Information Science, Nagoya University | ||||||||
| 著者名 |
古市, 祐樹
西田, 直樹
酒井, 正彦
草刈, 圭一朗
坂部, 俊樹
× 古市, 祐樹 西田, 直樹 酒井, 正彦 草刈, 圭一朗 坂部, 俊樹
|
|||||||
| 著者名(英) |
Yuki, Furuichi
Naoki, Nishida
Masahiko, Sakai
Keiichirou, Kusakari
Toshiki, Sakabe
× Yuki, Furuichi Naoki, Nishida Masahiko, Sakai Keiichirou, Kusakari Toshiki, Sakabe
|
|||||||
| 論文抄録 | ||||||||
| 内容記述タイプ | Other | |||||||
| 内容記述 | 手続き型プログラムの検証手法として，モデル検査やホーア論理に基づく検証手法が代表的である．一方，項書換えの分野では帰納的定理の証明手法として潜在帰納法や書換え帰納法などが広く研究されている．本論文では，帰納的定理の証明法を利用して手続き型プログラムの等価性の検証を試みる．具体的には，自然数上のwhile言語で定義された手続き型関数からプレスブルガー文を規則の制約として持つことが許された制約付き項書換え系への変換を与え，その変換により手続き型プログラムの等価性を書換え系の関数の等価性に帰着させ，潜在帰納法を用いて等価性検証を試みる．この手法を実現するために，合流性を保証するための危険対定理および完備化手続きを制約付き書換えに対応するように拡張する． | |||||||
| 論文抄録(英) | ||||||||
| 内容記述タイプ | Other | |||||||
| 内容記述 | In the field of procedural programming, several verification methods based on model checking or Hoare logic have been proposed. On the other hand, in the field of term rewriting, implicit induction and rewriting induction have been widely studied as methods for proving inductive theorems. In this paper, we try to take advantages of methods for proving inductive theorems in verifying procedural functions written in a "while" language with natural number type. More precisely, we propose a transformation from procedural programs to constrained term rewriting systems whose constraints are in Presburger arithmetic, and show that the transformation reduces the equivalence of procedural programs to that of functions in rewrite systems. By verifying the equivalence between rewrite systems, we verify the equivalence between the corresponding procedural functions. To establish this approach, we extend Critical Pair Theorem and the basic completion procedure for constrained systems. | |||||||
| 書誌レコードID | ||||||||
| 収録物識別子タイプ | NCID | |||||||
| 収録物識別子 | AA11464814 | |||||||
| 書誌情報 |
情報処理学会論文誌プログラミング（PRO） 巻 1, 号 2, p. 100-121, 発行日 2008-09-26 |
|||||||
| ISSN | ||||||||
| 収録物識別子タイプ | ISSN | |||||||
| 収録物識別子 | 1882-7802 | |||||||
| 出版者 | ||||||||
| 言語 | ja | |||||||
| 出版者 | 情報処理学会 | |||||||
