手続き型プログラムから書換え系への変換に基づくソフトウェア検証の試み (Approach to Software Verification Based on Transformation from Procedural Programs to Rewrite Systems) Export

@article{citeulike:3251461, abstract = {項書換えの分野では帰納的定理の証明手法として潜在帰納法や書換え帰納法などが広く研究されている.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.}, author = {Furuichi, Yuki and Nishida, Naoki and Sakai, Masahiko and Kusakari, Keiichiro and Sakabe, Toshiki}, citeulike-article-id = {3251461}, citeulike-linkout-0 = {http://ci.nii.ac.jp/naid/110004851906/}, citeulike-linkout-1 = {http://www.sakabe.nuie.nagoya-u.ac.jp/~nishida/DB/pdf/furuichi06ss2006-41.pdf}, day = {19}, journal = {電子情報通信学会技術研究報告. KBSE, 知能ソフトウェア工学}, keywords = {rewriting, verification}, month = {October}, number = {326}, pages = {7--12}, posted-at = {2008-09-13 08:15:18}, priority = {0}, publisher = {社団法人電子情報通信学会}, title = {手続き型プログラムから書換え系への変換に基づくソフトウェア検証の試み (Approach to Software Verification Based on Transformation from Procedural Programs to Rewrite Systems)}, url = {http://ci.nii.ac.jp/naid/110004851906/}, volume = {106}, year = {2006} }

TY - JOUR ID - citeulike:3251461 L3 - citeulike-article-id:3251461 N2 - 項書換えの分野では帰納的定理の証明手法として潜在帰納法や書換え帰納法などが広く研究されている.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. IS - 326 JF - 電子情報通信学会技術研究報告. KBSE, 知能ソフトウェア工学 EP - 12 TI - 手続き型プログラムから書換え系への変換に基づくソフトウェア検証の試み (Approach to Software Verification Based on Transformation from Procedural Programs to Rewrite Systems) PB - 社団法人電子情報通信学会 VL - 106 SP - 7 KW - rewriting KW - verification AU - Furuichi, Yuki AU - Nishida, Naoki AU - Sakai, Masahiko AU - Kusakari, Keiichiro AU - Sakabe, Toshiki PY - 2006/10/19/ UR - http://ci.nii.ac.jp/naid/110004851906/ ER -