Formal Developments with RODIN

To get the enumeration development click here.

The enumeration problem addresses a collection of important algorithmic issues related to distributed computations. Based on local computations, we present the formal development of Mazurkiewicz's algorithm. The main idea relies upon the development of the problem following a top/down approach that can be supported by an incremental process controlled by the refinement of models. Event-B modelling language is supporting this methodology.