KIDS: a semiautomatic program development system

The Kestrel Interactive Development System (KIDS) provides automated support for the development of correct and efficient programs from formal specifications. 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 we believe that KIDS could be developed to the point that it becomes economical to use for routine programming. To illustrate the use of KIDS, we trace the derivation of an algorithm for enumerating solutions to the k-queens problem. The initial algorithm that KIDS designs takes about sixty minutes on a SUN-4/110 to find all 92 solutions to the 8-queens problem instance. The final optimize...