| Document Type
|
:
|
BL
|
| Record Number
|
:
|
746859
|
| Doc. No
|
:
|
b566810
|
| Main Entry
|
:
|
K. Lano.
|
| Title & Author
|
:
|
The B language and method : : a guide to practical formal development\ K. Lano.
|
| Publication Statement
|
:
|
London : Springer Verlag, 1996
|
| Page. NO
|
:
|
232 p. ; 24 cm
|
| ISBN
|
:
|
3540760334
|
|
|
:
|
: 9783540760337
|
| Notes
|
:
|
Facit--Cubierta.Incluye índice.
|
| Contents
|
:
|
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.
|
| Subject
|
:
|
B (Lenguaje de programación para computadora)
|
| LC Classification
|
:
|
QA76.73.B155K536 1996
|
| Added Entry
|
:
|
Kevin Lano
|