A logic database for software release engineering

Any attempt to automate software configuration management (SCM) should employ data representations and computational models which are powerful enough to handle abstraction, specialization, combinatorial variance, and genericity. The authors describe a working database and query engine based on first-order logic, with an extended data domain accommodating large items (such as source or object files) as pure values and an extended predicate domain accommodating external utilities (such as compilers) as pure functions. It is shown that several well-understood logic programming techniques (theorem proving, partial evaluation, abstract interpretation, and lemma reuse) provide a sound theoretical and practical basis for mechanized software building. A high-level computational mechanism (theorem proving in first-order logic) has been found which elegantly, if unexpectedly, supports software release engineering. The user interface is essentially declarative: to build a release, the user asks a question to which the desired product is an answer