HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

Formal derivation of spanning trees algorithms

Jean-Raymond Abrial 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 : Graphs algorithms and graph-theoretical problems provide a challenging battlefield for the incremental development of proved models. The B event-based approach implements the incremental and proved development of abstract models which are translated into algorithms; we focus our methodology on the minimum spanning tree problem and on Prim's algorithm. The correctness of the resulting solution is based on properties over trees and we show how the greedy strategy is efficient in this case. We compare properties proven mechanically to the properties found in a classical algorithms textbook.
Document type :
Conference papers
Complete list of metadata

Contributor : Publications Loria Connect in order to contact the contributor
Submitted on : Tuesday, September 26, 2006 - 9:41:16 AM
Last modification on : Friday, February 4, 2022 - 3:33:13 AM


  • HAL Id : inria-00099793, version 1



Jean-Raymond Abrial, Dominique Cansell, Dominique Méry. Formal derivation of spanning trees algorithms. Third International Conference of B and Z Users - ZB'2003, Marina Walden, 2003, Turku, Finland, pp.457-476. ⟨inria-00099793⟩



Record views