We present a specification, a derivation and total correctness proofs of operations for bi-functional graphs implemented with pointers, including the Schorr-Waite algorithm. This one marks such a graph with an economical depth-first strategy. Our approach is purely algebraic and functional, from a simple graph specification to the simulation of a tail-recursive imperative program, then to a true C pointer program by elementary classical transformations. We stay in the unique higher-order formalism of the Calculus of Inductive Constructions for specifications, programs and proofs. All the development is supported by Coq.
J-F. Dufourd
ICFEM , Volume 8829 , page 139-154 - 2014
International conference with proceedings
Pointer Program Derivation using Coq: Graphs and Schorr-Waite Algorithm, ICFEM, Luxembourg, Luxembourg, pages 139-154, Springer-Verlag, LNCS, Volume 8829, novembre 2014, doi:10.1007/978-3-319-11737-9_10
Research team : IGG
@Inproceedings{4-Dufo14a, author = {Dufourd, J-F.}, title = {Pointer Program Derivation using Coq: Graphs and Schorr-Waite Algorithm}, booktitle = {ICFEM}, series = {LNCS}, volume = {8829}, pages = {139-154}, month = {Nov}, year = {2014}, publisher = {Springer-Verlag}, doi = {10.1007/978-3-319-11737-9_10}, x-international-audience = {Yes}, x-language = {EN}, url = {http://publis.icube.unistra.fr/4-Dufo14a} }