Incorporating Decision Procedures in Implicit Induction
Résumé
As many proof obligations in system verification require complex interleaving of pure logic and domain-specific steps, a crucial activity in the construction of a successful verification tool is the effective incorporation of reasoning specialists (such as decision procedures or unification algorithms) within more general inference modules (such as rewrite engines or inference procedures for reasoning by induction). Mathematical induction is a fundamental reasoning technique for system verification. In the last decades it has been thoroughly investigated and several powerful techniques and heuristics for reasoning about inductively defined objects have been put forward \cite{bm79,KNZ91:jsc,JAR::BouhoulaR1995}. These techniques allow the automatic discharge of many non trivial proof-obligations. Yet---when applied to verification problems of practical significance---the level of automation provided by such techniques is still unsatisfactory. The seminal work by Boyer and Moore \cite{bm88} showed that a higher level of automation can be achieved by induction provers thanks to the incorporation of decision procedures. However in Boyer and Moore's approach the interplay of the decision procedure is limited to the simplification engine and therefore it does not exploit the potentials of the cooperation between the decision procedure and the induction heuristics which are best illustrated by means of the following example. Let us consider the following proof-obligation occurring in the verification proof of the MJRTY algorithm \cite{bm91} given in \cite{str98b,str00b}: \begin{align} \label{eq:6} a\neq mc(p,i)\Rightarrow 2*(ml(p,i)+count(p,i,a)) < s(i+ml(p,i)) \end{align} Application of the cover set leads to the following sub-goal which is obtained by first applying the substitution $\sigma=\{i\mapsto s(i'),a\mapsto Noname\}$ to (\ref{eq:6}) and then by normalizing the result with the available (conditional) rewrite rules: \begin{equation} \label{eq:8} \begin{split} \textit{Noname} \neq mc(p,i'),access(p,i') \neq mc(p,i'),0 < ml(p,i'), \textit{Noname} = access(p,i') \Rightarrow \\ 2*((ml(p,i')-1)+s(count(p,i',\textit{Noname}))) < s(s(i')+(ml(p,i')-1)) \end{split} \end{equation} (\ref{eq:8}) is not an instance of (\ref{eq:6}) (which now plays the role of the induction hypothesis), nor it can be directly solved by arithmetic reasoning only. However (\ref{eq:8}) follows by simple arithmetic reasoning from the instance of (\ref{eq:6}) obtained by applying the substitution $\{a\mapsto\textit{Noname},i \mapsto i'\}$. This example suggests a general approach to the integration of a decision procedure with the activity of selecting the induction hypothesis: \emph{(i)} normalize the induction conclusion with the available rewrite rules and \emph{(ii)} select an appropriate instance of the induction hypothesis which is likely to entail the normalized conclusion. In this paper we present an extension to Boyer and Moore's integration schema that enables the decision procedure to use suitably selected instances of the induction hypotheses.\footnote{An alternative approach to the incorporation of reasoning specialists in induction provers is presented in \cite{JAR::KapurS1996}. There the reasoning specialist is used to incorporate semantic information into the process of selection of the induction schemas. The proposed solution enables the use of induction hypotheses which otherwise could not be applied thereby leading to an increased automation. The approach is complementary to that described in this paper.} The induction proof method we consider is based on cover set induction \cite{red90} and is implemented in the SPIKE prover \cite{spike}.\footnote{Cover set induction combines the advantages of explicit induction with those of proof by consistency.} The interplay with the decision procedure is obtained by extending and incorporating into the induction proof method Constraint Contextual Rewriting. \emph{Constraint Contextual Rewriting} \cite{ftp98}, CCR(X) for short, is an abstract integration schema between rewriting and decision procedures inspired by Boyer and Moore's ideas. Similarly to Boyer and Moore's approach, CCR(X) empowers conditional rewriting with the services provided by the available decision procedure, X, and the decision procedure with additional facts derived from the available lemmas.\footnote{This capability, called \emph{augmentation} by Boyer and Moore, is crucial to the effectiveness of the integration schema. See \cite{bm88} for the details.} Unlike Boyer and Moore's simplifier, CCR(X) is independent from the theory decided by the decision procedure, is formally and concisely presented by means of a calculus \cite{ftp98}, and is guaranteed to terminate \cite{frocos2000}. This contrasts with the 40 page long description available in \cite{bm88} in which high level design decisions are intermixed with optimization details. The extension of CCR(X) considered in this paper, \emph{Inductive Constraint Contextual Rewriting} or ICCR(X) for short, differs from CCR(X) in that the decision procedure is allowed to use suitably selected instances of the induction hypotheses. The main contribution of our work is twofold: \begin{itemize} \item SPIKE benefits of the flexibility and generality of CCR(X) as an off-the-shelf integration schema of decision procedures in formula simplification. To emphasize this, we call the resulting calculus SPIKE(X) where X is an abstract decision procedure. X can be instantiated in different ways. We have considered an instantiation for X, called LA+EQ, resulting from the combination of the quantifier-free Linear Arithmetics (LA) and the quantifier-free theory of equality (EQ), but the scheme can be applied to many other theories as well. \item ICCR(X) is a simple but nevertheless significant extension to CCR(X) for induction through the use of induction hypotheses. \end{itemize} Computer experiments carried out with SPIKE(LA+EQ) on non-trivial verification problems have shown the effectiveness of our approach. The proof of MJRTY does not need user-defined tactics as it is the case with PVS and Nuprl. Also in the proof of the ABR conformance algorithm \cite{rsk00}\nocite{bbr96} many of the about 80 user-defined lemmas require specific tactics with PVS but more than half of them are relieved automatically with SPIKE(LA+EQ). A formal presentation and proofs of soundness of ICCR(X), SPIKE(X), and of the compound decision procedure LA+EQ are not given here for the lack of space. They will be given in the final version of the paper.