Incremental Parametric Development of Greedy Algorithms

Dominique Cansell 1 Dominique Méry 1
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.
Type de document :
Communication dans un congrès
Stephan Merz and Tobias Nipkow. 6th International Workshop on Automatic Verification of Critical Systems - AVoCS 2006, Sep 2006, Nancy, France. pp.48-62, 2006, Automatic Verification of Critical Systems (AVoCS 2006)
Liste complète des métadonnées

Littérature citée [10 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00089497
Contributeur : Stephan Merz <>
Soumis le : vendredi 18 août 2006 - 19:53:03
Dernière modification le : jeudi 11 janvier 2018 - 06:19:52
Document(s) archivé(s) le : mardi 6 avril 2010 - 00:38:09

Identifiants

  • HAL Id : inria-00089497, version 1

Collections

Citation

Dominique Cansell, Dominique Méry. Incremental Parametric Development of Greedy Algorithms. Stephan Merz and Tobias Nipkow. 6th International Workshop on Automatic Verification of Critical Systems - AVoCS 2006, Sep 2006, Nancy, France. pp.48-62, 2006, Automatic Verification of Critical Systems (AVoCS 2006). 〈inria-00089497〉

Partager

Métriques

Consultations de la notice

241

Téléchargements de fichiers

141