Frequently Asked Questions

I'm looking for a material to learn B for free. Where can I find?

There is a MOOC on the B method, recorded by UFRN/ Natal, available here: https://mooc.imd.ufrn.br/course/the-b-method

There is also a Youtube channel populated with some videos about how to use Atelier B: https://www.youtube.com/@atelierbclearsy

What is the most stable version of ATELIER B to download for windows 10?

The latest version is available at https://www.atelierb.eu/en/atelier-b-support-maintenance/download-atelier-b/. It works for both Windows 10 and Windows 11.

I am having issues with Atelier B 4.7.1 running on Winwows 8. I get a message like "Error reading data from bbatch. Please check that the resource file exists and that you are using the correct bbatch version. Details: Details: Resource file: file or directory C:\Users\USER\AtelierB_Data\AtelierB_free_4.7.1\press\bdb does not exist or cannot be accessed"

Can you verify that the directory C:\Users\USER\AtelierB_Data\AtelierB_free_4.7.1\press\bdb exists?

I am having issues with Atelier B 4.7.1 running on my mac. I get a message like "The bbatch process could not be started. Check the prgram arguments (...)"

It seems that, for any reason, the Atelier B parameters stored in .config file are fuzzed. Our suggestion is to edit the file $HOME/.config with a text editor and to remove everything related to Atelier B.

I can't find the AtelierB Plugin with Rodin

Atelier B prover plugin has to be installed from Rodin (Eclipse software update) See https://sourceforge.net/p/rodin-b-sharp/mailman/message/32465997/ or the install windows when opening Rodin for the first time.

Where can I install library machines?

The library machines are not provided anymore with Atelier B.

I wonder if AtelierB is a tool for formal specification

B is used for both writing formal specification and formal implementation. Atelier B allows to prove both kinds of model and the correct refinement of the former by the latter.

Is Atelier B a compiler ?

Atelier B is not a compiler. It contains a C code generator which translates B models into C language. Then the C files need to be compiled with a compiler like gcc.

In the B language I did not understand the difference between PROPERTIES and INVARIANT. Can you explain it to me?

The PROPERTIES clause relates to constants, the INVARIANT clause relates to variables. For each, the type of the constant/variable (e.g. the variable is Boolean) and possible constraints (e.g. the sum of 2 integer constants is less than a certain value) are given.

I have the following issue when I use a structure in B language in the interactive prover: Goal: rec(Field1: TRUE): struct(Field1: BOOL). pp: starting Can't resolve set$5 = super(Field1$8888>>TRUE). Only "pr" is working fine.

Indeed the predicate prover is not able to handle records. Hence the kind of cryptic message. The main prover is able to handle records and to transform it into a conjunction of predicates that pp (or pr) could demonstrate. So the advice is to use mp or pr first on a goal involving records then discharge the resulting predicates with either mp, pr or pp (or any combination of resolving commands).