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

Search this Article

Author(s)

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.

Journal

  • IEICE technical report

    IEICE technical report 106(324), 7-12, 2006-10-19

    The Institute of Electronics, Information and Communication Engineers

References:  14

Codes

  • NII Article ID (NAID)
    110004851223
  • NII NACSIS-CAT ID (NCID)
    AN10013287
  • Text Lang
    JPN
  • Article Type
    ART
  • ISSN
    09135685
  • NDL Article ID
    8539129
  • NDL Source Classification
    ZN33(科学技術--電気工学・電気機械工業--電子工学・電気通信)
  • NDL Call No.
    Z16-940
  • Data Source
    CJP  NDL  NII-ELS 
Page Top