Formal Methods and Object Technology

Rationale Software engineering aims to develop software by using approaches which en­ able large and complex program suites to be developed in a systematic way. However, it is well known that it is difficult to obtain the level of assurance of correctness required for safety critical software using old fashioned program­ ming techniques. The level of safety required becomes particularly high in software which is to function without a break for long periods of time, since the software cannot be restarted and errors can accumulate. Consequently programming for mission critical systems, for example, needs to address the requirements of correctness with particular care. In the search for techniques for making software cheaper and more reliable, two important but largely independent influences have been visible in recent years. These are: • Object Technology • Formal Methods First, it has become evident that objects are, and will remain an important concept in software. Experimental languages of the 1970's introduced various concepts of package, cluster, module, etc. giving concrete expression to the importance of modularity and encapsulation, the construction of software com­ ponents hiding their state representations and algorithmic mechanisms from users, exporting only those features (mainly the procedure calling mechanisms) which were needed in order to use the objects. This gives the software com­ ponents a level of abstraction, separating the view of what a module does for the system from the details of how it does them.

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.