Program development by inductive stepwise refinement
R. Geoff Dromey · Software Practice and Experience · 1985
Abstract A constructive method of program development is presented. It seeks to unify two important ideas about program development. Namely that programming is a goal‐oriented activity and that there should be a correspondence between data and program structures. The latter concept is seen to be extensible beyond the data processing context in which it was originally proposed. Induction provides the vehicle for program development by stepwise refinement, with the final program being constructed by application of a sequence of progressively more powerful generalizations. The design process employed guarantees the correctness of the final program provided that each of the refinement steps have been correctly taken. The method is illustrated by a number of samples.