Skip to Main content Skip to Navigation
Journal articles

Incremental Parametric Development of Greedy Algorithms

Dominique Cansell 1 Dominique Méry 1, * 
* Corresponding author
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.
Document type :
Journal articles
Complete list of metadata
Contributor : Dominique Méry Connect in order to contact the contributor
Submitted on : Saturday, May 21, 2011 - 4:55:26 PM
Last modification on : Friday, February 4, 2022 - 3:30:57 AM

Links full text




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⟩



Record views