Foundations for a tool for the automatic adaptation of software components based on semantic specifications

We lay the foundations for a tool for the automatic adaptation of software components in call-by-value functional languages like Standard ML. Such a tool automatically generates simple adaptation functors that overcome minor incompatibilities between different but closely related signatures. The adaptation functors can be expressed in a typed λ-calculus with product types, ML-polymorphism and first-order type functions, but without recursion.; Component adaptation is based on semantic specification formulas. As it seems appropriate for functional programming languages, the semantic specifications are not pre-post-condition formulas. Instead, they are predicate logic formulas that treat functions in the same way as other values. For example, universal quantification over functions is allowed. Moreover, specification formulas pairs and projections. Specification formulas are similar, in style, to axioms in the wide spectrum language Extended ML (EML), but more restricted in order to facilitate automatic component adaptation. We study the semantics of specification formulas by interpreting them in a small call-by-value functional language. Predicates denote sets of closed expressions that are closed under observational equality.; A large part of the work consists of a high level description of methods for component adaptation. These methods come from the fields of automated theorem proving and typed λ-calculus, but substantial modifications are necessary for our purposes. Soundness proofs are provided for all of the methods and some completeness results are proved or conjectured. The investigation of the methods has three parts: Firstly, we study a classical logic sequent calculus whose term language is a recursion-free typed λ-calculus. Secondly, we study algorithms to decide subsets of observational equality for this term language. These include an algorithm that provides a better approximation of observational equality than β_υπ _υ-equality by allowing certain β-reductions that are not β _υ-reductions, and an algorithm for deciding an extension of β _υπ_υ-equality by value-restricted extensionality rules. Thirdly, we study βπ-unification for the term language. Extensions of known higher order unification procedures are necessary because our language has polymorphic existential variables and first order type functions. Moreover, unlike in most versions of higher order unification, we don't assume extensionality rules, because, unless value restrictions are imposed, they are unsound in a call-by-value language.