- Expander is a proof and test environment for algebraic data type
specifications and functional-logic programs.
Program design, test and verification are supported by tailor-made deduction
rules for proving
*Gentzen clauses*, which are the most frequently used formulas for expressing requirements and queries to data types. Inductive proofs are built up from simplification, subsumption, resolution, rewriting and narrowing steps in a natural way that permits interaction on various levels. The overall proof/test procedure works as follows.A conjecture

*conc0 IF prem0*is proved by stepwise constructing the lists*front = [conc0, ..., conc]*and*rear = [prem0, ..., prem]*consisting of goal sets.*front*and*rear*represent a backward proof of*conc0 IF conc*and a forward proof of*prem IF prem0*, respectively. The proof of*conc0 IF prem0*is complete as soon as*prem*subsumes*conc*. Subsumption is a purely syntactical condition on*prem*and*conc*that implies*conc IF prem*. If, in particular,*conc = FALSE*, then*not(conc0)*is valid. Testing*conc0*means deriving solutions of*conc0*. Solutions are identified as the equations in*solved form*among the goals of*conc*.When building up

*front*and*rear*one may interactively modify the underlying specification and add lemmas or induction orderings. The overall goal is to bring*prem*and*conc*``closer together'' so that, eventually,*prem*subsumes*conc*. The construction of*front*and*rear*may be interrupted whereby*conc0 IF conc*and*prem IF prem0*are identified as proved subtheorems and*conc IF prem*is memorized as the remaining subconjecture. The current induction ordering is transmitted to a later proof of the subconjecture. If the underlying specification is*functional*in the sense of Swinging Data Types or*canonical*in the sense of Inductive Theorem Proving for Design Specifications, then a number of additional rules are applicable that often ``speed up'' the proof construction considerably.The core system is written in Standard ML and should be translated by the New Jersey compiler, Version 0.93. After directories

*Specifications, Proofs*and*Graphs*have been created, the ML function call*Install "Specifications" "Proofs" "Graphs" "EXPANDER"*exports the target code to the executable file*EXPANDER*.An X-interface called

**eXpander**is documented here and extended here.Another version runs under NeXTSTEP and can be ordered from Peter Padawitz. This version and its use are described in Expander: A System for Testing and Verifying Functional-Logic Programs

*Contents*: 1 A uniform proof method - 2 Design language - 3 Rules - 4 Commands - 5 Built-in simplifications - 6 Error messages - 7 Sample proofs and tests - 8 Source code (the pure code listing starts on page 40).

Sorry, but Expander is not maintained any longer. Its successor**Expander2**provides much more features.

For more automated reasoning systems, take a look at Digital Math.

Peter Padawitz - Informatik 1
- TU Dortmund
- Germany