Mechanical translation of set theoretic problem specifications into efficient RAM code — A case study

There have been various proposals for program development methodologies in which a computer system is used to aid in the formulation of precise problem specifications, in the synthesis of efficient and correct programs, and in the analysis of performance. A few systems have actually been implemented. Although some of these systems are fully general in expressive power, they all lack a sufficient degree of automation to make them viable alternatives to conventional ad hoc approaches.