Refinement-Based Guidelines for Algorithmic Systems
Received:February 18, 2009  Revised:August 15, 2009  Download PDF
Dominique Méry. Refinement-Based Guidelines for Algorithmic Systems. International Journal of Software and Informatics, 2009,3(2):197~239
Hits: 4513
Download times: 2536
Fund:This work is sponsored by grant No. ANR-06-SETI-015-03 awarded by the Agence Nationale de la Recherche.
Abstract:The correct-by-construction approach can be supported by a progressive and incremental process controlled by the re.nement 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 objective 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 identi.ed during the development of case studies, and we propose auxiliary notions, such as re.nement 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 speci.c application of EVENT B models and re.nement. 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 speci.cation, 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.
keywords:EVENT B  modelling  re.nement  algorithm  pattern  proof  formal method  proof-based development  correct by construction
View Full Text  View/Add Comment  Download reader



Top Paper  |  FAQ  |  Guest Editors  |  Email Alert  |  Links  |  Copyright  |  Contact Us

© Copyright by Institute of Software, the Chinese Academy of Sciences

京公网安备 11040202500065号