Service interruption on Monday 11 July from 12:30 to 13:00: all the sites of the CCSD (HAL, Epiciences, SciencesConf, AureHAL) will be inaccessible (network hardware connection).
Skip to Main content Skip to Navigation
Journal articles

Refinement-Based Guidelines for Algorithmic Systems

Dominique Méry 1, * 
* Corresponding author
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.
Document type :
Journal articles
Complete list of metadata
Contributor : Dominique Méry Connect in order to contact the contributor
Submitted on : Monday, October 26, 2009 - 5:31:27 AM
Last modification on : Friday, February 4, 2022 - 3:30:08 AM


  • 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⟩



Record views