Formal Object-Oriented Development

Kevin Lano (Autor)

Buch | Softcover

XIV, 422 Seiten

1995 | 1. Softcover reprint of the original 1st ed. 1995
Springer Berlin (Verlag)
978-3-540-19978-6 (ISBN)

Artikel merken

Formal Object-Oriented Development provides a comprehensive overview of the use of formal object-oriented methods; it covers how and where they should be introduced into the development process, how they can be introduced selectively for critical parts of an application, and how to incorporate them effectively into existing deveopmental practices.
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
Themenwelt	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