Automating the design of algorithms

Abstract

This paper has two roughly independent parts. The first is devoted to the automation of program construction. The Kestrel Interactive Development System (KIDS) provides knowledge-based support for the derivation of correct and efficient programs from specifications. We trace the use of KIDS in deriving a scheduling algorithm. The derivation illustrates algorithm design, deductive inference, simplification, finite differencing, partial evaluation, data type refinement, and other techniques. 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 KIDS environment. The second part discusses the theory of algorithm design used in KIDS. Concepts include problem theories, algorithm theories, program schemes as parameterized theories, design as interpretation between theories (theory morphisms), algorithm design tactics, and refinement hierarchies of algorithm theories and the incremental construction of algorithms.