KIDS - A SEMIAUTOMATIC PROGRAM-DEVELOPMENT SYSTEM

被引:147
作者
SMITH, DR
机构
[1] Kestrel Institute, Palo Alto, CA 94304
关键词
Algorithm design; automated deduction; automated programming; data type refinement; formal specifications; program optimization; program transformation;
D O I
10.1109/32.58788
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
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 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. © 1990 IEEE
引用
收藏
页码:1024 / 1043
页数:20
相关论文
共 42 条
[1]  
ABRAIDOFADINO L, 1987, 2ND P INT S KNOWL EN
[2]  
BALZER R, 1983, COMPUTER, V16, P39, DOI 10.1109/MC.1983.1654237
[3]   TRANSFORMATIONAL IMPLEMENTATION - AN EXAMPLE [J].
BALZER, R .
IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 1981, 7 (01) :3-14
[4]  
BARSTOW D, 1988, 10TH P INT C SOFTW E, P439
[5]  
BARSTOW D, 1979, KNOWLEDGE BASED PROG
[6]  
BJORNER D, 1988, PARTIAL EVALUATION M
[7]  
BLAINE L, 1988, KESU8811 KESTR I TEC
[8]  
BORRAS P, 1988, ACM SIGPLAN NOTICES, V24, P14
[9]   PROGRAM-DEVELOPMENT - FROM ENUMERATION TO BACKTRACKING [J].
BROY, M ;
WIRSING, M .
INFORMATION PROCESSING LETTERS, 1980, 10 (4-5) :193-197
[10]   TRANSFORMATION SYSTEM FOR DEVELOPING RECURSIVE PROGRAMS [J].
BURSTALL, RM ;
DARLINGTON, J .
JOURNAL OF THE ACM, 1977, 24 (01) :44-67