ABSTRACT
This chapter illustrates the principle of reasoned development of loops. It explains that writing a loop is a straightforward task, but every programmer knows how tricky it can be. Generally, the rational development of a program consists in considering it as a mechanism which transforms a “system” from an initial state called “precondition” to a final state named “postcondition” or “goal”. The notation prec prog postc, used from now on, means that the program prog does come to an end and allows to go from the situation prec to the situation postc. In other words, prog being a program, prec and postc being predicates, prec prog postc means that if prog is run starting in a state complying with prec then it finishes and the state reached meets the predicate postc.
