USING MATHEMATICAL INDUCTION IN SYSTEMATIC PROGRAM DEVELOPMENT
Jianxin Li, Arun Lakhotia · International Journal of Software Engineering and Knowledge Engineering · 1994
This paper makes a contribution to the calculational paradigm of program development, a paradigm in which programs are calculated from their specifications by applying meaning preserving transformations. It introduces program induction, a technique analogous to mathematical induction, and iteration folding, a refinement rule. Using program induction, a specification is decomposed into a base case and an inductive case and their solutions are sequentially composed to derive the final program. The iteration folding rule is applied to transform potentially infinite nested if statements into a while statement. Our technique and rule augment the existing repertoire of techniques and rules in the calculus of program refinement.