Fundamental research on software verification based on algebraic method

本研究旨在建立方程式逻辑的验证方法，并将其应用于软体验证，将软体转换成方程式。（1）定义了项集重写系统，将终止方程作为序项重写规则，将非终止方程作为两边都有项集的重写规则. (2)如果相应的E-重写正在终止，则术语集重写系统正在终止。(3)如果所有的临界对都是可连接的，则终止项集重写系统和左线性项集重写系统是合流的。(4)定义了项集重写系统的完备化推理规则。(5)通过构造一个实验系统，研究了术语集重写系统的有效实现。(6)讨论了结合律和交换律的等价项上重写系统的终止性。(7)给出了优先级项重写系统的新语义。

This research is toward establishing verification method in equational logic and applying it software verification by transforming software to equations. The following results were obtained ;(1) The term set rewriting systems are defined by considering terminating equations as ordinal term rewriting rules and non-terminating equations as rewriting rules having sets of terms in both-hand sides.(2) term set rewriting systems is terminating if the corresponding E-rewriting is terminating.(3) Terminating and left-linear term set rewriting systems are confluent, if all critical pairs are joinable.(4) The inference rules for completion on term set rewriting systems are defined.(5) The efficient implementation of term set rewriting systems are investigated by constructing an experimental system.(6) The terminating property of rewriting systems on quotients of associative and commutative laws are discussed.(7) The new semantics of priority term rewriting system was offered.