pyeb: A Python Implementation of Event-B Refinement Calculus
Abstract
This paper presents the PyEB tool, a Python implementation of the Event-B refinement calculus. The PyEB tool takes a Python program and generates several proof obligations that are then passed into the Z3 solver for verification purposes. The Python program represents an Event-B model. Examples of these proof obligations are machine invariant preservation, feasibility of non-deterministic event actions, event guard strengthening, event simulation, and correctness of machine variants. The Python program follows a particular object-oriented syntax; for example, actions, events, contexts, and machines are encoded as Python classes. We implemented PyEB as a PyPI (Python Package Index) library, which is freely available online. We carried out a case study on the use of PyEB. We modelled and verified several sequential algorithms in Python, e.g., the binary search algorithm and the square-root algorithm, among others. Our experimental results show that PyEB verified the refinement calculus models written in Python.
Keywords
Cite
@article{arxiv.2505.13454,
title = {pyeb: A Python Implementation of Event-B Refinement Calculus},
author = {Néstor Cataño},
journal= {arXiv preprint arXiv:2505.13454},
year = {2025}
}