Formal Object-Oriented Development
Springer Berlin (Verlag)
978-3-540-19978-6 (ISBN)
The text is extensively illustrated, both with tutorial and self-assessment excercises and with examples of industrial applications from the reactive systems domain. This book will be of interest to academic and industrial researchers, software engineering practitioners and consultants, and will also provide invaluable reading material for students learning Z++ and VDM++.
1 Introduction.- 1.1 Why is Mathematics Useful?.- 1.2 Formal Methods in Software Development.- 1.3 Formal Methods and Object-orientation.- 1.4 Z++.- 1.5 VDM++.- 1.6 Adding Formality to Diagrammatic Methods.- 1.7 Problems in Object-oriented Development.- 2 The Software Development Process.- 2.1 Formal Object-oriented Development.- 2.2 Example Development: Shapes and Points.- 2.3 The Layered Development Paradigm.- 2.4 Development Example in VDM++.- 3 From Analysis to Formal Specification.- 3.1 Formalisation of Object Models.- 3.2 Aggregation.- 3.3 Alternative Approaches.- 3.4 Formalisation of Dynamic Models.- 3.5 The Booch Method.- 3.6 Specification Construction Principles.- 3.7 Animation.- 4 Specification Notations and Techniques.- 4.1 Attributes and Data Structures.- 4.2 Operations.- 4.3 Inheritance.- 4.4 Subtyping.- 4.5 Class Composition.- 4.6 Object Identity.- 4.7 Dynamic Behaviour.- 4.8 Complex Data Types.- 4.9 VDM++.- 5 Design and Refinement.- 5.1 Design Approaches.- 5.2 Refinement.- 5.3 Subtyping, Composition and Refinement.- 5.4 VDM++.- 6 Proof Methods and Techniques.- 6.1 Safety Reasoning — Monitor and Gate.- 6.2 Liveness Reasoning — Dining Philosophers.- 6.3 Internal Consistency Proofs.- 6.4 Refinement and Subtyping Proofs.- 6.5 Object Identity.- 6.6 Reasoning About Concurrent Object Execution.- 6.7 Synchronisation Refinement Proofs.- 6.8 General Refinement Proof Techniques.- 7 Concurrent and Real-time Behaviour.- 7.1 Extended Harel Statecharts.- 7.2 Specifying Reactive System Properties.- 8 Implementation and Code Generation.- 8.1 Translation into Procedural Languages.- 8.2 Introducing Concurrency in Implementations.- 8.3 Implementation Case Study: Personnel System.- 8.4 Testing.- 9 Case Studies.- 9.1 Invoice System.- 9.2 Expedited Data Queue.- 9.3 FireControl.- 9.4 Specification of Reactive Systems.- 9.5 Mine Pump Control.- A.1 Mathematical Notation.- A.2 Z Notation.- B.4 The Semantics of Procedural Statements.- B.5 Tool Support.- C Exercise Answers.- D Task Analysis.
| Erscheint lt. Verlag | 25.10.1995 |
|---|---|
| Reihe/Serie | Formal Approaches to Computing and Information Technology (FACIT) |
| Zusatzinfo | XIV, 422 p. 4 illus. |
| Verlagsort | London |
| Sprache | englisch |
| Maße | 155 x 235 mm |
| Gewicht | 730 g |
| Themenwelt | Informatik ► Software Entwicklung ► Objektorientierung |
| Mathematik / Informatik ► Informatik ► Theorie / Studium | |
| Schlagworte | code generation • Concurrency • data structures • Design • Development • formal methods • formal specification • Inheritance • language • Semantics • Software • software development • Software engineering |
| ISBN-10 | 3-540-19978-0 / 3540199780 |
| ISBN-13 | 978-3-540-19978-6 / 9783540199786 |
| Zustand | Neuware |
| Haben Sie eine Frage zum Produkt? |
aus dem Bereich
