# What is this plugin ?¶

An experimental front-end that parses a subset of Why3’s logic. More
precisely, this front-end targets proof obligations generated by the
Atelier-B framework in Why3 format. It should be used with a prelude
defining the B Set theory (currently provided in
`src/preludes/b-set-theory-prelude-2020-02-28.ae`

).

# What this plugin is not ?¶

This plugin mainly focuses on the shape of the proof obligations produced by the Why3 proofs obligations generator of Atelier-B. You will probably not be able to use it to parse/solve other formulas written in Why3’s logic.

# How to use it ?¶

Assuming you are currently in `alt-ergo-git/`

directory, you can run the command
`make AB-Why3`

to compile Alt-Ergo and the AB-why3 plugin. You can ask Alt-Ergo to
prove the goals given in a file `b-why3-POs.ae`

with the following
command:

```
./alt-ergo b-why3-POs.why --add-parser AB-Why3-plugin.cmxs --prelude src/preludes/b-set-theory-prelude-2020-02-28.ae
```

where `--add-parser AB-Why3-plugin.cmxs`

allows to load this plugin and
register the parser it contains, and `--prelude b-set-theory-prelude-2020-02-28.ae `

provides an axiomatization of the B Set
theory for Alt-Ergo.

For instance, using the following command to prove the goals in the
file `examples/AB-Why3-plugin/p4_34.why.zip`

:

```
./alt-ergo examples/AB-Why3-plugin/p4_34.why.zip --add-parser AB-Why3-plugin.cmxs --prelude src/preludes/b-set-theory-prelude-2020-02-28.ae --timelimit-per-goal --timelimit 3 --no-locs-in-answers
```

Alt-Ergo returns:

```
Warning: A parser for extension ".why" is already registered. It will be hidden !
Preprocessing (0.0315) (0 steps)
Valid (0.0033) (28 steps) (goal g_0)
Valid (0.0369) (163 steps) (goal g_1)
Valid (0.0087) (94 steps) (goal g_2)
Timeout (3.0016) (2191 steps) (goal g_3)
Valid (0.0476) (184 steps) (goal g_4)
Valid (0.0525) (215 steps) (goal g_5)
```

If you have already installed this version of Alt-Ergo and this plugin, you should be able to simply use the command:

```
alt-ergo b-why3-POs.why --add-parser AB-Why3-plugin.cmxs --prelude b-set-theory-prelude-2020-02-28.ae
```

# Licensing¶

The OCaml files in this directory come from Why3’s source code
(release 0.88.2 to be exact). We have quite modified them for our
needs. They are licensed under the terms of the GNU Lesser General
Public License version 2.1, as stated in
`src/plugins/AB-Why3/WHY3-LICENSE`

. The plugin `AB-Why3-plugin.cmxs`

resulting from their compilation is thus licensed under the same
terms.