Incremental Parametric Development of Greedy Algorithms

Dominique Cansell 1 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 event B method provides a general framework for modelling both data structures and algorithms. B models are validated by discharging proof obligations ensuring safety properties. We address the problem of development of greedy algorithms using the seminal work of S. Curtis; she has formalised greedy algorithms in a relational calculus and has provided a list of results ensuring optimality results. Our first contribution is a re-modelling of Curtis's results in the event B framework and a mechanical checking of theorems on greedy algorithms The second contribution is the reuse of the mathematical framework for developing greedy algorithms from event B models; since the resulting event B models are generic, we show how to instantiate generic event B models to derive specific greedy algorithms; generic event B developments help in managing proofs complexity. Consequently, we contribute to the design of a library of proof-based developed algorithms.
Keywords : greedy algorithms Formal method B event-based method refinement safety greedy algorithms.
Type de document :
Article dans une revue
Electronic Notes in Theoretical Computer Science, Elsevier, 2007, roceedings of the 6th International Workshop on Automated Verification of Critical Systems (AVoCS 2006), 185, pp.47-62. 〈10.1016/j.entcs.2007.05.028〉
Liste complète des métadonnées
https://hal.inria.fr/inria-00594883
Contributeur : Dominique Méry <>
Soumis le : samedi 21 mai 2011 - 16:55:26
Dernière modification le : jeudi 11 janvier 2018 - 06:19:52

Lien texte intégral

openaccess

Identifiants

Collections

INRIA | LORIA | UNIV-LORRAINE

Citation

Dominique Cansell, Dominique Méry. Incremental Parametric Development of Greedy Algorithms. Electronic Notes in Theoretical Computer Science, Elsevier, 2007, roceedings of the 6th International Workshop on Automated Verification of Critical Systems (AVoCS 2006), 185, pp.47-62. 〈10.1016/j.entcs.2007.05.028〉. 〈inria-00594883〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

237

Contact


archive-ouverte@inria.fr