An operational semantics for object-oriented concepts based on the class hierarchy

The formalisation of object-oriented languages is essential for describing the implementation details of specific programming languages or for developing program verification techniques. However there has been relatively little formalisation work aimed at abstractly describing the fundamental concepts of object-oriented programming, separate from specific language considerations or suitability for a particular verification style. In this paper we address this issue by formalising a language that includes the core object-oriented programming language concepts of field tests and updates, methods, constructors, subclassing, multithreading, and synchronisation, built on top of standard sequential programming constructs. The abstract syntax is relatively close to the core of typical object-oriented programming languages such as Java. A novel aspect of the syntax is that objects and classes are encapsulated within a single syntactic term, including their fields and methods. Furthermore, class terms are structured according to the class hierarchy, and objects appear as subterms of their class (and method instances as subterms of the relevant object). This helps to narrow the gap between how a programmer thinks about their code and the underlying mathematical objects in the semantics. The semantics is defined operationally, so that all actions a program may take, such as testing or setting local variables and fields, or invoking methods on other objects, appear on the labels of the transitions. A process-algebraic style of interprocess communication is used for object and class interactions. A benefit of this label-based approach to the semantics is that a separation of concerns can be made when defining the rules of the different constructs, and the rules tend to be more concise. The basic rules for individual commands may be composed into more powerful rules that operate at the level of classes and objects. The traces generated by the operational semantics are used as the basis for establishing equivalence between classes.     

Inter-deriving semantic artifacts for object-oriented programming

We present a new abstract machine for Abadi and Cardelli's untyped non-imperative calculus of objects. This abstract machine mechanically corresponds to both the reduction semantics (i.e., small-step operational semantics) and the natural semantics (i.e., big-step operational semantics) specified in Abadi and Cardelli's monograph. To move closer to actual implementations, which use environments rather than actual substitutions, we then represent methods as closures and we present three new semantic artifacts for a version of Abadi and Cardelli's calculus with explicit substitutions: a reduction semantics, an environment-based abstract machine, and a natural semantics (i.e., an interpreter) with environments. These three new semantic artifacts mechanically correspond to each other, and the two abstract machines are bisimilar. Their significance lies in the fact that they have not been designed from scratch and then proved correct; instead, they have been inter-derived.To illustrate the inter-derivation and to make this article stand-alone, we also comprehensively treat the example of negational normalization over Boolean formulas, in appendix.     

A family of syntactic logical relations for the semantics of Haskell-like languages

Logical relations are a fundamental and powerful tool for reasoning about programs in languages with parametric polymorphism. Logical relations suitable for reasoning about observational behavior in polymorphic calculi supporting various programming language features have been introduced in recent years. Unfortunately, the calculi studied are typically idealized, and the results obtained for them offer only partial insight into the impact of such features on observational behavior in implemented languages. In this paper we show how to bring reasoning via logical relations closer to bear on real languages by deriving results that are more pertinent to an intermediate language for the (mostly) lazy functional language Haskell like GHC Core. To provide a more fine-grained analysis of program behavior than is possible by reasoning about program equivalence alone, we work with an abstract notion of relating observational behavior of computations which has among its specializations both observational equivalence and observational approximation. We take selective strictness into account, and we consider the impact of different kinds of computational failure, e.g., divergence versus failed pattern matching, because such distinctions are significant in practice. Once distinguished, the relative definedness of different failure causes needs to be considered, because different orders here induce different observational relations on programs (including the choice between equivalence and approximation). Our main contribution is the construction of an entire family of logical relations, parameterized over a definedness order on failure causes, each member of which characterizes the corresponding observational relation. Although we deal with properties very much tied to types, we base our results on a type-erasing semantics since this is more faithful to actual implementations.     

A Space Semantics for Core Haskell

Haskell currently lacks a standard operational semantics. We argue that such a semantics should be provided to enable reasoning about operational properties of programs, to ensure that implementations guarantee certain space and time behaviour and to help determine the source of space faults. We present a small-step deterministic semantics for the sequential evaluation of Core Haskell programs and show that it is an accurate model of asymptotic space and time usage. The semantics is a formalisation of a graphical notation so it provides a useful mental model as well as a precise mathematical notation. We discuss its implications for education, programming and implementation. The basic semantics is extended with a monadic IO mechanism so that all the space under the control of an implementation is included.     

Mobile Agents in Interaction Spaces

Mobile agent systems are difficult to reason about and implement efficiently and safely. Theoretical work, most notably process calculi, provide solid semantics for mobile systems. However, the theory is often too abstract to match with the requirements of practical implementations. To fill this gap, intermediate models must be proposed. We present in this paper such a model named Interaction Spaces, a metaphor of geometrical spaces in which agents interact through simple transformations. The framework captures high-level distributed semantics, most notably asynchronous, multicast communications on FIFO channels. It also refines and implements the channel passing feature of the pi-calculus, together with the mobility of agent themselves. Above interaction spaces, we propose a full-fledged agent calculus and its associated operational semantics.     

A rewriting logic framework for operational semantics of membrane systems

Existing results in membrane computing refer mainly to P systems’ characterization of Turing computability, also to some polynomial solutions to NP-complete problems by using an exponential workspace created in a “biological way”. In this paper we define an operational semantics of a basic class of P systems, and give two implementations of the operational semantics using rewriting logic. We present some results regarding these implementations, including two operational correspondence results, and discuss why these implementations are relevant in order to take advantage of good features of both structural operational semantics and rewriting logic.     

Tensors, !-graphs,and Non-commutative Quantum Structures

!-graphs provide a means of reasoning about infinite families of string diagrams and have proven useful in manipulation of (co)algebraic structures like Hopf algebras, Frobenius algebras, and compositions thereof. However, they have previously been limited by an inability to express families of diagrams involving non-commutative structures which play a central role in algebraic quantum information and the theory of quantum groups. In this paper, we fix this shortcoming by offering a new semantics for non-commutative !-graphs using an enriched version of Penrose’s abstract tensor notation.     

Semantics of trace relations in requirements models for consistency checking and inferencing

Requirements traceability is the ability to relate requirements back to stakeholders and forward to corresponding design artifacts, code, and test cases. Although considerable research has been devoted to relating requirements in both forward and backward directions, less attention has been paid to relating requirements with other requirements. Relations between requirements influence a number of activities during software development such as consistency checking and change management. In most approaches and tools, there is a lack of precise definition of requirements relations. In this respect, deficient results may be produced. In this paper, we aim at formal definitions of the relation types in order to enable reasoning about requirements relations. We give a requirements metamodel with commonly used relation types. The semantics of the relations is provided with a formalization in first-order logic. We use the formalization for consistency checking of relations and for inferring new relations. A tool has been built to support both reasoning activities. We illustrate our approach in an example which shows that the formal semantics of relation types enables new relations to be inferred and contradicting relations in requirements documents to be determined. The application of requirements reasoning based on formal semantics resolves many of the deficiencies observed in other approaches. Our tool supports better understanding of dependencies between requirements.     

A confluent semantic basis for the analysis of concurrent constraint logic programs

The standard operational semantics of concurrent constraint logic languages is not confluent in the sense that different schedulings of processes may result in different program behaviors. While implementations are free to choose specific scheduling policies, analyses should be correct for all implementations. Moreover, in the presence of parallelism, it is usually not possible to determine how processes will actually be scheduled. Efficient program analysis is therefore difficult as all process schedulings must be considered. To overcome this problem, we introduce a confluent semantics which closely approximates the standard (nonconfluent) semantics. This semantics provides a basis for efficient and accurate program analysis for these languages. To illustrate the usefulness of this approach, we sketch analyses based on abstract interpretations of the confluent semantics which determine if a program is suspension- and local suspension-free.     

CPO Models for Compact GSOS Languages

In this paper, we present a general way of giving denotational semantics to a class of languages equipped with an operational semantics that fits the GSOS format of Bloom, Istrail, and Meyer. The canonical model used for this purpose will be Abramsky's domain of synchronization trees, and the denotational semantics automatically generated by our methods will be guaranteed to be fully abstract with respect to the finitely observable part of the bisimulation preorder. In the process of establishing the full abstraction result, we also obtain several general results on the bisimulation preorder (including a complete axiomatization for it), and give a novel operational interpretation of GSOS languages.     

Objects and Classes in Algol-Like Languages

Many object-oriented languages used in practice descend from Algol. With this motivation, we study the theoretical issues underlying such languages via the theory of Algol-like languages. It is shown that the basic framework of this theory extends cleanly and elegantly to the concepts of objects and classes. Moreover, a clear correspondence emerges between classes and abstract data types, whose theory corresponds to that of existential types. Equational and Hoare-like reasoning methods and relational parametricity provide powerful formal tools for reasoning about Algol-like object-oriented programs.     

Implementing associations: UML 2.0 to Java 5

A significant current software engineering problem is the conceptual mismatch between the abstract concept of an association as found in modelling languages such as UML and the lower level expressive facilities available in object-oriented languages such as Java. This paper introduces some code generation patterns that aid the production of Java based implementations from UML models. The work is motivated by a project to construct model driven development tools in support of the construction of embedded systems. This involves the specification and implementation of a number of meta-models (or models of languages). Many current UML oriented tools provide code generation facilities, in particular the generation of object-oriented code from class diagrams. However, many of the more complex aspects of class diagrams, such as qualified associations are not supported. In addition, several concepts introduced in UML version 2.0 are also not supported.The aim of the work presented in this paper is to develop a number of code generation patterns that allow us to support the automatic generation of Java code from UML class diagrams that support these new and complex association concepts. These patterns significantly improve the code generation abilities of UML tools, providing a useful automation facility that bridges the gap between the concept of an association and lower level object-oriented programming languages.     

A syntactic theory of sequential control

Sequential control operators like J and call/cc are often found in implementations of the λ-calculus as a programming language. Their semantics is always defined by the evaluation function of an abstract machine. We show that, given such a machine semantics, one can derive an algebraic extension of the λ_υ-calculus. The extended calculus satisfies the diamond property and contains a Church-Rosser subcalculus. This underscores that the interpretation of control operators is to a certain degree independent of a specific evaluation strategy. We also prove a standardization theorem and use it to investigate the correspondence between the machine and the calculus. Together, the calculus and the rewriting machine form a syntactic theory of control, which provides a natural basis for reasoning about programs with nonfunctional control operators.     

The operational semantics of user-defined relationships in object oriented database systems

In semantic data models, abstract relationship (e.g. generalization, aggregation, etc.) semantics are defined, specifying how insertion, deletion and modification operations made at a higher level of abstraction can affect the objects abstracted over and vice versa. These semantics, also known as structural constraints, are expressed through so-called update rules. This perspective has been somewhat lost in most object-oriented systems, where user-defined relationships are supported as simple pointers and their semantics are embedded, distributed and replicated within the operations accessing these pointers. This paper inherits and extends the treatment of relationships found in semantic data models to behavioural object-oriented models by presenting an approach to uniformly capture the update rules for user-defined relationships. The stress is not on supporting relationships as first-class objects, but on describing their update rules (or operational semantics) through a set of constructors namely, reaction, anticipation, delegation and exception. The approach has been borne out by an implementation in an active object-oriented database system.     

On Modeling Coordination via Asynchronous Communication and Enhanced Matching

The paper proposes a theoretical study of a coordination language embodying Linda's asynchronous communication primitive with a refined matching mechanism based on pairs composed of attribute names associated with their values. Computations in this language are described by means of an operational semantics, reporting the whole traces of executions. The non-compositionality of this intuitive operational semantics motivates the design of a compositional and fully abstract denotational semantics, which is then exploited for studying program equivalence in this setting.     

There is no fully abstract fixpoint semantics for non-deterministic languages with infinite computations

It is well known that for many non-deterministic programming languages there is no continuous fully abstract fixpoint semantics. This is usually attributed to “problems with continuity”, that is, the assumption that the semantic functions should be continuous supposedly plays a role in the difficulties of giving a fully abstract fixpoint semantics. We show that for a large class of non-deterministic programming languages there is no fully abstract least fixpoint semantics even if one considers arbitrary functions (not necessarily continuous) over arbitrary partial orders (not necessarily complete).     

Compatibility of parameter passing and implementation of parameterized data types

The basis for this paper are the concepts of parameterization and implementation of abstract data types which have been developed in the theory of algebraic specifications with initial algebra semantics. In this paper we combine both concepts defining implementations of parameterized data types and studying the compatibility of parameter passing and implementation of parameterized data types. In our main result we show that parameter passing commutes with implementation. This is an important step in order to apply the theory of algebraic specifications to development and stepwise refinement of software systems. We illustrate our notion and results by a small example implementing binary trees over arbitrary data by corresponding strings with brackets. Finally we consider the problem of 2-dimensional compatibility of parameter passing and implementation and discuss the kind of compatibility results which have been shown by other authors in the case of loose and final algebra semantics.