The B-Method uses a simple `pseudo' programming language to model
requirements, to specify interfaces, and to provide implementations
and intermediate designs. The language is know as AMN (The Abstract
Machine Notation).

AMN allows specifications to be statically type checked, dynamically
validated, and mathematically verified by proof to ensure the
correctness of the design process.

Step-wise development is used to reduce the complexity of large
developments into understandable components. A multi-layered
approach is achieved by allowing implementations to to be expressed
in terms of lower-level specifications. A complete development is
thus constructed from layers of specification/implementation pairs.

Specification/implementation pairs at the lowest levels are drawn from
an extensive library of pre-implemented re-usable components. A high
degree of reuse can be achieved by extending the library with new
components made from complete developments.

Implementations at all levels are translated into highly maintainable,
separately compilable source code (C) and executables.

Structuring mechanisms in AMN enforces information-hiding and data
encapsulation similar to those found in Object-Oriented approaches.
This allows the completely independent development of different
components of a large development, while enforcing rigorous control
of component interfaces.