The B Language and Method: A Guide to Practical Formal Development

ISBN-13: 9783540760337 / Angielski / Miękka / 1996 / 232 str.

K. Lano; Kevin Lano

Opis

This volume presents an introduction to the B Abstract Machine Notation, and how it can be used to support formal specification and development of high integrity systems. Emphasis is placed on the use of B in the context of existing software development methods.

Spis treści

1 Introduction.- 1.1 Formal Methods.- 1.2 The History of B.- 1.3 The Relationship of B to Other Formal Methods.- 1.4 Summary.- 2 The Foundations of B AMN.- 2.1 Mathematical Notation.- 2.2 Defining Operations.- 2.3 Abstract Machines.- 2.4 Machine Composition Mechanisms.- 2.5 Refinement.- 2.6 Implementation.- 2.7 Summary.- 2.8 Exercises 1.- 3 Analysis and Specification.- 3.1 Requirements Analysis.- 3.2 Specification Development.- 3.3 Animation.- 3.4 Proof of Internal Consistency Obligations.- 3.5 Ship Loading Case Study — Specification.- 3.6 Renaming.- 3.7 Aggregation.- 3.8 Summary.- 3.9 Exercises 2.- 4 Design and Implementation.- 4.1 The Layered Development Paradigm.- 4.2 Refinement Examples.- 4.3 Proofs of Refinement.- 4.4 Decomposing Implementations.- 4.5 Ship Loading Case Study — Implementation.- 4.6 Summary.- 4.7 Exercises 3.- 5 Case Studies.- 5.1 Personnel System Development.- 5.2 Mine Pump Control.- 5.3 Vending Machine.- 6 Conclusions.- A Exercise Solutions.- A.1 Exercises 1.- A.2 Exercises 2.- A.3 Exercises 3.- B Properties of Weakest Preconditions.- B.1 Termination and Feasibility.- B.2 Set-theoretic Semantics.- B.3 Refinement.- B.4 Well-formedness Obligations.- B.5 Normal Forms.- B.6 Rules for ?.- B.7 Definition of :=.- C Proof Techniques.