Refinement-based guidelines for developing structured programs

The development of structured programs is carried out either using bottom-up techniques, or top-down techniques; we show how refinement and proof can be used to help in the top-down development of structured imperative programs. When a problem is stated, the incremental proof-based methodology of event B starts by stating a very abstract model and further refinements lead to finer-grain event-based models which are used to build an algorithm. In this paper, the main idea is to consider each procedure call as an abstract event of a model corresponding to the development of the procedure; generally, a procedure is specified by a pre/post specification and then the refinement process can lead to a set of events, which are then combined to obtain the body of the procedure. It means that the abstraction corresponds to the procedure call and the body is derived by the refinement process. The refinement process may also use recursive procedures and it supports the top-down refinement. The technique is illustrated by the sorting problem.