A semi-algorithm for algebraic implementation proofs (Q1199928)

Formal implementation concepts are a necessary prerequisite for proving the correct of software development steps. In order to be useful in practice formal implementation notions should be supplied by appropriate proof methods. We present a recursive semi-algorithm for proving implementations based on behavioural semantics of algebraic specifications. The underlying idea of behavioural semantics is that an implementation is correct if it satisfies the desired input/output behaviour while it may abstract from the non observable properties of a given specification. For the formalization of this intuitive idea the sorts of a specification are divided into observable and non observable sorts. Then behavioural implementations can be characterized by the following proof theoretic condition on the set of observable contexts: A specification \(SP1\) is a behavioural implementation of a specification \(SP\) if and only if for all observable contexts \(c\) and for all axioms \(t=r\) of \(SP\) the ``observable'' equations \(c[t]=c[r]\) are deducible from the axioms of the implementation \(SP1\) (for all ground instantiations over the signature of \(SP\)). Thereby an observable context is any term \(c\) over the signature of \(SP\) of observable sort containing a distinguished variable \(z_ s\) (of some sort \(s\)) and the context application \(c[t]\) (\(c[r]\) resp.) is defined by replacing the variable \(z_ s\) by the term \(t\) (\(r\) resp.) if \(t\) and \(r\) are of sort \(s\). For instance, a behavioural implementation of a specification of finite sets where only the results of membership tests \(x\in S\) are observable not necessarily has to satisfy the characteristic set equations \(add(x,add(y,S))=add(y,add(x,S))\) and \(add(x,add(x,S))=add(x,S)\) but it has to satisfy all applications of observable contexts to these equations as e.g. \(n\in add(x,add(y,S))=n\in add(y,add(x,S))\), \(n\in add(m,add(x,add(y,S)))=n\in add(m,add(y,add(x,S)))\), etc. The basic idea of the semi-algorithm is to provide a proof procedure which allows to verify the above implementation condition by context induction, i.e. by induction on the structure of the observable contexts. In the first step (which corresponds to the base of the induction where trivial observable contexts are considered) it has to be shown that all ground instantiations of the ``observable'' axioms \(t=r\) of \(SP\) (i.e. \(t\) and \(r\) are of observable sort) are deducible from the axioms of \(SP1\). In the second step of the algorithm the induction step is performed for all contexts of the form \(f(\dots,c,\dots)\) where \(f\) is a function symbol of \(SP\) with observable result sort and \(c\) ranges over all contexts over \(SP\) of sort, say \(s_ i\). (Here the dots stand for arbitrary ground terms over the signature of \(SP\) with sorts according to the functionality of \(f\).) For the proof of the actual induction assertion it has to be shown that for all contexts \(c\) of sort \(s_ i\) and for all axioms \(t=r\) of \(SP\) (with appropriate sort), the equation \((f\dots,c[t],\dots)=f(\dots,c[r],\dots)\) is deducible from the axioms of the implementation \(SP1\) (for all ground instantiations). If the sort \(s_ i\) is observable then the induction step is trivial using the induction hypothesis and the congruence rule of the equational calculus. If the induction hypothesis cannot be applied for \(c\) (because the sort \(s_ i\) of \(c\) is not an observable sort) a nested context induction over all contexts \(c\) of sort \(s_ i\) is performed for proving the actual induction assertion. Each nesting of context induction is implemented by a recursive call of the semi-algorithm. Hence the algorithm obtains, besides the ``input'' specifications \(SP\) and \(SP1\), as an additional parameter a context which represents the actual assertion to be proved (For instance, in the first recursive call this is just the context \(f(\dots,z_{s_ i},\dots)\) with a distinguished variable \(z_{s_ i}\) of sort \(s_ i\).) In order to achieve successful termination of the algorithm it is often necessary (as usual when dealing with induction proofs) to find an appropriate generalization of the actual induction assertion. Therefore automated reasoning has to be supplemented by interaction with the user who may select before each recursive call a context which represents a generalization of the actual induction assertion. Moreover, in order to allow the use of overall induction hypotheses in any depth of recursion each call of the algorithm obtains as a further input a set \(C\) of contexts where each context of \(C\) represents a higher-level induction hypothesis. Then, if all steps of the algorithm are performed and the algorithm terminates, the principle of context induction implies that \(SP1\) is a behavioural implementation of \(SP\). The described semi- algorithm is the kernel of the ISAR system [cf. \textit{B. Bauer} and \textit{R. Hennicker}, Lect. Notes in Artif. Intell. 624, 451-453 (1992)] which provides an environment for interactive proofs of algebraic implementations.