Search Swinburne Research Bank
Please use this identifier to cite or link to this item: http://hdl.handle.net/1959.3/155488
- Using mathematical induction in systematic program development
- Li, Jianxin; Lakhotia, Arun
- 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.
- Publication type
- Journal article
- International Journal of Software Engineering and Knowledge Engineering, Vol. 4, no. 4 (Dec 1994), pp. 561-574
- Publication year
- FOR Code(s)
- 0801 Artificial Intelligence and Image Processing; 0803 Computer Software
- Calculational programming; Iteration folding; Mathematical induction; Program correctness; Program induction; Systematic program development
- World Scientific Publishing
- Publisher URL
- Copyright © 1994.
- Peer reviewed