Although we have talked about the B Language, the language is in fact
split into two different but equivalent views - one fit for humans and
one fit for machines.

• Abstract Machine Notation (AMN)
  This is the language in which B specifications and B designs are
  actually written - a simple pseudo programming notation that is used
  at all levels of a B development.

• Generalised Substitution Language (GSL)
  The machine-readable equivalent of AMN; when a construct is first
  analysed by the B-Toolkit, a GSL version of the AMN is created and
  each of the subsequent tools in the toolkit use this latter form, since
  it lends itself more easily to automated processing.

Many people are familiar with the formal methods Z and
VDM and we here provide a comparison of the three methods:

• A Comparison of Z and VDM with B

Further information on both the B-Method and the B-Toolkit can
be obtained through browsing the toolkit's on-line documentation,
accessed through the Contents or Index Pages:

• BToolkit On-line Manual: Contents

• BToolkit On-line Manual: Index