it is impossible, for example, to have an implementation that does not
conform to B0 - all such aspects of the B-Method are automatically
checked

the refinement rules, which originate from The Programming Research
Group in Oxford University and J-R Abrial's formulation in terms of
Predicate Transformers, are used within the tool.

enabling the specification to be `run', validated and tested;
pre-conditions, guards for conditional statements, and the values of
local and state variables may be inspected during animation.