Frequently Asked Questions
Last updated
Was this helpful?
Last updated
Was this helpful?
There is a MOOC on the B method, recorded by UFRN/ Natal, available here:
There is also a Youtube channel populated with some videos about how to use Atelier B:
The latest version is available at . It works for both Windows 10 and Windows 11.
Can you verify that the directory C:\Users\USER\AtelierB_Data\AtelierB_free_4.7.1\press\bdb
exists?
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.
Atelier B prover plugin has to be installed from Rodin (Eclipse software update) See or the install windows when opening Rodin for the first time.
The library machines are not provided anymore with Atelier B.
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.
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.
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.
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).