Key points are not available for this paper at this time.
Le Système de Développement Interactif Kestrel (KIDS) fournit un support automatisé pour le développement de programmes corrects et efficaces à partir de spécifications formelles. Le système a des composants pour effectuer la conception d'algorithmes, l'inférence déductive, la simplification de programmes, l'évaluation partielle, les optimisations par différences finies, le raffinement de types de données, la compilation et d'autres opérations de développement. Bien que leur application soit interactive, toutes les opérations de KIDS sont automatiques sauf les tactiques de conception d'algorithmes qui nécessitent actuellement une certaine interaction. Des dizaines de programmes ont été dérivés en utilisant le système et nous croyons que KIDS pourrait être développé au point de devenir économique à utiliser pour la programmation routinière. Pour illustrer l'utilisation de KIDS, nous traçons la dérivation d'un algorithme pour énumérer les solutions au problème des k-reines. L'algorithme initial que KIDS conçoit prend environ soixante minutes sur un SUN-4/110 pour trouver toutes les 92 solutions de l'instance du problème des 8-reines.
Douglas R. Smith (Mon,) a étudié cette question.