A specification case study using the B‐methodology
Andrew C. Storey · Software Testing Verification and Reliability · 1992
Abstract The B‐Method is a complete formal development process for mathematically transforming software systems from specification through to code. This article provides the reader with an overview of the process including a description of the language used for specifying systems (Abstract Machine Notation) and demonstrates its application by a simple, real‐life case study. The method has tool support in the form of a tool‐kit which is described here and applied to the case study. The results of the case study show how a system can be validated and verified in the early stages of its development through proof of the mathematical specification and an animating tool.