A Methodology for Program Construction by Stepwise Structural Enhancement

We advocate incremental construction of programs based on the idea of skeletons and techniques. Program construction begins bottom-up by first identifying skeleton program(s) embodying the central data structure(s), and proceeds by building computations around the control flow of the skeleton program(s) by application of techniques. Techniques are high level abstractions for the generic, frequently performed structural changes to programs. Positive consequences of structuring a program in terms of techniques applied to skeletons are ease of explanation, potential for program analysis, proof of correctness, and program maintenance. The paper illustrates each of these benefits with simple programs. 1 Introduction We present a method for incremental, bottom-up construction of provably correct programs using the notions of skeletons and techniques. Our method concerns correct implementation of a software design. We believe that software design involves user creativity, and attempting to ..