pyeb: A Python Implementation of Event-B Refinement Calculus

TL;DR

PyEB is a Python tool that models Event-B refinement calculus, generating proof obligations verified by Z3, enabling formal verification of algorithms modeled in Python classes.

Contribution

This work introduces PyEB, a novel Python library that models Event-B refinement calculus and automates proof obligation generation and verification.

Findings

PyEB successfully verified several algorithms in Python.

Proof obligations are effectively generated and checked using Z3.

PyEB is available as a free Python package.

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.