Vizing’s theorem proved using Event-B and Rodin

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.


The whole approach strikes me as slightly unwieldy and not as elegant as I would have imagined at first. But this impression may be rooted in my unfamiliarity with refinement based approaches. Just one question: If you had a choice, which tool or theory would you use to formalize the proof? Would you say that Event-B is a formalism that's worth investigating if one is already quite happy with type theoretic theorem provers?
#1 Thomas am 2011-04-15T12:56:20+00:00
Hi Thomas,

Thanks for your questions. I have replied in the body of the post.

#2 Joachim Breitner (Homepage) am 2011-04-15T13:23:17+00:00

Have something to say? You can post a comment by sending an e-Mail to me at <mail@joachim-breitner.de>, and I will include it here.