Refinement-Based Guidelines for Algorithmic Systems

Dominique Méry 1, *
* Auteur correspondant
1 MOSEL - Proof-oriented development of computer-based systems
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : The correct-by-construction approach can be supported by a progressive and incremental process controlled by the refinement of models of programs. We explore the EVENT B modelling language to illustrate the expression of our methodological proposal using proof-based patterns called guidelines. The main ob jective is to facilitate the correct- by-construction approach for designing classical sequential algorithms. We address the de- scription of guidelines for the design of programs and algorithms and the integration of proof-based aspects using the RODIN platform. More precisely, we introduce several method- ological steps identified during the development of case studies, and we propose auxiliary notions, such as refinement diagrams, for guiding users during problem analysis. A general structure characterizes the relationship between the contract, the EVENT B, and the devel- oped algorithm using a specific application of EVENT B models and refinement. We simplify the translation of EVENT B models into algorithmic elements by promoting the use of recur- sive constructs. The resulting algorithm is proved to be sound with respect to the pre/post specification, namely, the contract. Applications rely on a dynamic programming technique that illustrates the applicability of these patterns based on a call-as-event relationship. Each proof-based development is validated using the RODIN platform. Our paper contributes to the development of patterns for assisting the proof-based development of algorithmic systems.
Type de document :
Article dans une revue
International Journal of Software and Informatics (IJSI), ISCAS, 2009, 3 (2-3), pp.197-239. 〈〉
Liste complète des métadonnées
Contributeur : Dominique Méry <>
Soumis le : lundi 26 octobre 2009 - 05:31:27
Dernière modification le : jeudi 11 janvier 2018 - 06:19:52


  • HAL Id : inria-00426383, version 1



Dominique Méry. Refinement-Based Guidelines for Algorithmic Systems. International Journal of Software and Informatics (IJSI), ISCAS, 2009, 3 (2-3), pp.197-239. 〈〉. 〈inria-00426383〉



Consultations de la notice