28973 articles – 22398 references  [version française]

inria-00099793, version 1

Formal derivation of spanning trees algorithms

Jean-Raymond Abrial a, Dominique Cansell () b, 1, Dominique Méry () c, 1

Third International Conference of B and Z Users - ZB'2003 2651 (2003) 457-476

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.

  • a –  CONSULTANT - MARSEILLE
  • b –  INRIA
  • c –  UNIVERSITE HENRI POINCARE
  • 1:  MOSEL (INRIA Lorraine - LORIA)
  • INRIA – CNRS : UMR7503 – Université Henri Poincaré - Nancy I – Université Nancy II – Institut National Polytechnique de Lorraine (INPL)
  • Domain : Computer Science/Other
  • Keywords : refinement – proof – development – graph – tree || raffinement – preuve – développement – graphe – arbre
  • Internal note : A03-R-043 || abrial03a
  • Comment : Colloque avec actes et comité de lecture. internationale.
 
  • inria-00099793, version 1
  • http://hal.inria.fr/inria-00099793
  • oai:hal.inria.fr:inria-00099793
  • From: Publications Loria <>
  • Submitted on: Tuesday, 26 September 2006 09:41:16
  • Updated on: Thursday, 28 September 2006 15:22:46