KIDS: A Semiautomatic Program Development System
September 1990 (vol. 16 no. 9)
pp. 1024-1043
DOI Bookmark:
http://doi.ieeecomputersociety.org/10.1109/32.58788
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. [1] L. Abraido-Fandino, "An overview of REFINETM2.0." inProc. Second Int. Symp. Knowledge Engineering, Madrid, Spain, Apr. 8-10, 1987.[2] R. Balzer, T. E. Cheatham, and C. Green, "Software technology in the 1990's: Using a new paradigm,"Computer, vol. 16, no. 11, pp. 39-45, Nov. 1983.[3] R. Balzer, T. E. Cheatham, and C. Green, "Transformational implementation: An example,"IEEE Trans. Software Eng., vol. SE-7, no. 1, pp. 3-14, 1981.[4] D. Barstow, "Automatic programming for streams II: Transformational implementation," inProc. 10th Int. Conf. Software Engineering, Singapore, 1988, pp. 439-447.[5] D. Barstow,Knowledge-Based Program Construction. New York: North-Holland, 1979.[6] D. Bjørner, A. P. Ershov, and N. D. Jones, Eds.,Partial Evaluation and Mixed Computation. Amsterdam, The Netherlands: North-Holland, 1988.[7] L. Blaine, A. Goldberg, T. Pressburger, X. Qian, T. Roberts, and S. Westfold, "Progress on the KBSA performance estimation assistant," Kestrel Inst., Tech. Rep. KES.U.88.11, May 1988.[8] P. Borras.,et al., "CENTAUR: The system," inProc. ACM SIGSOFT/SIGPLAN Software Engineering Symp. Practical Software Development Environments, ACM, Boston, MA, November 1988, pp. 14-24; alsoACM SIGPLAN Notices, vol. 24, no. 2, Nov. 1988.[9] M. Broy and M. Wirsing, "Program development: From enumeration to backtracking,"Inform. Processing Lett., vol. 10, no. 4, pp. 193- 197, July 1980.[10] R. M. Burstall and J. Darlington, "A transformation system for developing recursive programs,"J. ACM, vol. 24, no. 1, pp. 44-67, Jan. 1977.[11] R. L. Constable,Implementing Mathematics with the NuPrl Proof Development System. Englewood Cliffs, NJ: Prentice-Hall, 1986.[12] O. J. Dahl, E. W. Dijkstra, and C. A. R. Hoare,Structured Programming. London: Academic, 1972.[13] J. D. Darlingtonet al., "A functional programming environment supporting execution, partial execution and transformation," inPARLE 89: Parallel Architectures&Languages Europe, Vol. 1: Parallel Architectures(Lecture Notes in Computer Science, Vol. 365), E. Odijk, M. Rem, and J. Syre, Eds. New York: Springer-Verlag, 1989, pp. 286-305.[14] M. Feather, "A system for transformationally deriving programs,"ACM Trans. Program. Lang. Syst., vol. 4, no. 1, pp. 1-21, Jan. 1982.[15] S. F. Fickas, "Automating the transformational development of software,"IEEE Trans. Software Eng., vol. SE-11, no. 11, pp. 1268- 1278, Nov. 1985.[16] J. A. Goguen and T. Winkler, "Introducing OBJ3," SRI International, Menlo Park, CA, Tech. Rep. SIR-CSL-88-9, 1988.[17] A. Goldberg, "Reusing software developments," Kestrel Inst., Tech. Rep., July 1989; also presented at the KBSA Workshop, Rome Air Development Center, Utica, NY, Aug. 1989.[18] M. J. Gordon, A. J. Milner, and C. P. Wadsworth,Edinburgh LCF: A Mechanised Logic of Computation(Lecture Notes in Computer Science, vol. 78). Berlin: Springer-Verlag, 1979.[19] J. V. Guttag and J. J. Horning, "Report on the Larch shared language,"Sci. Comput. Program., vol. 6, no. 2, pp. 103-157, 1986.[20] P. Lee, F. Pfenning, G. Rollins, and D. Scott, "The ERGO support system: An integrated set of tools for prototyping integrated environments," inProc. ACM SIGSOFT/SIGPLAN Software Engineering Symp. Practical Software Development Environments. Nov. 1988, pp. 25-34.[21] M. R. Lowry, "Algorithm synthesis through problem reformulation," Ph.D. dissertation, Dep. Comput. Sci., Stanford Univ., 1989.[22] M. R. Lowry, "Algorithm synthesis through problem reformulation," inProc. 1987 Nat. Conf. Artificial Intelligence. Seattle, WA, July 13-17, 1987; Kestrel Inst., Tech. Rep. KES.U.87.10, Aug. 1987.[23] M. Lubars and M. Harandi, "Knowledge-based software design using design schemas," inProc. Ninth Int. Conf. Software Engineering, Monterey, CA, 1987, pp. 253-262.[24] R. D. McCartney, "Synthesizing algorithms with performance constraints," inProc. 1987 Nat. Conf. Artificial Intelligence, Seattle, WA, July 13-17, 1987, pp. 149-154.[25] J. D. Mostow, "Machine transformation of advice into a heuristic search procedure," inMachine Learning: An Artificial Intelligence Approach, R. S. Michalski, Ed. Palo Alto, CA: Tioga, 1983, pp. 367-404.[26] J. M. Neighbors, "The Draco approach to constructing software from reusable components,"IEEE Trans. Software Eng., vol. SE-10, no. 5, pp. 564-574, Sept. 1984.[27] R. Paige and F. Henglein, "Mechanical translation of set theoretic problem specifications into efficient RAM code--A case study,"J. Symbolic Computation, vol. 4, no. 2, pp. 207-232, 1987.[28] R. Paige and S. Koenig, "Finite differencing of computable expressions,"ACM Trans. Program. Lang. Syst., vol. 4, no. 3, pp. 402- 454, July 1982.[29] H. Partsch, "The CIP transformation system," inProgram Transformation and Programming Environments, P. Pepper, Ed. New York: Springer-Verlag, 1983, pp. 305-322.[30] H. Partsch and R. Steinbrüggen, "Program transformation systems,"ACM Comput. Surveys, vol. 15, no. 3, pp. 199-236, Sept. 1983.[31] W. Scherlis, "Program improvement by internal specialization," inProc. Eighth ACM Symp. Principles of Programming Languages, Williamsburg, VA, Jan. 1981, pp. 41-49.[32] E. Schonberg, J. Schwartz, and M. Sharir, "An automatic technique for the selection of data representations in SETL programs,"ACM Trans. Program. Lang. Syst., vol. 3, no. 2, pp. 126-143, Apr. 1981.[33] D. R. Smith, "Applications of a strategy for designing divide-and-conquer algorithms,"Sci. Comput. Program., vol. 8, no. 3, pp. 213- 229, June 1987; also Tech. Rep. KES.U.85.2, Kestrel Inst., Mar. 1985.[34] D. R. Smith, "Derived preconditions and their use in program synthesis," inSixth Conf. Automated Deduction(Lecture Notes in Computer Science, vol. 138), D. W. Loveland, Ed. Berlin: Springer-Verlag, 1982, pp. 172-193.[35] D. R. Smith, "Structure and design of global search algorithms," Kestrel Inst., Tech. Rep. KES.U.87.12, Nov. 1987; also inActa Inform., to be published.[36] D. R. Smith, "Top-down synthesis of divide-and-conquer algorithms,"Artificial Intell., vol. 27, no. 1, pp. 43-96, Sept. 1985; reprinted inReadings in Artificial Intelligence and Software Engineering, C. Rich and R. Waters, Eds. Los Altos, CA: Morgan Kaufmann, 1986.[37] D. R. Smith and M. R. Lowry, "Algorithm theories and design tactics," inProc. Int. Conf. Mathematics of Program Construction(Lecture Notes in Computer Science, vol. 375), L. van de Snepscheut, Ed. Berlin: Springer-Verlag, 1989, pp. 379-398; extended version to appear inSci. Comput. Program.[38] D. R. Smith and T. T. Pressburger, "Knowledge-based software development tools," inSoftware Engineering Environments, P. Brereton, Ed. Chichester, England: Ellis Horwood, 1988, pp. 79-103; also Tech. Rep. KES.U.87.6, Kestrel Inst., May 1987.[39] D. Steier, "Automatic algorithm design within a general architecture for intelligence," Ph.D. dissertation, Dep. Comput. Sci., Carnegie-Mellon Univ., Apr. 1989.[40] D. M. Steier and A. P. Anderson,Algorithm Synthesis: A Comparative Study. New York: Springer-Verlag, 1989.[41] D. S. Wile, "Program developments: Formal explanations of implementations,"Commun. ACM, vol. 26, no. 11, pp. 902-911, Nov. 1983.[42] N. Wirth, "Program development by stepwise refinement,"Commun. ACM, vol. 14, no. 4, pp. 221-227, Apr. 1971.
Index Terms:
KIDS; semiautomatic program development system; Kestrel Interactive Development System; formal specifications; algorithm design; deductive inference; program simplification; partial evaluation; finite differencing optimizations; data type refinement; compilation; k-queens problem; SUN-4/110; inference mechanisms; optimisation; software engineering.
Citation:
D.R. Smith, "KIDS: A Semiautomatic Program Development System," IEEE Transactions on Software Engineering, vol. 16, no. 9, pp. 1024-1043, Sept. 1990, doi:10.1109/32.58788
Usage of this product signifies your acceptance of the
Terms of Use.
|
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb