Program Synthesis and Extension

Abstract

Over the years, researchers have tried to gain insight into the haphazard art of programming. This has led to the development of “structured programming,” which has been defined as “the task of organizing one’s thought in a way that leads, in a reasonable time, to an understandable expression of a computing task.”^p1 One of the guidelines of structured programming is that “one should try to develop a program and its proof of correctness hand-in-hand.”^p2 Much has been written on the subject, including [Dijkstra68], [Wirth71], pahlDijkstraHoare72], [Wirth73], [Wirth74], [ConwayGries75], [Dijkstra76], [Gries81], and others.

While the design of an alternative construct now seems to be a reasonably straightforward activity, that of a repetitive construct requires what I regard as “the invention” of an invariant relation and a variant function. —Edsger Wybe Dijkstra (Guarded commands, nondeterminancy and formal derivation of programs)