Formal methods applied to complex systems: implementation of the B method

摘要

B, the language created by Jean-Raymond Abrial, stands (as a "confidential informant" had revealed to me more than a decade ago) for "Bourbaki." The letter refers to a 19th-century French general of Greek descent, Nicolas Bourbaki, whose name was adopted in the 1930s as a single, collective pseudonym by a group of French mathematicians seeking to reconstruct all of mathematics with full rigor, from the ground up. "Nicolas Bourbaki" soon included prominent non-French mathematicians, and "his" mathematical volumes, highly formal in "the Bourbaki style," continue to be well known, if not to everyone's taste. (This matter of taste is not relevant to the B-based formal-methods tools that are expounded in the excellent book under review, though no application of the contemporary formal-methods languages comprising today's Tower of Babel is the proverbial "walk in the park.").