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.
Type de document :
Communication dans un congrès
Didier Bert, Jonathan Peter Bowen, Steve King, Marina Walden. Third International Conference of B and Z Users - ZB'2003, 2003, Turku, Finland, Springer Verlag, 2651, pp.457-476, 2003, Lecture Notes in Computer Science
Liste complète des métadonnées

https://hal.inria.fr/inria-00099793
Contributeur : Publications Loria <>
Soumis le : mardi 26 septembre 2006 - 09:41:16
Dernière modification le : jeudi 11 janvier 2018 - 06:19:52

Identifiants

  • HAL Id : inria-00099793, version 1

Collections

Citation

Jean-Raymond Abrial, Dominique Cansell, Dominique Méry. Formal derivation of spanning trees algorithms. Didier Bert, Jonathan Peter Bowen, Steve King, Marina Walden. Third International Conference of B and Z Users - ZB'2003, 2003, Turku, Finland, Springer Verlag, 2651, pp.457-476, 2003, Lecture Notes in Computer Science. 〈inria-00099793〉

Partager

Métriques

Consultations de la notice

146