Premium
Program development by inductive stepwise refinement
Author(s) -
Dromey R. Geoff
Publication year - 1985
Publication title -
software: practice and experience
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.437
H-Index - 70
eISSN - 1097-024X
pISSN - 0038-0644
DOI - 10.1002/spe.4380150102
Subject(s) - correctness , computer science , development (topology) , constructive , structured programming , programming language , refinement calculus , process (computing) , context (archaeology) , sequence (biology) , program structure , program analysis , program design language , software engineering , theoretical computer science , mathematics , paleontology , genetics , biology , mathematical analysis
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.