Formal Systems Laboratory

Inductive Behavioral Proofs by Unhiding

Abstract. We show that for any behavioral $\backslash Sigma$-specification $~B$ there is an ordinary algebraic specification $\backslash tilde\{B\}$ over a larger signature, such that a model behaviorally satisfies $~B$ iff it satisfies, in the ordinary sense, the $\backslash Sigma$-theorems of $\backslash tilde\{B\}$. The idea is to add machinery for contexts and experiments (sorts, operations and equations), use it, and then hide it. We develop a procedure, called ''unhiding'', which takes a finite $~B$ and produces a finite $\backslash tilde\{B\}$. The practical aspect of this procedure is that one can use any standard equational inductive theorem prover to derive behavioral theorems, even if neither equational reasoning nor induction is sound for behavioral satisfaction.