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.
Keywords : greedy algorithms Formal method B event-based method refinement safety greedy algorithms.
Document type :
Journal articles
Complete list of metadatas
https://hal.inria.fr/inria-00594883
Contributor : Dominique Méry <>
Submitted on : Saturday, May 21, 2011 - 4:55:26 PM
Last modification on : Thursday, September 19, 2019 - 1:14:05 AM

Links full text

openaccess

Identifiers

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⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

266

Contact


archive-ouverte@inria.fr