Formal Software Development
Spring Semester 2008
Here are some extra machines for you to look:
- An example of an injective function. wk2Injective.mch
You may wish to consult the concised summary of the B mathematical toolkit (reproduced with permisson from Ken Robinson). This is an essential guide to the ASCII notation you will need during the lab sessions.
- Full size
- 2 page reference card
You may wish to look at other B courses and websites
- Ken Robinson System Modelling and Design using B
- Ken Robinson Software Engineering using B. Contains interesting lecture notes on B machines to OO classes.
- B research pages
- Industrial Paris Metro Project used B
- Good Linux introduction
- B-Core toolkit suppliers. The site contains general articles about the method.
- Managing the construction of Large Computerized Systems - Jean Raymond Abrial
- Using UML and B
- B in large scale projects Daniel Dolle, Siemens
