Proving Quicksort Correct in Event-B

Citations of this article
Mendeley users who have this article in their library.


The Event-B method can be used to model all sorts of discrete event systems, among them sequential programs. We have made the experience that the minimalist nature of Event-B is of advantage when it comes to tool support and to using proof as a means to analyse a model. The downside of the minimalism is that when models get more complex the lack of structure in the models can make them cluttered with auxiliary variables. System decomposition will not solve this problem. This can not be reasonably applied to a sequential program. In this article we describe our experiences with using Event-B by way of an example. We show how we verified iterative Quicksort in Event-B and intersperse our observations and criticisms. We use them to formulate some suggestions of how we believe Event-B should evolve in future. Some of the minimalism may have to be abandoned in favour of more clarity of the produced formal models. © 2009 Elsevier B.V. All rights reserved.




Hallerstede, S. (2009). Proving Quicksort Correct in Event-B. Electronic Notes in Theoretical Computer Science, 259(C), 47–65.

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free