| 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: 4808 |
| Download times: 3047 |
|
| 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 |
