Proving behavioral equivalence for weakly complete behavioral specifications by implicit induction

摘要

The behavioral completion system proposed by Kano et. al 8 provides the basis of the Knuth-Bendix algorithm for proving behavioral equational theorems of strongly complete behavioral specifications as does the inductive completion system 5 for inductive equational theorems. In this paper, we improve the behavioral completion system so that it can apply to weakly complete behavioral specifications. We prove that given an equation and a weakly complete behavioral specification, if the Knuth-Bendix algorithm stops successfully then the equation is a behavioral theorem of the specification.