# pyeb: Bridging Event-B Refinement and Python for Automated Program Verification

## Néstor Cataño

<figure><img src="image_1.png" /></figure>

### ► To cite this version:

Néstor Cataño. pyeb: Bridging Event-B Refinement and Python for Automated Program Verification. 2025. hal-05053034

HAL Id: hal-05053034

https://hal.science/hal-05053034v1

Preprint submitted on 1 May 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_2.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# pyeb: Bridging Event-B Refinement and Python for Automated Program Verification

Néstor Cataño¹*

¹*Faculdade de Ciências e Tecnologia, Universidade do Algarve, Faro, Portugal.

Corresponding author(s). E-mail(s): nestor.catano@gmail.com;

## 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 proof obligations attest to the soundness of the Python-written model. pyeb implements most of the refinement calculus structure of the Event-B language and the Rodin platform. Examples of 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 must be encoded as Python classes.

The pyeb tool is implemented as a PyPI (Python Package Index) library, which is freely available online. We have tested pyeb on several sequential programming algorithms, such as the binary search algorithm, the square root algorithm, and an algorithm that finds the minimum of an array. Our experimental results show that pyeb can verify the correctness of the algorithms. pyeb supports Event-B's syntax in Python, including deterministic and non-deterministic event actions, events, machines, machine contexts, machine variants and invariants, events, event refinement, and machine refinement. Given Python's widespread adoption and rich ecosystem, we expect pyeb to contribute to our long-term goal of making formal methods based on refinement calculus more popular. pyeb simplifies access to formal methods by making refinement calculus more approachable for software developers without extensive mathematical training.

**Keywords:** Event-B, Formal Methods, Program Correctness, Python, Refinement Calculus, Testing.

## 1 Introduction

The traditional style of programming today uses a low-level programming language (e.g. C, Java, or Python) to encode the design decisions (often expressed as informal specifications) a programmer has in mind. This style justifies the view that programming languages are high-level program abstractions. However, this view has a few drawbacks. First, a key challenge is that establishing a formal relationship between informal

specifications and program code is error-prone and labour-intensive. Second, although errors in informal specifications can be detected through simulation or animation, they are better spotted once a code implementation is already in place, e.g., formal specifications are not always executable whereas program code can be unit-tested. A third issue is related to code documentation, which oftentimes is either non-existent or is informally written within the code. Informal specifications make it difficult for (formal) tools to reason about
program correctness. A fourth issue relates to code evolution; as program designs evolve and code documentation is maintained informally, it is difficult to establish a palpable formal relationship between the original program and new or refined versions of it. Ideally, one would like to ensure that any new program version (at least) enjoys the same properties as the original version of the program. This code evolution problem is exacerbated when multiple developers work on the same program or code baseline and make changes concurrently.

Another program style is stepwise refinement [1], therefore, a high-level program specification is written, then transformed into a more concrete program through successive correctness-preserving transformations. Refinement calculus [2] is a formalisation of the stepwise refinement approach based on the action system formalism [3] for parallel and distributed computations; therefore, actions can be executed in parallel as long as they do not write into common variables. Actions are atomic: they are executed completely without interference from any other action. Atomicity guarantees that parallel executions of a system can be expressed in terms of non-deterministic sequential executions. The Rodin [4] and Atelier-B [5] Toolsets provide support for refinement calculus.

Total correctness is the underlying correctness notion of the refinement calculus. This is the appropriate notion for parallel algorithms executed sequentially by cooperation between actions. Program algorithms are expected to terminate only if their final result is of interest. With every program step refinement, proof obligations are generated that ensure the correctness of the refinement process; thus, every refined model is a correct refinement. Proof obligations address the issue of the traditional programming view concerning the proper tracking of program evolution. It also enables formal tools to reason about programs.

This paper presents the pyeb tool, a Python implementation of Event-B refinement calculus with which users can write and verify Event-B models written in Python. 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 that is yet to be written in Python. The generated proof obligations attest to

the soundness of the Python-written model. The pyeb tool generates proof obligations similar to those generated by the Rodin IDE for Event-B models [4, 6]. 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. We have conducted a case study on the verification of sequential algorithms with the pyeb tool. Our experimental results show that pyeb can verify the correctness of sequential algorithms.

The main contributions of this paper are the following:

* We have carried out an implementation of Event-B's refinement calculus in Python. Our implementation (the pyeb tool) is a PyPI library [7], which can be freely installed using the pip [8] Python package installer. pyeb provides support for Event-B's syntax, including machines, contexts, events, deterministic and non-deterministic event actions, event guards, predicates, machine variants and invariants, event refinement, and machine refinement, among other syntaxes.

* We carried out a case study on the modelling and verification of sequential algorithms with pyeb. These algorithms have been written elsewhere by J.-R. Abrial in [9]. They include the binary search algorithm, an algorithm for finding the minimum element of an array, an algorithm that searches for a value in an array, and an algorithm that calculates the square root. We have manually written the algorithms in Python (from the Event-B versions) and used pyeb to generate and discharge the generated proof obligations. The files of the case study are hosted at https://github.com/ncatanoc/pyeb

* To enhance its usability, the pyeb tool seamlessly integrates with the Pytest framework [10], allowing users to unit-test their formal models in Python. The GitHub website https://github.com/ncatanoc/pyeb/tree/-/main/tests includes the test files for the algorithms of the case study.

* pyeb contributes to our long-term goal of making refinement-calculus-based formal methods more accessible and popular for standard programmers often unfamiliar with Event-B's mathematical syntax. In the long run, pyeb
will play a pivotal role in developing alternative and accessible tool support for Event-B that will include the generation of Python and Rust code and the use of machine learning techniques for program repair. Despite the capabilities of existing tools like Rodin, there is a lack of lightweight Python-based solutions that integrate seamlessly with modern software development.

**Organisation.** This paper is organised as follows: Section 2 introduces the syntax and semantics of Event-B and gives a brief introduction to the Z3 solver. Section 3 presents our approach to modelling refinement calculus in Python; it presents the syntax of formal programs in Python, and it shows how proof obligations are generated and verified. Section 4 presents the implementation of the `pyeb` tool; it explains how `pyeb` can be installed and used; it also explains how `pyeb` can be used together with the `Pytest` testing framework. Section 5 presents our case study with `pyeb`. Section 6 discusses related work. Finally, Section 7 concludes.

# 2 Preliminaries

## 2.1 Event-B

Event-B models represent the development of transition systems. The models comprise *machines* and *contexts*. Machines comprise a static part that defines observations about the system, and a series of state transition operations called *events*. Each operation must maintain the machine invariants. Contexts define the static part of a machine (uninterpreted sets, constants, axioms, and theorems), whereas variables and invariants are defined within the machines. A machine definition generates a series of proof obligations, in essence, theorems stating a property that must be true for the machine to be consistent. For example, if an Event-B model includes an invariant property that states that some mathematical relation *r* is a function, then for each machine event that modifies *r*, a proof obligation is generated that states that the modified relation *r'* must be a function.

Software development with Event-B relies on *model refinement* [11, 12] whereby a machine goes through a series of stages, each adding more

<figure><img src="image_3.png" /><figcaption>**Fig. 1** i.) event syntax ii.) event refinement syntax</figcaption></figure>

details (called observations) to the description of the system. Hence, the most abstract machine is first developed and verified to satisfy the system's safety properties. Then, with every refinement machine, one must prove a correspondence between the refinement and its abstract machine, therefore, the refinement (concrete) machine fulfils at least the same properties that the abstract machine does. To prove such correspondence, refinement proof obligations are to be discharged (proven) to ensure that each refinement is a faithful and sound model of the previous machine, and so that all the machines satisfy the safety properties of the most abstract machine.

An Event-B-modelled system may reach a state where several event guards hold, for which we say that the system is *non-deterministic*. Event-B only allows events whose guards hold to be executed. If the system reaches a state where no event guard holds, it halts and is said to have deadlocked.

Figure 1 shows the syntax for events and event refinements. An event can have one of three possible *status*: **ordinary**, **convergent**, or **anticipated**. **convergent** events and machine variants are used to model Event-B models that halt, e.g., the sequential algorithms presented in Section 5. The body of an event (written between the keywords **then** and **end**) is composed of a set of actions. Actions compute new values for machine variables, thus performing an observable state transition. Actions can either be deterministic or non-deterministic and may change the value of machine variables as part of state transitions. Deterministic actions (assignments) use the `:=` operator, and non-deterministic assignments use the notation `:∈` (becomes in) or `:|` (becomes such
that) operators. The right side of :∈ is a set expression, and the right side of : | is a predicate. The left side of an assignment is a disjoint set of machine variables. The right side of a non-deterministic assignment might include a *before-after* predicate that relates machine variables pre- and post-state values.

Event-B provides some simplified syntax versions. For example, if `x` is empty, the event does not include an **any** clause. The event does not include a **then** clause if the actions are missing.

## 2.2 The SMT solver

Z3 is an efficient SMT solver with specialised algorithms for solving background theories [13]. SMT (Satisfiability Modulo Theories) problems are decision problems for logical formulas. Z3 provides background theories such as arithmetic, bit vectors, arrays, and uninterpreted functions. The Z3 solver is a high-performance solver developed by Microsoft Research that comes with an API for Python [14]. The API brings the Z3 solver functionality to Python. Hence, one can declare a solver in Python, add some formulae to it, and finally ask it if a solution exists or not. Solvers work pretty much as program stores in constraint programming where adding new formulae to the store constrains it. The Python API uses functions `check` below to decide if there is a model that satisfies the formulae previously added.

```python
n = Const('n', IntSort())
s = Solver() s.add(n > IntVal(55))
s.check()
if s.check() == sat:
    print(s.model())
```

## 3 Python Encoding

Next, we present our refinement calculus Python encoding and discuss underlying design and implementation decisions. We present our ideas with the aid of the Event-B model of the search algorithm in Figure 2. The left part shows the abstract Event-B machine and the right refinement machine. We do not show the machine context here, which includes the definition for an integer-valued total function `f` - modelling an array of size `n`, storing a `v` we search for. The variable `r` represents an index of the array `f`. The example in

Figure 2 uses the Rodin [4] notation, where predicates on different lines are implicitly conjoined, and actions on different lines run simultaneously.

We use Z3’s Python API [14] to represent uninterpreted constants and functions. For example, for the search algorithm in Section 5, we declare an integer-valued function `f`, an integer constant `n` (representing the size of `f`) and the value `v` we search for in `f`.

```python
self.f = Function('f', IntSort(), IntSort())
self.n = Const('n', IntSort())
self.v = Const('v', IntSort())
```

We use Python object-oriented syntax to encode Event-B syntax. Class `BContext` encodes machine contexts. Event-B contexts include constants, axioms, and theorems. Class `BContext` (not shown here) encodes them as dictionary class fields. `BContext` uses setter and getter methods to add and retrieve any value from or to these dictionaries. A dictionary accesses values through a key, which is a string, i.e. the name of the constant, axiom, or theorem, thus matching the way the Rodin IDE works [4]. Event-B constants and functions are encoded as Z3 constants and functions of some particular sort, e.g. `IntSort()` above.

**Primed variables.** Event-B models represent the development of discrete transition systems. Thus, we must find a way to represent $x'$, the value of a variable `x` at the *next* step. We encode $x'$ in Python with the help of the function `prime` below.

```python
def prime(x):
    s = x.sort()
    return Function("prime", s, s)(x)
```

The body of an event is composed of actions. We use function `prime` to encode them. Actions can either be deterministic or non-deterministic. Deterministic actions use the `:=` operator; for instance, in Figure 2, the `progress` refinement event uses the deterministic assignment `r := r+1`. Event-B provides two non-deterministic actions (assignment) operators, namely, `|` (becomes such that) and `:∈` (becomes in). The right side of `|` must be a predicate, and the right side of `:∈` must be a set expression. For instance, one can write the deterministic action above as `r:∈{r+1}`. Further,
∈ actions can always be reduced to :| actions. Hence, we can encode the two previous versions of the assignment as the action r : | r' = r +1. Therefore, `pyeb` only supports non-deterministic actions built with the aid of the :| operator.

We encode the right-hand side of the assignment above as the following *before-after* Python predicate.

`prime(self.r) == self.r+1`

**Frame-conditions.** Similar to *frame-conditions* [15] typically used in behavioural interface specification languages [16] in which one must state which part of the state a function or method may modify, non-deterministic actions must account for the state change of all the machine variables. Therefore, we wrap up *before-after* predicates within a `BAssignment` class which includes two fields: the assigned machine variables and the *before-after* predicate itself.

The whole event action is shown below, which corresponds to inc's actions on the right-hand side of Figure 2. `BAssignment`'s constructor takes the *before-after* predicate as the second parameter and the set of machine variables it modifies (assigns to) as the first parameter.

```
ba = BAssignment({self.r},
prime(self.r) == self.r+1)
```

The `skip` statement (see the code below) is implemented as a function that takes a set `v` of machine variables and returns a non-deterministic assignment such that no variable in `v` is assigned to. The function `conjunct` returns the logical-and of the predicates of a list.

```python
def skip(v):
    ba = conjunct([(prime.elm) == elm
                   for elm in v])
    res = BAssignment(v,ba)
    return res
```

___ `skip` ___

**Guards.** Event guards are modelled as Python dictionaries. The refinement event `progress` in Figure 2 is encoded as shown below, where `f` and `v` are declared in the machine context, and `r` is a machine variable.

```
guard = {'g': (self.Context.f(self.r) !=
                             self.Context.v)}
```

**Events.** We use classes `BEvent` and `BEventRef` to encode events and refinement events, respectively. The status of an event is encoded as a Python enumerated type (see below). Each event class declares a private class field of type dictionary for storing the event guards. The dictionary follows the structure of object guard above, using strings as keys and storing Z3 predicates. Each event class also has a class field of type `BAssignment` for storing the event body and a field of type `Status`.

```
Status = Enum('Status', ['Ordinary',
                             'Convergent', 'Anticipated'])
```

We show below the Python implementation of the event `progress` of the search algorithm (right side of Figure 2). The event progresses as it searches for value `v`; hence, increasing the value of `r` by one. The abstract event (left side of Figure 2) just constrains `r` to take a non-negative value between the boundaries of the array `f`. In the excerpt below, class `BEventRef` is parametrised by the name of the refinement event and the refined event, respectively. The status of the abstract event is **anticipated**, so the refinement event is **convergent**.

```python
def ref_event_progress(self):
    guard = {'grd': (self.Context.f(self.r)
               != self.Context.v)}
    ba = BAssignment({self.r},
                      prime(self.r) == (self.r+1))
    progress = BEventRef('progress',
                          super().event_progress())
    progress.set_status(status.Convergent)
    progress.add guards(guard)
    progress.add_bassg(ba)
    return progress

convergent
```

**Machines.** We also implement (not shown here) the class `BMachine` that encodes abstract machines, and the class `BMachineRefines` that encodes refinement Event-B machines, respectively. These classes include fields of type dictionary for modelling events, machine variables, and invariants. These classes also include a reference
<table><caption>**Fig. 2** i.) search abstract machine ii.) search refinement machine</caption><tr><td>machine abs</td><td>machine ref</td></tr><tr><td>sees context</td><td>refines abs</td></tr><tr><td></td><td>sees context</td></tr><tr><td>variables r</td><td>invariants</td></tr><tr><td></td><td>@inv1 r ∈ 1..n</td></tr><tr><td></td><td>@inv2 v ∉ f[1..r-1]</td></tr><tr><td>invariants</td><td>variant n - r</td></tr><tr><td>@inv1 r ∈ N</td><td></td></tr><tr><td>event initialisation</td><td>event initialisation</td></tr><tr><td>then</td><td>then</td></tr><tr><td>@act1 r :∈ N</td><td>@act1 r := 1</td></tr><tr><td>end</td><td>end</td></tr><tr><td>event final</td><td>event final</td></tr><tr><td>where</td><td>refines final</td></tr><tr><td>@grd1 r ∈ 1..n</td><td>where</td></tr><tr><td>@grd2 f(r) = v</td><td>@grd1 f(r) = v</td></tr><tr><td>end</td><td>end</td></tr><tr><td>anticipated</td><td>convergent</td></tr><tr><td>event progress</td><td>event progress</td></tr><tr><td>then</td><td>refines progress</td></tr><tr><td>@act1 r :∈ N</td><td>where</td></tr><tr><td>end</td><td>@grd1 f(r) ≠ v</td></tr><tr><td></td><td>then</td></tr><tr><td></td><td>@act1 r := r+1</td></tr><tr><td></td><td>end</td></tr></table>

self. context to the machine context. Similar to BContext, BMachine and BMachine-Refines use getters and setters to access and modify dictionaries.

## 3.1 Proof obligations

pyeb generates proof obligations for contexts, machines, machine refinements, events, and event refinements, following Event-B's semantics for proof-obligation generation [17]. Table 1 presents a summary of these proof obligations and describes which components are involved. The first column gives the name of the proof obligation, the second column gives a small description, and the third column shows the components related to the proof obligation.

<table><caption>**Table 1** Proof obligations</caption><thead><tr><td>po</td><td>desc</td><td>comp</td></tr></thead><tbody><tr><td>Th</td><td>theorem</td><td>context</td></tr><tr><td>Inv</td><td>invariant preservation</td><td>machine</td></tr><tr><td>Init</td><td>initialisation</td><td>machine</td></tr><tr><td>Fis</td><td>feasibility</td><td>machine</td></tr><tr><td>Grd</td><td>guard strengthening</td><td>machine ref.</td></tr><tr><td>Sim</td><td>before-after pred. simulation</td><td>machine ref.</td></tr><tr><td>Var</td><td>variant decreasing</td><td>machine</td></tr><tr><td>WFis</td><td>witness feasibility</td><td>machine ref.</td></tr></tbody></table>

The first row presents the Th proof obligation, which is generated in the definition of a context, and which depends on the axioms and other theorems included in that context. The invariant preservation proof obligation is defined for the execution of an event, therefore, the event actions must set machine variables with values that do not break the machine invariants. In particular, the **initialisation** event must provide machine variables with initial values for which the machine invariants hold (Init).

The feasibility proof obligation (Fis) is defined for the event actions; therefore, every non-deterministic assignment must be feasible; in other words, there must exist a valuation (a set of machine variables) that makes the before-after predicate used in the definition of the action true.

Through refinement, a machine can either i.) strengthen the event guards, ii.) add new ones, iii.) add more actions to some of the machine events, or iv.) add more events to the machine. Guard strengthening proof obligations (Grd) are generated for i.) and ii.). They ensure that the guard of a concrete event is stronger than the guard of an abstract event. Simulation proof obligations (Sim) ensure that the action of a concrete event simulates the action of the respective abstract event; in other words, the before-after predicate of the concrete event cannot contradict the before-after predicate of the abstract event.

There is no requirement for Event-B models to terminate and, in fact, most Event-B models run forever. However, we can use machine variants and convergent events to force Event-B models to terminate. An event status can be **ordinary**, **convergent**, or **anticipated**. A machine **variant** can be a natural number expression or a finite set expression. A numeric **variant** must be decreased by every **convergent** event, and a set
**variant** must be strictly included in its previous value by all **convergent** events. Hence, the variant decreasing proof obligation (Var) ensures that every convergent event decreases the machine variant. **anticipated** events become **convergent** in a machine refinement. Hence, whereas for each **convergent** event a proof obligation is generated that states that the event decreases the machine **variant**, for each **anticipated** event a similar proof obligation is generated, but for any refinement event. `pyeb` supports numerical variants, but does not support set variants.

Refinement events can include witness predicates for disappearing variables. A disappearing variable is a variable that is in *x* but not in *y* in Figure 1. For example, a refinement (concrete) event can include a **with** *a*: *P*(*a*) witness clause for a disappearing variable *a* and a predicate *P*. The witness feasibility proof obligation (WFis) ensures that the predicate *P* is feasible, that is, there exist appropriate parameters that make *P* true<fnref n="1" />.

**Guard strengthening Python encoding.** The following excerpt shows the guard strengthening proof obligation (Grd) in Python, which follows Abrial's definition of guard strengthening in [9, 17]. Function evt_grd_GRD is parametrised by the name of the concrete event (a dictionary key). This function is part of BMachineRefines, the concrete class machine, which keeps a reference to the abstract machine as self.abs_machine. This abstract machine can then access all the abstract events, and abstract invariants and theorems. As per the guard strengthening proof obligation, the function evt_grd_GRD returns a logical implication, therefore, the abstract event guard is implied from the concrete guard plus axioms, invariants and theorems.

```python
def evt_grd_GRD(self, conc_key):
    # abstract and concrete events
    m = self abs_machine
    abs_key = self ref_chain[conc_key]
    abs_event = m.get_event(abs_key)
    conc_event = self.events[conc_key]

    # abstract and concrete guards
    abs-guard = abs_event.get_guards()
```

```python
conc-guard = conc_event.get_guards()

# axioms and theorems
axioms = self.get_context().
        get-axioms()
theorems = self.get_context().
        get-theorems()
A = And(axioms, theorems)

# abstract invariants and theorems
abs-invariants = m.get_invariants()
abs-theorems = m.get_theorems()
I = And(abs-invariants, abs-theorems)

# concrete axioms and theorems
conc-invariants = self.get_invariants()
conc-theorems = self.get_theorems()
J = And(conc-invariants, conc-theorems)

# witness predicate
W = self.events[conc_key].
        get-witnesses()
# machine constants
C = self.get_context().getConstants()

# proof obligation
po = Implies(And(A, I, J, C, conc-guard, W),
              abs-guard)
return po
```

**Discussion.** Apart from the proof obligations in Table 1, the Rodin platform generates well-definedness proof obligations. These proof obligations intend to detect ill-formed (theorems, axioms, functions, events, etc.) definitions for which unprovable proof obligations are generated. `pyeb` does not generate well-defined proof obligations; instead, it relies on the Z3's type system to detect ill-formed formulae. Should `pyeb` not rely on the Z3's type system, it would need to implement a bespoke syntax checker or parser.

**Discussion.** Z3 does not provide native support for several of the operators available in Event-B; for example, domain and range subtraction, domain and range restriction, and function overriding; which was the main reason we did not carry out the modelling and verification of the sorting algorithm and the algorithm to find the minimum element of an array. As an alternative, one can model these operators (or the predicate calculus of event Event-B) in the language of the solver or using another language, as we did with Yices [18].

<footnote n="1">¹In general, *P* depends on several parameters other than *a* such as machine variables, sets, and constants.</footnote>
# 4 Tool Usage

PyPI [7] is a repository for the Python language which users can use to publish Python libraries, made available to the entire community of Python users. pyeb is a PyPI library implementation. pyeb is installed with pip [8] via the python3 -m pip install-pyeb command line. This line further installs the z3-solver,anicl4-python3-runtime and  antlr4-tools, which are required packages. pyeb requires the first package to discharge the proof obligations automatically (see Section 3.1), and the remaining two packages to translate Python programs into a sequence of interactions the Z3 SMT solver then discharges.

pyeb's source code is hosted at GitHub, reachable from https://github.com/ncatanoc/pyeb; the GitHub site includes a sample folder with the Python algorithm files from the experimental evaluation presented in Section 5. The Event-B models [9] were manually translated into Python to evaluate pyeb's verification capabilities.

For example, you can run the Python model of the search algorithm by either typing pyeb -sample/search oo.py or by running pyeb as a module or package via python3 -m pyeb sample/search oo.py. Either command line creates a search oo obj.py object Python file that includes a sequence of object creation instructions and calls to the Z3 SMT solver.

## 4.1 Object sequence

pyeb translates Python models into a sequence of object creation and method calls that are then loaded and executed in Python. We show below an excerpt of the context definition for the search algorithm (Section 5). The context class is called Context and the declaration of the sole axiom is prefixed with axiom.

class Context:
    def __init__(self):
        self.f = Function('f', IntSort(), IntSort())
        self.n = Const('n', IntSort())
        self.v = Const('v', IntSort())

    def axiom Rolling (self):
        return (self.n>=1)

The context class is translated into the object-creation sequence below. Thus, an object obj0 is created of type BContext, and additional objects are created for the fields of class Context, e.g. object obj0.f is created of type Function, and objects obj0.n and obj0.v are created for respective constant definitions. Then, method add constant is called upon object obj0 to add each constant. Finally, the axiom declaration is wrapped into an obj0 axiom axm0 object upon which method add axiom is called with the appropriate parameters.

obj0=BContext()
obj0.f=Function('obj0_f', IntSort(), IntSort())
obj0.add constant('obj0_f', obj0.f)
obj0.n=Const('obj0_n', IntSort())
obj0.add constant('obj0_n', obj0.n)
obj0.v=Const('obj0_v', IntSort())
obj0.add constant('obj0_v', obj0.v)
obj0 axiom axm0=(obj0_n>=1)
obj0.add axiom('obj0 axiom axm0',
obj0 axiom axm0)

Beyond static verification, pyeb enables developers to incorporate formal proofs into real-world development workflows through Pytest. This integration allows for seamless validation of correctness properties alongside standard Python tests (see Section 5.1).

## 4.2 Tool interaction

We show an excerpt of the output the pyeb tool produced on the search algorithm. The tool issues sat or unsat on each proof obligation, depending on whether it is satisfiable or not. pyeb takes reported messages and errors reported directly from Z3 and prints them on the screen.

--- Machine Search ref0 ---
sat: machine invariants hold
sat: non-determ. actions are feasible
sat: theorems hold
--- Machine Search ref1 ---
sat: initialisation event
sat: machine invariants hold
sat: non-determin. actions are feasible
sat: theorems hold
sat: event guards strengthening
sat: event guards simulation
sat: machine variants
sat: event witnesses are feasible
pyeb analyses all the machine declarations, starting from the most abstract and finishing with the most concrete. Some proof obligations only exist in the context of a refinement machine and not for the most abstract machine, e.g. checking that a concrete event guard is stronger than the respective abstract event guard makes sense for machine refinements only.

# 5 Case Study

For our experimental evaluation of the pyeb tool, we took various Event-B models for sequential algorithms, manually wrote Python programs for them, and finally used the tool to verify them. The Event-B models are written by J.-R. Abrial, and are available from https://web-archive.southampton.ac.uk/deploy-eprints.ecs.soton.ac.uk/122/ as Rodin projects. They can be imported using the Rodin IDE [4]. We used Rodin version 3.5.

pyeb takes a Python program as input and generates various types of proof obligations as described in Section 3.1. pyeb then discharges each proof obligation or shows an error with the information of the proof obligation that is unprovable. This error information is a replica of the error information provided by the Z3 SMT solver. Z3 was able to discharge the proof obligations generated for the Python models of the algorithms automatically or was able to detect the errors in early versions of the Python models, which we used to evolve and correct the models.

## Event-B models of sequential programs.
Jean-Raymond Abrial's paper [9] describes an approach for designing and building sequential programs in Event-B, therefore, programs are represented as Hoare triples [19] composed of a program precondition, the program itself, and a program postcondition. In this approach, the program input is the set of constants defined in the machine context, the program precondition is the set of axioms defined on those constants, the program postcondition is the guard of a unique final event defined in the last refinement machine, and the program outputs are (the values of) the machine variables.

Software development with Event-B is a three-stage process. Abstract events are written during the specification phase, event refinements are made during the design phase, and a final unique

event (program) is calculated during the *merging* phase. The two former phases are strongly related to pyeb. The latter phase relates to the generation or synthesis of code [20], which pyeb does not yet support. Next, we discuss the algorithms used in our case study as per the modelling and verification of sequential programs.

## Binary search.
According to its program precondition, the Event-B model includes a total function *f* that models a vector of natural numbers, a positive constant *n* modelling the size of *f*, and a value *v* the algorithm searches for in *f*. The vector *f* is sorted. According to its post-condition, the algorithm finds the position *r* at which the value *v* is. According to the algorithm design phase, the refinement machines include indices *p* and *q*, which hold the first and the last positions of the subarray of *f* over which the algorithm continues to search *v*. The pivot index *r* is set halfway between *p* and *q*. If *v* is greater than *f*(*r*), then the algorithm searches *v* to the right of *r*; otherwise, if the value is less than *f*(*r*), then the search continues to the left of *r*. Following Abrial's approach to modelling sequential algorithms, the Event-B model includes a *final* event whose guard is *f*(*r*) = *v*.

We show below *ref_event_final*, the Python version of the final event; it is side-effects free, hence, we encode the event actions as the *skip* statement, which is parametrised by the machine variables. The event guard models the stop condition.

```python
def ref_event_final(self):
    guard = {'grdl': self.Context.f(self.r)
             == self.Context.v}
    ba = skip({self.p, self.q, self.r})
    final = BEventRef('final',
                      super().ref_event_final())
    final.set_status(status.Ordinary)
    final.add guards(guard)
    final.add_bassg(ba)
    return final
```

## Minimum.
According to the program precondition, the Event-B model includes a total function *f* that models a vector of natural numbers and a constant *n* representing the number of elements of *f*. Regarding its post-condition, the algorithm calculates the minimum element *m* through an exhaustive search over vector *f*. According to the
algorithm design phase, the refinement machines declare indices *p* and *q*, whose initial values are 1 and *n*, respectively. It declares two events. An event searches from left to right, increasing the index *p*, and a second event searches from right to left, decreasing the index.

We show below the Python implementation of the *final* event. As stated by the event guard, the algorithm for the minimum element stops when *p* = *q*.

```python
def ref_event_mini(self):
    guard = {'grdl': (self.p == self.q)}
    ba = BAssignment({self.m, self.p, self.q},
        And(prime(self.m) == self(context.f(
            self.p),
            prime(self.p) == self.p,
            prime(self.q) == self.q))
    mini = BEventRef('mini',
        super().event_mini())
    mini.set_status(status.Ordinary)
    mini.add_guards(guard)
    mini.add_bassg(ba)
    return mini
```

### Reversing.
According to its precondition, the Event-B model declares a total function *f* whose size is a positive constant *n*. As per its postcondition, the algorithm calculates a relation *g* with the same elements as *f* yet organised in reverse order. According to the algorithm design phase, the model includes two indexes, *i* and *j*, with initial values 1 and *n*, respectively. A refinement event progresses by increasing *i* and decreasing *j*. The final event stops (its guard is) when *j* ≤ *i*. The main reason we did not include the reversing algorithm in our experimental evaluation is that the event that progresses also uses some domain subtraction operations (which are typical of Event-B) that *pyeb* does not support.

### Search.
Regarding its precondition, the Event-B model introduces a function *f* modelling a vector of natural numbers, a positive constant *n* modelling the size of *f*, and a value *v* the algorithm searches for in *f*. The algorithm does not require *f* to be sorted. According to its post-condition, the algorithm finds the vector index *r* at which the value *v* is. Regarding the algorithm design phase, the sole machine refinement constrains *r* to be between 1 and *n*, and *f* to contain *v*. The algorithm progresses by giving *r* an initial value of 1

and increasing *r* by 1 each time that *f*(*r*) is different than *v*. The refinement machine includes a *final* event whose guard is *f*(*r*) = *v*, for which the final result is *r*.

### Sorting.
According to its precondition, the Event-B model declares a total injective function *f*, and a constant *n* modelling its size. According to its post-condition, the algorithm calculates a relation *g* whose domain is sorted and has the same elements as *f*. The reason for not including the sorting algorithm in our experimental evaluation is similar to that for not including the reversing algorithm (discussed above).

### Square root.
As per its precondition, the model includes a non-negative integer constant *n* whose square root is to be calculated. As per its postcondition, the algorithm finds a non-negative integer variable *r* such that *r* × *r* is less than or equal to *n*, but *n* is less than (*r* + 1) × (*r* + 1). Hence, *r* is the integer square root of *n*.

We show below the Python encoding of the final event of the first refinement machine. The algorithm stops (see the event guard) when *r* reaches a value such that *n* is between *r* × *r* and (*r* + 1) × (*r* + 1). The event is side-effect-free: the event body is encoded as the *skip* statement.

```python
def event_final(self):
    guard = {'grdl': And(self.r*self.r <=
        self(context.n,
        self(context.n <
            (self.r+1) * (self.r+1)))}
    ba = skip({self.r})
    return BEvent('final',
        Status.Ordinary, [], guard, ba)
```

### Inverse.
As per its precondition, the model includes an integer constant *n*, and a total function *f* that is strictly increasing, hence injective. *f* is an integer-valued function. There exist two values *a* and *b* that bound the inverse value of *n* through *f* such that *f*(*a*) ≤ *f*(*n*) < *f*(*b* + 1). Regarding its post-condition, the algorithm calculates a value *r* such that *r* is the inverse value of *n* throughout the function *f*. Regarding the algorithm design phase, the machine refinement progresses by increasing *r* and decreasing *q*. The algorithm stops when *r* and *q* are equal.

We show below the Python implementation of the final event. The event stops when *r* = *q*.
```python
def ref_event_final(self):
    guard = {'grdl': (self.r == self.q)}
    ba = skip({self.r, self.q})
    final = BEventRef('final',
                      super().event_final())
    final.set_status.Status.Ordinary)
    final.add_guards(guard)
    final.add_bassg(ba)
    return final
```

Table 2 shows some statistics related to the size and structure of the algorithms. The table has five columns: the name of the algorithm, whether or not it has been included in our experimental evaluation, the number of Event-B machines of the algorithm, the type of algorithm - array, pointer or numerical, and the number of lines of code of the respective Python model that we have written.

The Python versions of these algorithms are accessible from https://github.com/ncatanoc/pyeb/tree/main/sample. The main site includes instructions on how to install pyeb using PyPI and how to access the code and examples of the case study.

<table><caption>Table 2 Sequential models</caption><thead><tr><td>model</td><td>pyeb</td><td># m.</td><td>type</td><td># loc</td></tr></thead><tbody><tr><td>binary search</td><td>Yes</td><td>3</td><td>array</td><td>180</td></tr><tr><td>minimum</td><td>Yes</td><td>2</td><td>array</td><td>115</td></tr><tr><td>reversing</td><td>No</td><td>2</td><td>pointer</td><td>n/a</td></tr><tr><td>search</td><td>Yes</td><td>2</td><td>array</td><td>99</td></tr><tr><td>sorting</td><td>No</td><td>3</td><td>array</td><td>n/a</td></tr><tr><td>square root</td><td>Yes</td><td>3</td><td>numerical</td><td>121</td></tr><tr><td>inverse</td><td>Yes</td><td>2</td><td>array</td><td>138</td></tr></tbody></table>

The number of proof obligations generated by `pyeb` is less than the number of proof obligations generated by the Rodin IDE, in general. Whereas Rodin allows the use of deterministic assignments, `pyeb` forces users to encode all the deterministic assignments as a sole non-deterministic assignment.

## 5.1 Testing with PyTest

`pyeb` is seamlessly integrated with `Pytest` [10], a Python testing framework. `Pytest` allows users to automatically inspect the generated proof obligations, which would otherwise be manually inspected, which is inefficient. Integrating `pyeb`

with `Pytest` not only streamlines verification but also embeds formal proofs into real-world software development cycles. Developers can run correctness checks alongside conventional unit tests, ensuring continuous assurance of model validity. `Pytest` also enables continuous integration for verifying proof-obligations, ensuring correctness across software updates.

We have written `Pytest` files for each of the Python algorithms discussed in Section 5. The `Pytest` files can be reached from https://github.com/ncatanoc/pyeb/tree/main/tests. Each file tests the proof obligations discussed in Section 3.1. For example, the command `pytest tests/-test_search.py` tests all the proof obligations of the search algorithm in Table 1.

Next, we show the test for the SIM proof obligation. The test initially adds the negation of the proof obligation `po` to the solver and then uses Z3 to verify its satisfiability.

```python
def test_evts_act SIM():
    po = __machine__.evts_act SIM()
    s = Solver()
    s.add(Not(po))
    if s.check() == sat:
        print("unsat:...")
        print(s.model())
    else:
        print("sat:")
```

## 5.2 The search algorithm

Next, we discuss the object-oriented syntax and format that Python classes should follow. A machine context should be declared as a Python class, and its constructor should initialise constants and functions the usual way in Python, i.e., using the `self` object syntax. Class constants and functions should be encoded as Z3 constants and functions. Axioms and theorems should be encoded as Python functions that return their predicate encodings. These predicates are Z3 predicates. The names of all these functions should be prefixed with `axiom_` and `theorem_`, respectively. An abstract machine should be declared as a Python class whose constructor is parametrised by a context class object. A concrete machine should also be a Python class, but the constructor is further parametrised by a reference to the abstract machine. Events are declared
within Python classes for abstract and concrete machines. Events are functions whose names are prefixed with `event_` and invariants with `invariant_`. Events in a refinement machine should be prefixed with `ref_event_`.

In the following, we show the Python encoding of the search algorithm in Figure 2². The class `Context` includes the declaration of constants, axioms, and theorems. Class `Context` declares class fields `self.f`, `self.n`, and `self.v` similar to the declarations at the beginning of Section 3. Event-B axioms are defined as functions in Python. The Python encoding below shows the first axiom of the Event-B model; therefore, every element in `self.f` is non-negative. The axiom itself is returned by the function.

```python
def axiom_axml(self):
    x = Int('x')
    return ForAll(x,
        Implies(And(x>=1, x<=self.n),
                self.f(x)>=0))

axiom
```

Likewise, theorems are Python functions that return the actual encoding of the theorems. They are also defined in class `Context`. Additionally, as explained in Section 3.1, theorems generate proof obligations that we should have proven from the axioms defined in class `Context`.

```python
def theorem_thml(self):
    return (self.n>0)

theorem
```

Class `MachineRef0` is the abstract machine that encodes the left part in Figure 2. Its class constructor `__init__` sets initial values for the index `self.r` and the machine context. Hence, the machine context is referred from `Machine Search Ref 0`.

```python
def __init__(self, context):
    self.r = Int('r')
    self.Context = context
```

```python
__init__
```

The events of the abstract machine are introduced as Python functions. In the following, we show the encoding of the event `event_progress`, the abstract version of the event `progress`. The event guard is the empty dictionary. This means that the event is always enabled. The event non-deterministically assigns a non-negative value to index `self.r`. The event is refined by `ref_event_progress` (shown in Section 3), which is part of the `Machine-Search_ref1` refinement machine. The event `event_progress` is an **anticipated** event, therefore, the event `ref_event_progress` is a **convergent** event.

```python
def event_progress(self):
    guard = {}
    ba = BAssignment({self.r},
        prime(self.r) >= 0)
    return BEvent('progress',
        Status.Anticipated,
        [], guard, ba)

anticipated
```

The class `Machine Search Ref1` implements the first machine refinement of the search algorithm. The class constructor initialises the context and the abstract machine. It also sets the machine variant to `(self.n - self.r)`.

```python
def __init__(self, abs_machine, context):
    super().__init__(abs_machine.Context)
    self.Context = Context
    self abstract_machine = abs_machine
    selfContext = self.Context.n - self.r
    self variant = self.Context.n - self.r
    __init__
```

Event-B machines have a distinguishable event, the **initialisation** event, which initialises machine variables. The refinement machine initialises `self.r` to 1. The event guard is the empty dictionary. This reflects the fact that machine variables are always initialised.

<footnote n="2">²Figure 2 does not show the machine context.</footnote>
```python
def ref_event_initialize(self):
    guard = {}
    ba = BAssignment({self.r},
                      prime(self.p) == 1)
    init = BEventRef('initialisation',
                     super().event_initialize())
    init.set_status(status.Ordinary)
    init.add_guards(guard)
    init.add_bassg(ba)
    return init

initialisation
```

Machine invariants are encoded as Python functions that return their function encoding. Invariants restrict the set of values that machine variables can take. In addition to this, next-state (variable) values calculated by events must comply with these invariants. This is also true for the initialisation event: initial values for machine variables must conform to the machine invariants.

We show below the encoding of the two machine invariants in the refinement machine in Figure 2 (right side). The first invariant states that the index *r* must be between 1 and *n*. The second invariant tells us that either we have found the value *v* we are looking for or that the value is in the remaining part of the array for which we have not searched.

```python
def invariant_inv1(self):
    return And(self.r >= 1, self.r <=
               self.Context.n)

def invariant_inv2(self):
    x = Int('x')
    po = ForAll(x, Implies(
                  And(x>=1, x <= (self.r-1)),
                  self.Context.f(x) !=
                  self.Context.v))
    return po

invariant
```

Event `ref_event_final` encodes the case when the algorithm finds the value `self.con-text.v` at index `self.r`, in which case the algorithm executes the `skip` statement, which ensures that the event does not modify the state since the algorithm has already terminated.

```python
def ref_event_final(self):
    guard = {'g': self.Context.f(self.r)
              ==
              self.Context.v}
    ba = skip({self.r})
    final = BEventRef('final',
                      super().event_final())
    final.set_status(status.Ordinary)
    final.add_guards(guard)
    final.add_bassg(ba)
    return final

final
```

# 6 Related Work

The authors in [21] propose the translation of Event-B models into Python. This translation is implemented as a Rodin plugin that generates a design-by-contract Python program that uses `assert` and `raise` statements to verify generated contracts at runtime. We plan to extend `pyeb` to generate Python and Rust code but *outside* the Rodin IDE box. The website [22] includes a large list of data structures and algorithms in Python. We will use these Python implementations as a testbed for our work on code generation.

Data groups have been studied for a long time [23]. They convey information on the modifiable state of objects. Not surprisingly, in checking the specifications of the algorithms presented in Section 5, we needed to define a `skip` statement for which the values of machine variables do not change from pre- to post-state. An alternative would have been not to state anything, but then that would amount to stating that each machine variable can take any value in the post-state, which is not what we wanted. Data groups and frame conditions fit nicely in the context of design-by-contract [16]. This fact may suggest a path for `pyeb` to interact with design-by-contract verification techniques.

The authors in [24] describe the program verifier Dafny's SMT encoding of (recursive) functions. As Z3 does not provide native support for all the plethora of sets and relations operators that Event-B supports, we will investigate the ways in which `pyeb` can fully provide support for those operators. As an alternative, in previous work [18], we implemented a Yices library that included most of Event-B's set and relational
operators, including domain subtraction, domain
restriction, function overriding, etc. We plan to
either hook pyeb into the existing Yices library
implementation or port the library directly to Z3's
language.

The authors in [25] propose a joint machine
learning and Event-B methodology to automati-
cally repair faulty Event-B models, for example,
models that include deadlocked states or events
that break machine invariants. Although our work
with pyeb strives to check the soundness of a
model, a complementary and related aspect is to
repair unsound models, for which machine learn-
ing and program repair techniques seem promising
to us.

In [26], the author proposes a mechanism to
reuse, combine, and compose Event-B specifica-
tions in the context of large complex systems, e.g.
in distributed systems. It is not only a mechanism
used for the composition of specifications, but also
for proof obligations. We could incorporate this
extension into pyeb.

Event-B specifications are descriptions of
abstract systems that are refined until a close-to-
implementation specification is reached. However,
the Event-B language lacks an explicit control
structure for ordering events so that the final
design phase that goes into producing a program is
accomplished. In [27], authors propose a schedul-
ing language to derive algorithm control structures
in Event-B. This is also replicated and summarised
in [9]. We plan to incorporate a similar schedul-
ing mechanism in pyeb. In fact, the Event-B
algorithms that are introduced and discussed in
Section 5 are in a ready-to-code-generate form.

We next survey on program analysis tools for
the Python language. mypy [28] is a static type
checker for Python that checks if program vari-
ables and functions are used with the right type. It
issues a warning in case they are not. pylint [29]
is a static Python tool that looks for code smells
and makes suggestions on code refactoring and
good programming practices. pyflakes [30] is
a light version of pylint; it is simpler, faster,
and does not compile the source program. These
3 Python static checkers are PyPI library imple-
mentations [7]. Our pyeb tool is not a Python
analyser, but rather allows programmers to write
mathematical models in Python of programs that
can eventually be implemented in Python or any
other programming language. pyeb could use type

annotations and compile-time type checking to
assist a (hypothetical) code generation process,
but this is still future work.

Other static analysers for Python are Pros-
pector [31], built on top of pylint, and py-
flakes, which can suppress spurious warnings;
also, the Bandit tool [32], a tool designed to
find common security issues in Python programs
from their AST (Abstract Syntax Trees) represen-
tations.

The Nagini [33] tool is an automatic ver-
ifier for statically typed Python programs. Na-
gini builds on top of Viper. Nagini verifies
memory safety, termination, absence of deadlocks,
and functional properties of Python programs.
Nagini translates a Python program and its
specifications into the Viper language [34], for
which automated verifiers already exist. Nagini
requires input programs to adhere to the PEP 484
standard syntax for type annotations, which also
the mypy tool implements.

PyModelChecking [35, 36] is a model
checker of Python programs. It is implemented as
a PyPI library. It takes a Python program and
transforms it into a Kripke structure, which is
then model-checked with Maude [37]. PyModel-
Checking supports LTL and CTL temporal log-
ics. Also, Pytest [10] is a PyPI library that
performs Python program testing. It originates
from the PyPy program [38]. Our pyeb tool sup-
ports testing with Pytest (see Section 5.1). More
concretely, one can either use pyeb to check
the refinement proof obligations of mathematical
models of programs written in Python, or one can
use Pytest to unit test the correctness of those
proof obligations.

7 Conclusion

Despite previous and current efforts to make soft-
ware applications (more) reliable, there are still
challenges that must be overcome, for which for-
mal methods can give a satisfactory answer. This
paper presented the pyeb tool, a Python imple-
mentation of the Event-B refinement calculus. The
tool allows users to work with a familiar syn-
tax, object-oriented Python, which allows them
to abstract away from most of the mathemat-
ical formalisms. The pyeb tool is implemented
as a pip library, available for all platforms.
pyeb supports Event-B's syntax, including the
definition and use of events, contexts, machines, machine refinements, machine variants and invariants, and witness clauses. Variants are used to enforce termination. Our idea of generating proof obligations for Event-B originated from previous work in which we designed and implemented a Rodin plugin that generates Event-B proof obligations in Dafny [39]. In contrast, pyeb generates proof obligations outside the Rodin platform more completely and independently.

We presented a case study in which we have modelled several sequential algorithms in Python (manually) from some existing Event-B versions. The case study showed that pyeb was able to deal with special Event-B constructs such as non-deterministic assignments, witness clauses, and machine variants, which are at the core of formal software development with Event-B. We plan to conduct a larger case study that would involve the modelling and analysis of a whole system.

Our work with pyeb is part of a long-term work in which we plan to implement a Correct-by-Construction [40, 41] (CbC) framework to generate Python and Rust certified code from Event-B models written as Python programs. The Python programs would follow the syntax described in this paper. This CbC work will be based on previous work on program synthesis for Event-B and the Java programming language presented in [20, 42]. As Event-B models are models of reactive systems, challenges for this program synthesis work would be related to the code generation of high-performance implementations that would synchronise correctly.

We also plan to extend pyeb supported syntax for users to write and verify LTL [43] (Linear Temporal Logic) invariant properties in Python. Temporal logic allows one to model safety ("something bad does not occur") or liveness ("something good will eventually happen") security requirements. Verifying liveness properties in the context of a design-by-contract specification language has already been studied elsewhere [44].

Finally, with Python's widespread and popularity and its large number of libraries, from numerical analysis libraries such as NumPy to statical analysis libraries such as SciPy or Pandas, we expect pyeb to contribute to our long-term goal of making refinement-calculus-based formal methods more popular. pyeb reduces the cognitive entry barrier to formal methods, making

refinement calculus more accessible to standard software developers unfamiliar with mathematical formalisms. pyeb provides a light formal methods solution that integrate seamlessly with modern programming languages like Python and with modern software development techniques and methodologies.

As future work, we plan to extend pyeb to generate Python and Rust code. We will first focus on implementing Abrial's rules while and if for sequential algorithms [9]. As Z3 does not provide native support for all the plethora of sets and relation operators the Event-B language ships, we will investigate ways pyeb can fully provide support for those operators. As an alternative, in previous work [18], we implemented a Yices library that included most of Event-B's set and relational operators, including domain-subtraction, domain-restriction, function-overriding, etc. We plan to either hook pyeb into the existing Yices library implementation or port the library directly to Z3's language.

## References

[1] Back, R.J.R.: On correct refinement of programs. Journal of Computer and System Sciences 23(1), 49-68 (1981)

[2] Back, R.J.R.: Correctness Preserving Program Refinements: Proof Theory and Applications. Mathematical Centre Tracts, vol. 131. Mathematisch Centrum, Science Park 123, 1098 XG Amsterdam, Netherlands (1980). https://books.google.com.co/books?id=vQTvAAAAMAAJ

[3] Back, R.-J., Sere, K.: Stepwise Refinement of Action Systems. Structured Programming 12, 17-30 (1991)

[4] Abrial, J.-R., Butler, M., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: An Open Toolset for Modelling and Reasoning in Event-B. International Journal on Software Tools for Technology Transfer 12(6), 447-466 (2010)

[5] The AtelierB Tool. https://www.atelierb.eu/en/atelier-b-tools/
[6] Abrial, J.-R.: Modeling in Event-B: System and Software Design. Cambridge University Press, New York, NY, USA (2010)

[7] PyPI: The Python Package Index. https://pypi.org/ (2024)

[8] pip: The Package Installer for Python. https://pypi.org/project/pip/ (2024)

[9] Abrial, J.-R.: Chapter 15: Sequential Program Development. https://wiki.event-b.org/index.php/Event-B_Language (2009)

[10] Krekel, H.: Pytest. https://docs.pytest.org/en/7.4.x/ (2024)

[11] Abrial, J.-R., Hallerstede, S.: Refinement, Decomposition and Instantiation of Discrete Models: Application to Event-B. Fundamentae Informatica 77(1,2), 1–24 (2007)

[12] Roever, W.P., Engelhardt, K.: Data Refinement: Model-oriented Proof Theories and Their Comparison. Cambridge Tracts in Theoretical Computer Science, vol. 46. Cambridge University Press, USA (1998)

[13] Moura, L.M., Bjørner, N.S.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29–April 6, 2008. Proceedings. Lecture Notes in Computer Science, vol. 4963, pp. 337–340. Springer, Berlin, Heidelberg (2008)

[14] The Z3 SMT Prover. https://github.com/Z3-Prover/z3 (2024)

[15] Leino, K.R.M., Poetzsch-Heffter, A., Zhou, Y.: Using Data Groups to Specify and Check Side Effects. In: Knoop, J., Hendren, L.J. (eds.) Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Berlin, Germany, June 17-19, 2002, pp. 246–257. ACM, Berlin, Germany (2002)

[16] Cataño, N., Huisman, M.: Chase: A Static Checker for JML’s Assignable Clause. In: Zuck, L.D., Attie, P.C., Cortesi, A., Mukhopadhyay, S. (eds.) Verification, Model Checking and Abstract Interpretation (VMCAI). Lecture Notes in Computer Science, vol. 2575, pp. 26–40. Springer, New York, NY, USA (2003)

[17] Abrial, J.-R.: Summary of Proof Obligations for Event-B. https://web.archive.southampton.ac.uk/deploy-e-prints.ecs.soton.ac.uk/234/19/po-slides.pdf (2010)

[18] Cataño, N., Rueda, C., Hanvey, S.: Verification of JML Generic Types with Yices. In: Proceedings of 6th Colombian Congress of Computing (6CCC). IEEE Xplore Digital Library, pp. 1–6, Manizales, Colombia (2011)

[19] Hoare, T.: An Axiomatic Basis for Computer Programming. Communications of the ACM 12(10), 576–580 (1969)

[20] Rivera, V., Cataño, N., Wahls, T., Rueda, C.: Code Generation for Event-B. International Journal On Software Tools For Technology Transfer 19(1), 31–52 (2017)

[21] Barona, J.F.E., Rocha, C.: Traduccion Automatica a Python de Modelos Correctos de Event-B en la Plataforma Rodin. Master’s thesis, Pontificia Universidad Javeriana (2020)

[22] Keon: Pythonic Data Structures and Algorithms. https://github.com/keon/algorithms (2024)

[23] Leino, K.R.M.: Data Groups: Specifying the Modification of Extended State. In: Freeman-Benson, B.N., Chambers, C. (eds.) Proceedings of the 1998 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages & Applications, OOPSLA 1998, Vancouver, British Columbia, Canada, October 18-22, 1998, pp. 144–153. ACM, British Columbia, Canada (1998)

[24] Amin, N., Leino, K.R.M., Rompf, T.: Computing with an SMT Solver. In: Seidl, M.,
Tillmann, N. (eds.) Tests and Proofs, pp. 20–35. Springer, Cham (2014)

[25] Cai, C., Sun, J., Dobbie, G.: Automatic B-model Repair Using Model Checking and Machine Learning. Automated Software Engineering **26**(3), 653–704 (2019)

[26] Silva, R.: Towards the Composition of Specifications in Event-B. In: Potet, M., Treharne, H. (eds.) Proceedings of the B 2011 Workshop, a Satellite Event of the 17th International Symposium on Formal Methods, FM 2011, Limerick, Ireland, June 21, 2011. Electronic Notes in Theoretical Computer Science, vol. 280, pp. 81–93. Elsevier, Limerick, Ireland (2011)

[27] Dalvandi, M., Butler, M.J., Rezazadeh, A.: Derivation of Algorithmic Control Structures in Event-B Refinement. Science of Computing Programming **148**, 49–65 (2017)

[28] The mypy Static Tool. https://mypy-lang.org/ (2024)

[29] The Pylint Static Tool. https://pylint.org/ (2024)

[30] PyFlakes. https://pypi.org/project/pyflakes/ (2024)

[31] The Prospector Static Tool. https://prospector.landscape.io/en/master/ (2024)

[32] The Bandit Tool. https://github.com/PyCQA/bandit (2024)

[33] Eilers, M., Müller, P.: Nagini: A Static Verifier for Python. In: Chockler, H., Weisenbacher, G. (eds.) Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I. Lecture Notes in Computer Science, vol. 10981, pp. 596–603. Springer, Oxford, U.K. (2018)

[34] Müller, P., Schwerhoff, M., Summers, A.J.: Viper: A Verification Infrastructure for Permission-Based Reasoning. In: Pretschner, A., Peled, D., Hutzelmann, T. (eds.) Dependable Software Systems Engineering. NATO Science for Peace and Security Series - D: Information and Communication Security, vol. 50, pp. 104–125. IOS Press, Berlin, Heidelberg (2017)

[35] Rubio, R., Marti-Oliet, N., Pita, I., Verdejo, A.: PyModelChecking. https://github.com/albertocasagrande/pyModelChecking (2024)

[36] Rubio, R., Marti-Oliet, N., Pita, I., Verdejo, A.: Strategies, model checking and branching-time properties in Maude. Journal of Logical and Algebraic Methods in Programming **123**, 100700 (2021)

[37] Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.L.: The Maude 2.0 System. In: Nieuwenhuis, R. (ed.) Rewriting Techniques and Applications, 14th International Conference, RTA 2003, Valencia, Spain, June 9-11, 2003, Proceedings. Lecture Notes in Computer Science, vol. 2706, pp. 76–87. Springer, Valencia, Spain (2003)

[38] Krekel, H.: PyPy. https://pypy.org/ (2024)

[39] Cataño, N., Rivera, V., Leino, R.: The EventB2Dafny Rodin Plug-In. In: 2nd Workshop on Developing Tools as Plug-ins (TOPI), pp. 49–54. IEEE Xplore, Zurich, Switzerland (2012). https://doi.org/10.1109/TOPI.2012.6229810

[40] Beek, M.H., Hähnle, R., Schaefer, I.: Correctness-by-Construction and Post-hoc Verification: Friends or Foes? In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques - 7th International Symposium, ISOLA 2016, Imperial, Corfu, Greece, October 10-14, 2016, Proceedings, Part I. Lecture Notes in Computer Science, vol. 9952, pp. 723–729 (2016)

[41] Watson, B.W., Kourie, D.G., Schaefer, I., Cleophas, L.: Correctness-by-Construction and Post-hoc Verification: A Marriage of Convenience? In: Margaria, T., Steffen, B. (eds.) Leveraging Applications of Formal
Methods, Verification and Validation: Foundational Techniques - 7th International Symposium, ISoLA 2016, Imperial, Corfu, Greece, October 10-14, 2016, Proceedings, Part I, vol. 9952, pp. 730-748 (2016)

[42] Rivera, V., Cataño, N.: Translating Event-B to JML-Specified Java Programs. In: Proceedings of the 29th Annual ACM Symposium on Applied Computing (SAC-SVT). SAC 2014, pp. 1264-1271. ACM, New York, NY, USA (2014). https://doi.org/10.1145/

2554850.2554897

[43] Pnueli, A.: The Temporal Logic of Programs. In: Symposium on the Foundations of Computer Science (FOCS), pp. 46-57. IEEE Computer Society Press, Providence, Rhode Island, USA (1977)

[44] Giorgetti, A., Groslambert, J., Julliand, J., Kouchnarenko, O.: Verification of class live-ness properties with java modelling language. IET Software 2(6), 500-514 (2008)