Program Development by Refinement : Case Studies Using the B Method

The Idea of Program Refinement Programs are complex. They are typically so complex, that they go beyond the full comprehension even of the programmer or team who designed them, with all the consequences this has. How can we cope with such complexity in a satisfactory way? An approach, advocated for a long time, is to separate a concise specification of a program - the "what" - from a possibly involved implementation - the "how". Once a specification is obtained from the set of requirements on the program, there can still be a large gap to an efficient implementation. The development from specification to implementation can then proceed by a succession oflayers, such that each layer is a refinement of the previous one. Design decisions can be introduced in refinement steps one at a time. By this, the refinement steps can be kept small and manageable. Still, the set of all requirements can be far too large to be taken completely into account in the initial specification. Even if they could, they might obscure issues more than clarify them. For example: • An information system for stored goods needs to produce an error message on il­ legal input. Yet, the exact wording - and even the language - of those messages is irrelevant for an understanding of the essence of the system. • A banking application interacts with customers with a graphical interface. Yet the specification of the graphical layout is secondary compared to the specification of the possible transactions.

I. Information Systems.- 1. Introduction to the B Method.- 1.1 Machines.- 1.1.1 Machine Semantics and Generalised Substitutions.- 1.1.2 Set Theory and Types.- 1.1.3 Types in B.- 1.2 Specification.- 1.2.1 The Square Root Machine.- 1.2.2 The Unique Identifier Machine.- 1.3 Refinement.- 1.3.1 Procedural Refinement.- 1.3.2 Data Refinement.- 1.3.3 Refinement and Non-Determinism.- 1.4 Implementation.- 1.4.1 Layered Development.- 1.4.2 Proof Obligations.- 1.5 An Extended Example.- 1.5.1 A Simple Data Queue Machine.- 1.5.2 Refinement of the Data Queue.- 1.5.3 The Doubly-Linked List Machine.- 1.5.4 Implementing the DList Machine.- 1.5.5 The Node Machine.- 1.6 Exercises.- 1.7 Logic and Set Theory Notation.- 2. Container Station.- 2.1 Introduction.- 2.2 Task Description.- 2.3 Design of Specification.- 2.4 Introducing Fairness in a Refinement Step.- 2.5 Implementation: Development of Robust Software.- 2.6 Conclusions.- 2.7 Exercises.- 3. Minimum Spanning Tree.- 3.1 Introduction.- 3.2 The Minimum Spanning Tree Problem.- 3.2.1 An Abstract View of a Graph.- 3.2.2 Specification of the Minimum Spanning Tree Problem.- 3.3 Kruskal’s Algorithm.- 3.3.1 A Greedy Strategy.- 3.3.2 Correctness Proof.- 3.3.3 Decomposing the Development.- 3.4 The UNION-FIND Algorithm.- 3.4.1 Equivalence Relations.- 3.4.2 Representatives of Equivalence Classes.- 3.4.3 Tree Representation of Disjoint Sets.- 3.4.4 Weight Balancing.- 3.5 Heap Algorithms.- 3.5.1 Priority Queues.- 3.5.2 Indirect Heaps.- 3.5.3 Complete Binary Trees.- 3.6 Discussion.- 4. The B Bank.- 4.1 Introduction.- 4.2 Rewriting the Requirements.- 4.3 Structured Models.- 4.3.1 Class Diagrams.- 4.4 System Design.- 4.5 B Specification.- 4.5.1 State.- 4.5.2 Functionality.- 4.5.3 Discussion.- 4.6 Robust Abstraction.- 4.7 Base Machines.- 4.7.1 Strings in Atelier B.- 4.7.2 Machine BasicCGI.- 4.7.3 Implementing BasicCGI.- 4.8 User Interface.- 4.8.1 Main Program.- 4.8.2 Implementations.- 4.9 Implementation of the Robust Abstraction.- 4.10 Implementation of Bank.- 4.10.1 Machine Object.- 4.10.2 Machine BasicString.- 4.10.3 Implementation Bank_1.- 4.10.4 Machine BasicFile.- 4.10.5 Implementation Object_1.- 4.11 B-Toolkit Implementation.- 4.11.1 Differences in the Supported Language.- 4.11.2 Differences in the Provided Base Machines and Libraries.- 4.11.3 Adapting the Development.- 4.11.4 Automatic Translation of Object Models.- 4.12 Discussion.- 4.12.1 Related Work.- 4.12.2 Metrics.- 4.12.3 What Have We Proved?.- 4.13 Exercises.- II. Reactive Systems.- 5. Parallel Programming with the B Method.- 5.1 Introduction.- 5.2 Actions and Action Systems.- 5.2.1 Action Systems in B AMN.- 5.2.2 Actions in B AMN.- 5.3 Procedures Within Action Systems.- 5.3.1 Procedures.- 5.3.2 Procedures within Abstract Machines.- 5.4 Parallel Composition.- 5.5 Refining Action Systems.- 5.5.1 Data Refinement of Actions.- 5.5.2 Refinement of Action Systems.- 5.5.3 Refinement and Parallel Composition.- 5.6 Discussion.- 6. Production Cell.- 6.1 Introduction.- 6.1.1 Specifying Control Systems with Action Systems.- 6.1.2 Structure of the Development.- 6.2 The Production Cell.- 6.3 Specification of the Machines.- 6.3.1 The Feed Belt.- 6.3.2 The Table.- 6.3.3 The Robot.- 6.3.4 The Press.- 6.3.5 The Deposit Belt.- 6.4 Derivation of the Machine Controllers.- 6.4.1 The Feed Belt.- 6.4.2 The Table.- 6.4.3 The Robot.- 6.4.4 The Press.- 6.4.5 The Deposit Belt.- 6.5 Specification of the Production Cell.- 6.6 Derivation of the Production Cell Controller.- 6.7 Discussion.- 6.8 Exercises.- 7. Distributed Load Balancing.- 7.1 Introduction.- 7.2 Informal Problem Description.- 7.3 Problem Specification.- 7.4 Superposition Refinement.- 7.5 Superposition Step Within the B-Method.- 7.5.1 Enabledness of Global Proceduresq.- 7.5.2 Termination of Auxiliary Actions.- 7.6 Refinement Step 1: Distributing Loads.- 7.7 Refinement Step 2: Estimation of Neighbouring Loads.- 7.7.1 Refinement of Actions and Procedures.- 7.7.2 Refining the Guards of the Global Procedures.- 7.7.3 Termination of Auxiliary Actions.- 7.7.4 Introducing New Procedures.- 7.8 Refinement Step 3: Distributing the Estimates.- 7.9 Decomposition of the Load Balancing Algorithm.- 7.10 Discussion.- 7.11 Exercises.- 8. Distributed Electronic Mail System.- 8.1 Introduction.- 8.2 Event-Based Actions Systems.- 8.2.1 Parameter Passing.- 8.2.2 Refinement.- 8.2.3 Example Refinement: Unordered Buffer.- 8.3 Internal Actions.- 8.3.1 Refinement with Internal Actions.- 8.3.2 Example.- 8.3.3 Hiding Operator.- 8.4 Parallel Composition.- 8.4.1 Basic Parallel Composition of Actions.- 8.4.2 Basic Parallel Composition of Action Systems.- 8.4.3 Parallel Composition with Value-Passing.- 8.4.4 Design Technique.- 8.5 Email System.- 8.5.1 Abstract Specification.- 8.5.2 First Refinement of MailSys.- 8.5.3 Parallel Decomposition of MailSys.- 8.5.4 Parallel Decomposition of Agents.- 8.6 CSP Correspondence.- 8.7 Concluding.- 8.8 Exercises.- References.