|
" Formal methods and object technology "
S.J. Goldsack and S.J.H. Kent (eds.).
| Document Type
|
:
|
BL
|
| Record Number
|
:
|
732137
|
| Doc. No
|
:
|
b551924
|
| Main Entry
|
:
|
S.J. Goldsack and S.J.H. Kent (eds.).
|
| Title & Author
|
:
|
Formal methods and object technology\ S.J. Goldsack and S.J.H. Kent (eds.).
|
| Publication Statement
|
:
|
Berlin: Springer-Verlag, 1996
|
| Series Statement
|
:
|
Formal Approaches to Computing and Information Technology.
|
| Page. NO
|
:
|
XVIII, 368 p.
|
| ISBN
|
:
|
3540199772
|
|
|
:
|
: 9783540199779
|
| Contents
|
:
|
I Introduction.- 1 The Object Paradigm.- 1.1 The Ubiquitous Object.- 1.1.1 Active Objects.- 1.2 Defining the Object Concept.- 1.3 Objects in Software v.- 1.4 Object Classes.- 1.4.1 Class Hierarchies and Inheritance of Properties.- 1.4.2 Multiple Inheritance.- 1.5 Clientship.- 1.5.1 Polymorphic Substitut ability.- 1.5.2 Abstract Classes and Dynamic Binding.- 1.5.3 Abstract Interfaces.- 1.5.4 Aggregation.- 1.5.5 Reuse.- 1.6 Conclusion.- 2 Formality in Object Technology IT.- 2.1 Formal Methods Concepts.- 2.2 Formal Methods in Object Technology.- 2.3 Object Technology in Formal Methods.- 2.4 Formal Underpinnings.- 2.5 Concurrency.- 2.6 Conclusions.- II Formal Methods in Object Technology.- 3 LOTOS in the Object-Oriented Analysis Process.- 3.1 Introduction.- 3.2 Reasons for Choosing LOTOS.- 3.3 The ROOA Method.- 3.4 Structuring Specifications.- 3.4.1 Aggregation.- 3.4.2 Behavioural Inheritance.- 3.5 Conclusions.- 4 The Impact of Inheritance on Software Structure.- 4.1 Introduction.- 4.2 Multiple Inheritance Hierarchies.- 4.3 Type-Module Hierarchies.- 4.4 A Model Of Multiple Inheritance Hierarchies.- 4.4.1 Basic Definitions.- 4.4.2 Discussion: Assumptions in the Model.- 4.5 A Model of Type-Module Hierarchies.- 4.5.1 Basic Definitions.- 4.5.2 Discussion: From Inheritance to Module Hierarchies.- 4.5.3 Discussion: Language Issues.- 4.6 Relating Multiple Inheritance and Module Hierarchies.- 4.7 Summary & Conclusions.- III Object Technology in Formal Methods.- 5 D_Parlog++: Object-Oriented Logic Programming with Distributed Active Classes.- 5.1 Introduction.- 5.2 Informal Computation Model of D_Parlog++.- 5.3 An Introductory Example.- 5.3.1 State Declaration and State Variables.- 5.3.2 Method Declaration.- 5.4 Communication Between Objects.- 5.4.1 Atomic Transactions.- 5.4.2 Self Communications.- 5.5 Inheritance and Delegation of Classes.- 5.5.1 Super Communication.- 5.5.2 Self Communication in an Inheritance Hierarchy.- 5.6 Concluding Remarks.- 6 Concurrency and Real-time in VDM++.- 6.1 Concurrency and Object Structuring.- 6.1.1 Why Concurrency.- 6.2 The world model.- 6.3 Synchronisation and threads in VDM++.- 6.4 Describing the behaviour of active objects.- 6.4.1 A new look at the Dining Philosophers.- 6.5 Concurrency and Contention.- 6.5.1 Declarative synchronization control (permission predicates).- 6.5.2 Example of a Passive Class.- 6.5.3 A return to the Dining Philosophers.- 6.6 Other Ways of Expressing Synchronisation.- 6.6.1 Traces.- 6.7 Feasibility and the periodic obligation.- 6.8 Specifying Real-time systems.- 6.8.1 Real-time requirements engineering.- 6.9 Language facilities.- 6.9.1 The notion of time.- 6.10 Continuous models.- 6.10.1 Continuous time variables.- 6.11 Continuous classes.- 6.11.1 An example of a continuous model.- 6.11.2 Subclasses of Component.- 6.12 The principle of discretising.- 6.12.1 Reasoning about sampling.- 6.13 Synchronising the components.- 7 Integrating Formal and Structured Methods in Object-Oriented System Development.- 7.1 B Abstract Machine Notation.- 7.2 Representation of Data Models.- 7.3 Representation of Dynamic Models.- 7.3.1 Process Model for Formalisation.- 7.4 Alternative State Representation.- 7.4.1 Comparison.- 7.4.2 Alarmclocks.- 7.5 Ship Load Planning.- 7.5.1 Results.- 7.6 Formalisation of Dynamic Models: A Lift System.- 7.6.1 From Analysis to Specification.- 7.6.2 Applications of Formalisation.- 8 Introducing Object-Oriented Concepts into a Net-Based Hierarchical Software Development Process.- 8.1 Introduction.- 8.2 Channel/Agency Nets.- 8.2.1 General Presentation.- 8.2.2 Techniques for the Use of CA Nets.- 8.3 General Object Concepts and Characteristics.- 8.4 The O-CA Net Model.- 8.4.1 Integration Methods.- 8.4.2 Description of Object Concepts in O-CA Nets.- 8.4.3 Structure Rules and Transformation Rules of O-CA Nets.- 8.5 O-CA Nets and PROOFS Method.- 8.5.1 Use of O-CA Nets.- 8.5.2 Link from O-CA Nets to PNs and CPNs.- 8.6 Example.- 8.7 Conclusion.- IV Formal Foundations of Object Technology.- 9 Design Structures for Object-Based Systems.- 9.1 Introduction.- 9.2 Temporal Specification of Objects.- 9.3 Interconnecting Objects.- 9.4 Interfacing: Action Calling.- 9.5 Abstraction: Object Calling.- 9.6 Concluding Remarks.- 10 Interconnection of Object Specifications.- 10.1 Some Preliminaries.- 10.1.1 Categories.- 10.1.2 Functors and Natural Transformations.- 10.1.3 Limits.- 10.1.4 Monoids.- 10.1.5 Right Actions of Monoids.- 10.1.6 Sheaves.- 10.2 Process Classes.- 10.3 Object Specification.- 10.4 System Specification.- 10.5 Some Speculations.- 11 Refinement of Concurrent Object-Oriented Programs.- 11.1 Overview of FOOPS.- 11.1.1 Functional Level.- 11.1.2 Object Level.- 11.2 Refinement for FOOPS.- 11.2.1 Simulations.- 11.2.2 Refinement of States.- 11.2.3 Refinement of Expressions.- 11.2.4 Refinement of Specifications.- 11.3 Proving Refinement.- 11.3.1 Memory Cells.- 11.3.2 Buffers.- 11.3.3 Laws of FOOPS Method Combiners.- 11.4 Aspects Considered by Refinement.- 11.5 Conclusions.- 12 Static Typing for Object-Oriented Languages.- 12.1 Introduction.- 12.2 Subclases and Subtypes.- 12.2.1 Type vs. Class.- 12.2.2 Subtype vs. Subclass.- 12.2.3 ST&T: An Example.- 12.3 Types in ST&T.- 12.3.1 Some Subclass Relationships in Smaltalk.- 12.3.2 Object Types.- 12.3.3 The Subtype Relationship.- 12.3.4 Method Signatures.- 12.3.5 Receiver Type, Argument Type, Application of a Signature.- 12.3.6 Method Types.- 12.4 Type Rules in ST&T.- 12.4.1 The Environment.- 12.4.2 Type Checking Classes.- 12.4.3 Types of Assignments.- 12.4.4 Types of Return Expressions.- 12.4.5 Types of Message Expressions.- 12.5 Discussion, Implementation, Soundness.- 12.6 Conclusions and Further Work.- 13 A Note on the Semantics of Inclusion Polymorphism.- 13.1 The Concept of Inclusion Polymorphism.- 13.2 Formalization of Inclusion Polymorphism.- 13.2.1 Object Types, Classes and Theories.- 13.2.2 Behavioural Subtyping - Simple Cases.- 13.2.3 Behavioural Subtyping - Contravariance.- 13.2.4 Behavioural Subtyping - General Case.- 13.3 Inclusion Polymorphism in Practice.- 13.3.1 C++.- 13.3.2 Eiffel.- 13.3.3 Smalltalk-80.- 13.3.4 Objective-C.- 13.4 Related Work.- 13.5 Conclusions.- 14 Categorical Semantics for Object-Oriented Data-Specifications.- 14.1 A Categorical Specification Mechanism.- 14.1.1 Classes and Dependencies.- 14.1.2 An Extended Example.- 14.1.3 Constraints.- 14.1.4 Attributes.- 14.2 Canonical Forms for Specifications.- 14.3 Verification of Specifications.- 14.4 A Note on Terminology.- 14.5 Specifications.- 14.5.1 Specifications without Attributes.- 14.5.2 Specifications with Attributes.- 14.5.3 Elimination of Attributes.- 14.6 Canonical Forms for Specifications.- 14.7 Verification of Specifications.- 14.7.1 Verification of the Underlying Category.- 14.7.2 Verification of Specifications.- 14.8 Conclusion.- 15 A Type-Theoretic Basis for an Object-Oriented Refinement Calculus.- 15.1 Introduction.- 15.2 Statements as Predicate Transformers.- 15.3 Objects as Packed Records.- 15.4 Using Abstract and Concrete Classes.- 15.5 Related Work and Conclusions.
|
| Subject
|
:
|
Programación orientada al objeto (Informática)
|
| LC Classification
|
:
|
QA76.64S546 1996
|
| Added Entry
|
:
|
Stephen J Goldsack
|
|
|
:
|
Stuart John Harding Kent
|
| |