Proved-Patterns-Based Development for Structured Programs.

Dominique Cansell (1) , Dominique Méry (1)

1 MOSEL - Proof-oriented development of computer-based systems

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.

Domaines: Autre [cs.OH]

Dominique Cansell, Dominique Méry. Proved-Patterns-Based Development for Structured Programs.. Computer Science - Theory and Applications, Second International, Symposium on Computer Science in Russia - CSR 2007, Ural State University (USU) ; Institute of Mathematics and Mechanics of Ural Branch of Russian Academy of Sciences, Sep 2007, Ekaterinburg, Russia. pp.104-114, ⟨10.1007/978-3-540-74510-5_13⟩. ⟨inria-00168307⟩