Proved-Patterns-Based Development for Structured Programs.

Dominique Cansell 1 Dominique Méry 1
1 MOSEL - Proof-oriented development of computer-based systems
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : 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.
Type de document :
Communication dans un congrès
Volker Diekert and Mikhail V. Volkov and Andrei Voronkov. Computer Science - Theory and Applications, Second International, Symposium on Computer Science in Russia - CSR 2007, Sep 2007, Ekaterinburg, Russia. Springer Berlin / Heidelberg, 4649, pp.104-114, 2007, Lecture Notes in Computer Science. 〈10.1007/978-3-540-74510-5_13〉
Liste complète des métadonnées

https://hal.inria.fr/inria-00168307
Contributeur : Dominique Cansell <>
Soumis le : lundi 27 août 2007 - 13:19:54
Dernière modification le : jeudi 11 janvier 2018 - 06:19:52

Identifiants

Collections

Citation

Dominique Cansell, Dominique Méry. Proved-Patterns-Based Development for Structured Programs.. Volker Diekert and Mikhail V. Volkov and Andrei Voronkov. Computer Science - Theory and Applications, Second International, Symposium on Computer Science in Russia - CSR 2007, Sep 2007, Ekaterinburg, Russia. Springer Berlin / Heidelberg, 4649, pp.104-114, 2007, Lecture Notes in Computer Science. 〈10.1007/978-3-540-74510-5_13〉. 〈inria-00168307〉

Partager

Métriques

Consultations de la notice

166