Towards complete reasoning about axiomatic specifications

Abstract. To support verification of expressive properties of functional programs, we consider algebraic style specifications that may relate mul-tiple user-defined functions, and compare multiple invocations of a func-tion for different arguments. We present decision procedures for reason-ing about such universally quantified properties of functional programs, using local theory extension methodology. We establish new classes of universally quantified formulas whose satisfiability can be checked in a complete way by finite quantifier instantiation. These classes include single-invocation axioms that generalize standard function contracts, but also certain many-invocation axioms, specifying that functions satisfy congruence, injectivity, or monotonicity with respect to abstraction func-tions, as well as conjunctions of some of these properties. These many-invocation axioms can specify correctness of abstract data type imple-mentations as well as certain information-flow properties. We also present a decidability-preserving construction that enables the same function to be specified using different classes of decidable specifications on different partitions of its domain.