Fundamental research on software verification based on algebraic method

点击翻译按钮获取中文摘要

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.