Merkzettel Warenkorb
  • Produktbild: Program Development by Refinement
  • Produktbild: Program Development by Refinement
- 11%

Program Development by Refinement Case Studies Using the B Method

Aus der Reihe Formal Approaches to Computing and Information Technology (FACIT)
11% sparen

189,99 € UVP 213,99 €

inkl. gesetzl. MwSt., Versandkostenfrei

Lieferung nach Hause

Beschreibung

Produktdetails

Einband

Taschenbuch

Erscheinungsdatum

23.10.1998

Herausgeber

Emil Sekerinski + weitere

Verlag

Springer London

Seitenzahl

364

Maße (L/B/H)

23,5/15,5/1,9 cm

Gewicht

542 g

Auflage

1999

Sprache

Englisch

ISBN

978-1-85233-053-8

Beschreibung

Produktdetails

Einband

Taschenbuch

Erscheinungsdatum

23.10.1998

Herausgeber

Verlag

Springer London

Seitenzahl

364

Maße (L/B/H)

23,5/15,5/1,9 cm

Gewicht

542 g

Auflage

1999

Sprache

Englisch

ISBN

978-1-85233-053-8

Herstelleradresse

Springer-Verlag GmbH
Tiergartenstr. 17
69121 Heidelberg
DE

Email: ProductSafety@springernature.com

Kundinnen und Kunden meinen

0 Bewertungen

Informationen zu Bewertungen

Zur Abgabe einer Bewertung ist eine Anmeldung im Konto notwendig. Die Authentizität der Bewertungen wird von uns nicht überprüft. Wir behalten uns vor, Bewertungstexte, die unseren Richtlinien widersprechen, entsprechend zu kürzen oder zu löschen.

Die Bewertungen sind nach Format, Anzahl Sterne und Datum sortiert.

Verfassen Sie die erste Bewertung zu diesem Artikel

Helfen Sie anderen Kund*innen durch Ihre Meinung

Kundinnen und Kunden meinen

0 Bewertungen filtern
  • Produktbild: Program Development by Refinement
  • Produktbild: Program Development by Refinement
  • 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.