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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [10 references]  Display  Hide  Download

https://hal.inria.fr/inria-00089497
Contributor : Stephan Merz <>
Submitted on : Friday, August 18, 2006 - 7:53:03 PM
Last modification on : Thursday, September 19, 2019 - 5:00:11 PM
Long-term archiving on : Tuesday, April 6, 2010 - 12:38:09 AM

Identifiers

  • HAL Id : inria-00089497, version 1

Collections

Citation

Dominique Cansell, Dominique Méry. Incremental Parametric Development of Greedy Algorithms. 6th International Workshop on Automatic Verification of Critical Systems - AVoCS 2006, Sep 2006, Nancy, France. pp.48-62. ⟨inria-00089497⟩

Share

Metrics

Record views

267

Files downloads

297