Software Engineering With B (International Computer Science Series)

Rating:
Summary: Guide to robust software development
Review: Mathematics in Software Development! Yes, that is what this book is all about. The book presents the B-method as a systematic engineering approach, backed by the formalism of mathematical specification, resulting in unambiguous analysis, design and development of software. The chapters in the book are as systematically organized as the subject of formal methods itself. Each chapter builds upon the previous one in a "layered" manner. Techniques presented in the book enable the conscientious software developer to design reusable component-based software that is amenable and robust to change. This book enriched my knowledge of software engineering and motivated me to look at software development from an entirely new perspective. It looks at software development from the design specifications point of view, rather than the conventional code-oriented development technique. The B-toolkit is an extremely useful resource. The book and the toolkit together provide a complete and practical insight into the world of formal software development. I would recommend this book to all software developers, who work with complex and large-scale software systems and who have always wanted a reliable method of defining their software systems.

Rating:
Summary: A quick glance at formal methods...
Review: The B method is a formal methodology for the development of software components as state machines. Basically you write a formal description of each component in a variant of Hoare-logic, submit it to the B tool, animate it to try it out, and when satisfied, use the B tool to generate proof obligations and semi-automatically prove it's partial correctness. Depending on the tool you use, it will also generate code, but that might be less important to you.

The limititations of B are quite obvious, it cannot be used to represent e.g. concurrent processes, but it might be helpful to you anyway, as surprisingly many tasks can be modelled as simple state-machines, and with good tool-support, it might even be an advantage to do so.

The book is short, and to the point. It will not work as a textbook for formal methods, being far too short, and not covering enough material (but it can be used as a starter text). It contains just enough to get you started using the B tool. The book is written in simple language, and can be understood by any reasonably intelligent programmer or software engineer. In particular, it does not require training in formal logic.

For people new to formal methods, this is the ideal starter text, but those that already know some would want to look elsewhere.