A selection of testimonials from lecturers currently using the B-Toolkit in teaching B.

• University of Manchester,
  Department of Computer Science
  

  Dr. R.H.Banach
  email: banach@cs.man.ac.uk
  web: www.cs.man.ac.uk/~banach
  

  CS611 System Construction Using B, is a module in the MSc in Advanced
  Computer Science at the University of Manchester. Like all modules in this
  masters course it is run in intensive mode, with one week's contact
  teaching, preceded by one week's preparatory reading, and followed by
  a one week practical assignment. The course text (Software Engineering in B,
  by Wordsworth) is mercifully light regarding the extensive formal
  underpinnings of B, making it suitable for use in this course format.
  The students come away with an appreciation of the breadth of coverage
  of the B-Method, with an emphasis on the building of specifications.
  The B-Toolkit certainly brings the material to life for students in
  a way that pure chalk and talk could never do.
  

  
  

• Michigan State University
  Department of Computer Science and Engineering
  

  Prof. Laura K. Dillon
  email: ldillon@cse.msu.edu
  web: www.cse.msu.edu/~ldillon
  

  The B module is the first module in a 15 week graduate level class
  on formal methods. Students had no prior experience with formal
  methods.
  

  The B module provided a great introduction to methods of formal
  specification and design. The B book (Software Engineering in B)
  motivates the method well and describes it clearly and completely.
  The unified approach used in B, which is based on well known
  mathematical concepts (sets, relations, predicate logic, state
  machines, etc.), was easy for students to learn and understand.
  The B-Toolkit allowed them to see the benefits of formality,
  reinforced their understanding of the B method, and provided them
  concrete feedback about their designs. It also made the course more
  "hands on" and fun!
  

  Following the module on B, the class covered process algebras,
  temporal logic, and model checking.
  

  
  

• Royal Holloway, University of London
  Department of Computer Science
  

  Steve Schneider
  email: S.Schneider@cs.rhul.ac.uk
  web: www.cs.rhul.ac.uk/research/formal/steve.html
  

  `Advanced methods for Software Engineering'
  An 11 week (33 hour) final year undergraduate course on the B-Method.
  

  In 1995 I switched to using the B-Method for teaching formal methods.
  The initial motivation for using B was the single uniform notation for
  teaching so many of the techniques that I wanted to cover, including
  state-based specification, data refinement, wp calculus, and reasoning
  about loops. It quickly became clear that the B-Toolkit was able to
  synthesise all of these techniques, and bring them to life in a way that
  gave students a real appreciation of a practical formal software
  development process.
  

  The course now teaches the B-Method, rather than `formal methods using B
  notation', and developed into my book The B-Method: an Introduction.
  It makes heavy use of the B-Toolkit from the very first week. The students
  respond well to the ability to animate, explore, and debug their
  specifications, to structure their developments, to verify their
  implementations, and to generate code at the touch of a button. They
  really believe in the viability of formal methods for real software
  development, in a way that simply did not happen before the tool support
  was available. Most importantly, they enjoy the learning experience.
  

  
  

• University of Teesside
  School of Computing and Mathematics
  

  Steve Dunne, Senior Lecturer in Computing
  email: s.e.dunne@tees.ac.uk
  

  The B method is now the basis of all our formal methods teaching
  at Teesside. First-year students on the Computer Science,
  Software Engineering and Informatics routes of our BSc Computing
  are introduced to it in our year 1 semester 2 core module
  Formal Methods 1 (FM1). Students at this stage have only had
  elementary exposure to a few underlying discrete mathematics
  concepts in the first semester, so the principles of formal modelling
  and state-based formal specification are taught in FM1 essentially
  from scratch. This is done mainly by use of simple examples, all
  processed by the B-Toolkit. The individual discrete mathematics
  constructs like sets, relations and functions are introduced as
  needed. The emphasis at this stage is on system modelling rather
  than abstract theory, but even so the B-Toolkit provides invaluable
  support for: (1) quality control by its powerful syntax and
  type-checking capabilities and its impressive document mark-up
  feature which facilitates a high professional standard of
  documentation; (2) verification by its ability to generate consistency
  proof obligations for a specification component and its autoprover
  facility which seeks to discharge them; (3) validation by its
  easy-to-use specification animation facility; and (4) specification
  structuring with its support for the B method's component composition
  operators INCLUDES, USES and SEES.
  Although at this stage students do not yet engage in formal proof
  as such, they are encouraged to review any proof obligation relating
  to the consistency of their specification which the Autoprover
  fails to discharge, in case it has arisen from any mistake or
  oversight in their spcification.
  

  Second-year students may follow up FM1 with our year 2 semester 1
  module Formal Methods 2 (FM2) which addresses refinement
  and implementation, with particular emphasis on the B method's
  own characteristic "layered-implementation" paradigm (re B's IMPORTS
  and SEES composition operators). Here especially, the B method's modular
  approach to proof obligation generation comes into its own. The B-Toolkit's
  provers environment is exploited for its support of user-driven proofs,
  and students are encouraged to formulate their own domain-specific
  proof rules where appropriate to achieve discharge of their refinement
  proof obligations.
  

  Final-year students must each undertake a major personal project.
  Sometimes such a student will choose to undertake a B based project
  using the B-Toolkit. He or she will thus have the opportunity to
  exercise the B method further, and explore the finer points of the
  B-Toolkit in considerable depth. These projects have invariably been
  completed to a high standard.
  

  The originators of the B method and its support tools like the B-Toolkit
  are justly proud to assert that theirs is a genuine industrial-strength
  and comprehensive formal method that has already been and continues to be
  applied to large-scale real-life systems. It should also be noted that it
  "scales down" equally effectively to treat the sort of elementary examples
  we employ during the early stages of our teaching. With the B-Toolkit
  our students clearly sense that even for their small-scale learning
  exercises they are employing, albeit lightly, a full-strength tool.
  This, we feel sure, has an impact on their perception of formal methods
  as a potential reality in the software industry rather than a mere academic
  novelty.