Blick ins Buch

The B Language and Method

A Guide to Practical Formal Development

Kevin Lano (Autor)

Buch | Softcover

VIII, 232 Seiten

1996 | 1. Softcover reprint of the original 1st ed. 1996
Springer Berlin (Verlag)
978-3-540-76033-7 (ISBN)

Lese- und Medienproben

Inhaltsverzeichnis (PDF)

Artikel merken

B is one of the few formal methods which has robust, commercially-available tool support for the entire development lifecycle from specification through to code generation. This volume provides a comprehensive introduction to the B Abstract Machine Notation, and to how it can be used to support formal specification and development of high integrity systems. A strong emphasis is placed on the use of B in the context of existing software development methods, including object-oriented analysis and design. The text includes a large number of worked examples, graduated exercises in B AMN specification and development (all of which have been class-tested), two extended case studies of the development process, and an appendix of proof techniques suitable for B. Based on material which has been used to teach B at postgraduate and undergraduate level, this volume will provide invaluable reading a wide range of people, including students, project technical managers and workers, and researchers with an interest in methods integration and B semantics.

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.

Erscheint lt. Verlag	14.5.1996
Reihe/Serie	Formal Approaches to Computing and Information Technology (FACIT)
Zusatzinfo	VIII, 232 p.
Verlagsort	London
Sprache	englisch
Maße	155 x 235 mm
Gewicht	375 g
Themenwelt	Mathematik / Informatik ► Informatik ► Programmiersprachen / -werkzeuge
	Mathematik / Informatik ► Informatik ► Software Entwicklung
	Informatik ► Theorie / Studium ► Compilerbau
Schlagworte	C programming language • Design • Development • formal methods • formal specification • language • Mathematica • Object-oriented analysis • Object-Oriented Analysis and Design • Semantics • Software • system development
ISBN-10	3-540-76033-4 / 3540760334
ISBN-13	978-3-540-76033-7 / 9783540760337
Zustand	Neuware