pyeb is a Python implementation of Event-B's refinement calculus. It takes an Event-B model as an input and generates proof-obligations that are eventually discharged with the Z3 SMT solver. Event-B models are written in Python following a special Object-Oriented syntax and notation. The pyeb tool generates proof obligations such as invariant preservation, feasibility of non-deterministic event actions, guard strengthening, simulation, preservation of machine variants, among others. pyeb uses Z3 Python API to discharge the proof obligations automatically. It supports large parts of Event-B' syntax such as non-deterministic assignments, events, machines, contexts, and machine refinements.

pyeb can be downloaded from GitHub.

Getting Started (Mac OS X)

It is recommended to run pyeb in a virtual environment thus it will not have collateral effects on your local installation. pyeb dependencies are the Z3 solver, antlr Python runtime, and the antlr tools.

1. Creating and activating the virtual environment::

   python -m venv .venv

   source .venv/bin/activate

2. Optionally, you can deactivate the virtual environment after using pyeb::

   deactivate

3. Installing dependencies::

   pip install z3-solver==4.13.0.0

   pip install antlr4-tools==0.2.1

   pip install antlr4-python3-runtime==4.13.1

4. Installing pyeb::

   pip install pyeb

Command Line Usage (Mac OS)

1. Running pyeb::

   pyeb python-file

2. We have included a sample folder with several object-oriented examples of sequential algorithms (binary search, squared root, inverse function, etc.)::

   pyeb sample/binsearch_oo.py

Unit testing with pytest

1. Installing pytest::

   pip install pytest

2. Running pytest on a file in the sample directory::

   pytest tests/test_binsearch.py

GitHub Installation

You might want to install and run the latest version of pyeb available from GitHub.

1. Installing pyeb::

   mkdir dist

   cd dist

   git init

   git remote add origin https://github.com/ncatanoc/pyeb.git

   git pull origin main

   git branch -M main

2. Running pyeb as a console script::

   python main.py sample/binsearch_oo.py

3. Optionally, Running pyeb as a module::

   python -m pyeb sample/binsearch_oo.py

Troubleshooting

For any questions or issues regarding pyeb, contact Néstor Cataño nestor.catano@gmail.com.