A unifying type-theoretic framework for objects

AbstractWe give a direct type-theoretic characterization of the basic mechanisms of object-oriented programming, including objects, methods, message passing, and subtyping, by introducing an explicit constructor for object types and suitable introduction, elimination, and equality rules. The resulting abstract framework provides a basis for justifying and comparing previous encodings of objects based on recursive record types (Cardelli, 1984; Cardelli, 1992; Bruce, 1994; Cook et al., 1990; Mitchell, 1990a) and encodings based on existential types (Pierce & Turner, 1994).

Download Full-text

A specification logic for concurrent object-oriented programming

Mathematical Structures in Computer Science ◽

10.1017/s0960129599002789 ◽

1999 ◽

Vol 9 (3) ◽

pp. 253-286 ◽

Cited By ~ 4

Author(s):

G. DELZANNO ◽

D. GALMICHE ◽

M. MARTELLI

Keyword(s):

Logic Programming ◽

Programming Languages ◽

Linear Logic ◽

Operational Semantics ◽

Object Oriented ◽

Object Oriented Programming ◽

Higher Order Logic ◽

Specification Logic ◽

Theoretic Characterization

This paper focuses on the use of linear logic as a specification language for the operational semantics of advanced concepts of programming such as concurrency and object-orientation. Our approach is based on a refinement of linear logic sequent calculi based on the proof-theoretic characterization of logic programming. A well-founded combination of higher-order logic programming and linear logic will be used to give an accurate encoding of the traditional features of concurrent object-oriented programming languages, whose corner-stone is the notion of encapsulation.

Download Full-text

Simple type-theoretic foundations for object-oriented programming

Journal of Functional Programming ◽

10.1017/s0956796800001040 ◽

1994 ◽

Vol 4 (2) ◽

pp. 207-247 ◽

Cited By ~ 84

Author(s):

Benjamin C. Pierce ◽

David N. Turner

Keyword(s):

Message Passing ◽

Object Oriented ◽

Object Oriented Programming ◽

Simple Type ◽

Theoretic Foundations

AbstractWe develop a formal, type-theoretic account of the basic mechanisms of object-oriented programming: encapsulation, message passing, subtyping and inheritance. By modelling object encapsulation in terms of existential types instead of the recursive records used in other recent studies, we obtain a substantial simplification both in the model of objects and in the underlying typed λ-calculus.

Download Full-text

DKRL — AN OBJECT-ORIENTED LANGUAGE TO SUPPORT PROBLEM SOLVING IN DISTRIBUTED BLACKBOARD SYSTEMS

International Journal of Pattern Recognition and Artificial Intelligence ◽

10.1142/s0218001493000121 ◽

1993 ◽

Vol 07 (02) ◽

pp. 221-242 ◽

Cited By ~ 1

Author(s):

MANOJ K. SAXENA ◽

K.K. BISWAS ◽

P.C.P. BHATT

Keyword(s):

Problem Solving ◽

Knowledge Base ◽

Message Passing ◽

Object Oriented ◽

Object Oriented Programming ◽

Current Status ◽

External Knowledge ◽

Blackboard Systems ◽

Problem Solving Process ◽

Internal Knowledge

For distributed problem solving systems, there is a need to define knowledge at two levels, one external to the agents and the other internal to the agents. External knowledge is required to achieve cooperation among agents and global convergence of the problem solving process, whereas internal knowledge is required to solve the sub-problems assigned to the agents. External knowledge specifies the role of each agent and its relationship with other agents in the system. Internal knowledge specifies knowledge structure and the problem solving process within each agent. DKRL is an object-oriented language for describing distributed blackboard systems. In DKRL a problem solving system is described as a collection of distributed intelligent, autonomous agents (modelled as objects), cooperating to solve the problem. An agent consists of a knowledge base, a behaviour part, a local controller, a monitor, and a communication controller. DKRL has characteristics of a dynamic nature, i.e. the agents can be created dynamically and the relationship among them also changes dynamically. An agent in DKRL’s computational model cannot be activated by more than one message at the same time and uses a virtual synchrony environment for message transmission among agents. This model combines the advantages of remote procedure calls with those of asynchronous message passing. DKRL allows object-oriented programming techniques to be used for system development and facilitates the development by allowing one-to-one mapping between the objects in the knowledge model and the knowledge base of the agent. In this paper, we give an overview of the distributed blackboard paradigm for which DKRL was developed as well as the design considerations. We also propose and formally describe the underlying models of DKRL and explain how concurrency is exploited by DKRL. We conclude with the current status of and preliminary experience with DKRL in using it for the development of a gate assignment problem.

Download Full-text

Towards a Theory of Regular MSC Languages

BRICS Report Series ◽

10.7146/brics.v6i52.20122 ◽

1999 ◽

Vol 6 (52) ◽

Cited By ~ 6

Author(s):

Jesper G. Henriksen ◽

Madhavan Mukund ◽

K. Narayan Kumar ◽

P. S. Thiagarajan

Keyword(s):

Message Passing ◽

Finitely Generated ◽

Message Sequence Charts ◽

Proper Subclass ◽

Finite State ◽

Sequence Graph ◽

System Requirements ◽

Sequential Processes ◽

Theoretic Characterization

Message Sequence Charts (MSCs) are an attractive visual formalism widely used to capture system requirements during the early design stages in domains such as telecommunication software. It is fruitful to have mechanisms for specifying and reasoning about collections of MSCs so that errors can be detected even at the requirements level. We propose, accordingly, a notion of regularity for collections of MSCs and explore its basic properties. In particular, we provide an automata-theoretic characterization of regular MSC languages in terms of finite-state distributed automata called bounded message-passing automata. These automata consist of a set of sequential processes that communicate with each other by sending and receiving messages over bounded FIFO channels. We also provide a logical characterization in terms of a natural monadic second-order logic interpreted over MSCs. A commonly used technique to generate a collection of MSCs is to use a Message Sequence Graph (MSG). We show that the class of languages arising from the so-called locally synchronized MSGs constitute a proper subclass of the languages which are regular in our sense. In fact, we characterize the locally synchronized MSG languages as the subclass of regular MSC languages that are finitely generated.

Download Full-text

Proving Monitors Revisited: A First Step Towards Verifying Object Oriented Systems1

Fundamenta Informaticae ◽

10.3233/fi-1986-9402 ◽

1986 ◽

Vol 9 (4) ◽

pp. 371-399

Author(s):

Rob Gerth ◽

W.P. De Roever

Keyword(s):

Message Passing ◽

Object Oriented ◽

Axiomatic Characterization ◽

Synchronous Communication ◽

Proof Systems ◽

Shared Variables ◽

Soundness And Completeness ◽

Sequential Processes ◽

Object Oriented Systems

An axiomatic characterization of monitors, based on assumption-commitment style reasoning, is given that is sound and (relatively) complete. This characterization is based on the fundamental notions of cooperation and interference, but does not use them as second order notions. The cooperation test was originally conceived to capture the proof theoretical analogue of distributed message passing between disjoint processes, as opposed to the interference freedom test, being the proof theoretical analogue of concurrency based on interference by jointly shared variables. Since then, the cooperation test has been applied to characterize synchronous communication in Hoare’s Communicating Sequential Processes, Ichbia’s Ada, and Wirth’s Modula-2, supported by soundness and completeness proofs. An overview is given of the rationale underlying this characterization, culminating in the development of proof systems for a new monitor based programming language for concurrency (Communicating Modules, CM) which combines distributed message passing between processes with interference through local variables of a process which are shared between its sub-processes. As such this is a first step towards the formal verification of object oriented systems. In this context, we also show how the method, traditionally cauched in terms of proof outlines, can be rendered syntax directed in a precise and formal way. In a separate paper, the proof system has been shown to be sound and (relatively) complete.

Download Full-text