Joachim Breitner's Homepage

As the project for the course “System specification and implementation”, which introduced the Event-B formalism to us, I modeled the algorithm given in one of the constructive proofs of Vizing’s theorem and showed it to be correct, using the Event-B tool Rodin. Vizing’s theorem states

For a finite undirected graph without autoloops and without multiple edges, at any vertex of which no more than N edges meet, N+1 colors suffice for an edge coloring such that edges incident on the same vertex are of different color.

You can find more details about my approach and my conclusions about Event-B and Rodin in the project report and you can download my Rodin model.

I was asked in the comments about my conclusions, so I’ll reply here. The proof looks unweidly, but I do think that refinement based proofs, where possible, increase clarity, as more, but smaller steps have to be looked at. Also note that I had no prior exposure to Rodin, so some thing could have been done quicker and easier with more experience. But Rodin itself is not the theorem proving tool of my choice. More detail in the report, shortly put: Its math is too weak and not expressive enough, individual proofs are WORN (write-once-read-never) and can easily be lost when changing the models and there is too little emphasis on correctness, e.g. no trusted core base approach known from dedicated theorem provers. So I would use a different tool for proving mathematical statements, nevertheless the idea of refinements, and trying to find those small-steps-refinements, can also help coming up with better proofs in those tools.