A System for Testing and Verifying Functional-Logic
ProgramsA System for Testing and Verifying Functional-Logic
ProgramsA 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).