pyeb: A Python Implementation of Event-B Refinement Calculus
Néstor Cataño
TL;DR
The paper tackles the barrier to formal refinement methods by implementing PyEB, a Python-based encoding of the Event-B refinement calculus that generates proof obligations and discharges them with the Z3 SMT solver. By providing a PyPI library, Python-style modeling of contexts, machines, and events, and a case study on sequential algorithms, PyEB demonstrates that Event-B refinement can be accessible to mainstream programmers. It contributes a concrete encoding strategy (including non-deterministic actions and machine variants) and demonstrates practical verification of refinement models, illustrating the viability of formal methods within Python ecosystems. The work advances practical formal verification by enabling verification of refinement correctness and sets the stage for future automation toward correct-by-construction code generation and broader operator/LTL support.
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.