KIDS (Kestrel Interactive Development System) Project

People: Dr Douglas R. Smith, Dr Stephen Westfold, Limei Gilham, and Thomas Pressburger.

Objective:

The Kestrel Interactive Development System (KIDS, active from 1987 through 2001) 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. Dozens of programs have been derived using the system.

KIDS has been used to develop many applications in such diverse areas as scheduling, combinatorial design, sorting and searching, computational geometry, pattern matching, and mathematical programming. KIDS was applied to build transportation schedulers for use in military settings. Because they incorporate scheduling constraints directly into code, these schedulers run orders of magnitude faster than manually written codes of comparable functionality. Examples include the ITAS in-theater airlift scheduler for the Pacific Air Force at Hickham AFB (developed jointly with BBN), the CAMPS mission planning system for the Air Mobility Command at Scott AFB (developed with BBN and CMU), and several others.

The most unique aspect of KIDS is its approach to algorithm design. Abstract algorithmic concepts, such as divide-and-conquer and global search, are expressed formally as parameterized first-order theories. To apply an algorithmic concept A to a particular problem P, KIDS has a specialized tactic for constructing a theory morphism from the theory of A to the theory of P. It emerges that the hard work in algorithm design is constructing theory morphisms using constructive inference support.