KIDS: a semiautomatic program development system

The Kestrel Interactive Development System (KIDS), which provides automated support for the development of correct and efficient programs from formal specifications, is described. The system has components for performing algorithm design, deductive inference, program simplification, partial evaluation, finite differencing optimizations, data type refinement, compilation, and other development operations. Although their application is interactive, all of the KIDS operations are automatic except the algorithm design tactics, which require some interaction at present. Dozens of programs have been derived using the system, and it is believed that KIDS could be developed to the point where it becomes economical to use for routine programming. To illustrate the use of KIDS, the author traces the derivation of an algorithm for enumerating solutions to the k-queens problem. The initial algorithm that KIDS designed takes about 60 minutes on a SUN-4/110 to find all 92 solutions to the 8-queens problem instance. The final optimized version finds the same solutions in under one second