Automated Proving of the Behavioral Attributes

Behavioral equivalence is indistinguishably under experiments: two elements are behavioral equivalent iff each experiment returns the same value for the two elements. Behavioral equivalence can be proved by coinduction. CIRC is a theorem prover which implements circular coinduction, an efficient coinductive technique. Equational attributes refer properties like associativity, commutativity, unity, etc. If these attributes are behaviorally satisfied, then we refer them as behavioral attributes. Two problems regarding these properties are important: expressing the commutativity as a rewrite rule leads to non-termination and their use as attributes requires a careful handling in the proving process. In this paper we present how these attributes are automatically checked in CIRC and we prove that this extension is sound.