The B-Method when used with the B-Toolkit supports the teaching of
formal methods, software design, programming and sound practices of
software engineering.

It is a complete, rigorous programming environment, leading the
student from formal specification to running C code, with support for
proof work and design documentation along the way.

A major benefit of using B for teaching is that the activities of
formal specification, programming as well as proofs are carried out
in a single notational framework within a fully integrated
development environment.

The notation employed by the method helps to teach students what it
means to specify rather than to implement, by enforcing the use of
specification statements, based on the principles of pre- and
post-conditioning. Imperative constructs as known from High Level
Languages are reserved for refinements and implementations.

The structuring mechanisms support the principles of
data-encapsulation and full information-hiding, giving the opportunity
to teach the rationale behind an object-based approach.

The B-Animator allows students to experiment with their specifications
before they engage in proof or refinement work. It also helps teach
students to understand the discrete mathematics behind the models they
build.

Step-wise refinement is well supported by the layered design approach
intrinsic to the B-Method.

A library of basic abstract machines allows students to experience
rapid prototyping of specifications through reuse. Coupled with an
automated interface generator, the resulting programs can be run and
tested.

Many universities are now teaching B on their Masters Courses,
and an increasing number are beginning to teach B at undergraduate
level. The B-Toolkit is now widely regarded as the de-facto
standard tool for teaching mathematically-based methods of software
development at Universities and is currently used worldwide at over forty
universities. See University Testimonials for a selection of comments.

B-Core has recognized that capital expenditure budgets are tight in
most university departments and has accordingly made the toolkit
available on a yearly leasing scheme, which fits in more comfortably as
a revenue expenditure item. We believe that the Teaching Licence prices
are extremely cost-effective, and, indeed, have not risen since they were
introduced in 1994.

Many students now prefer to work on their own laptop machines (typically
running operating systems such as Linux) and, at the request of several
universities, B-Core now provides licences for such student machines in
addition to the department licence, at no further cost to the university.

Further, B-Core intends to make its own teaching material available on-line,
specifically aimed at those universities starting to teach B for the
first time.