Refinement-Based Guidelines for Algorithmic Systems
Résumé
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.