KIDS
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
Keywords for this software
References in zbMATH (referenced in 10 articles )
Showing results 1 to 10 of 10.
Sorted by year (- Delaware, Benjamin; Pit-Claudel, Clément; Gross, Jason; Chlipala, Adam: Fiat: deductive synthesis of abstract data types in a proof assistant (2015)
- Visser, Eelco: A survey of strategies in rule-based program transformation systems (2005)
- Buchberger, Bruno; Crăciun, Adrian: Algorithm synthesis by lazy thinking: using problem schemes (2004)
- Visser, Eelco: A survey of rewriting strategies in program transformation systems (2001)
- Anderson, Penny; Basin, David: Program development schemata as derived rules (2000)
- Flener, Pierre; Lau, Kung-Kiu; Ornaghi, Mario; Richardson, Julian: An abstract formalization of correct schemas for program synthesis (2000)
- Veloso, Paulo A. S.; Veloso, Sheila R. M.: On methods for safe introduction of operations (1997)
- Srinivas, Yellamraju V.: A sheaf-theoretic approach to pattern matching and related problems (1993)
- Erbas, Cengiz; Tanik, Murat M.; Aliyazicioglu, Zekeriya: Linear congruence equations for the solutions of the (N)-queens problem (1992)
- Smith, D. R.: KIDS: A Semiautomatic Program Development System (1990) ioport