BRICS RS-98-52 Kleist & Sangiorgi: Imperative Objects and Mobile Processes BRICS

Basic Research in Computer Science

Imperative Objects and Mobile Processes

Josva Kleist Davide Sangiorgi BRICS Report Series RS-98-52 ISSN 0909-0878 December 1998 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1998, BRICS, Department of Computer Science

University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent BRICS Report Series publications. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK–8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk
ftp://ftp.brics.dk

This document in subdirectory RS/98/52/

Imperative Objects and Mobile Processes

Josva Kleist^{∗}  Davide Sangiorgi^{†}

December, 1998

Abstract

An interpretation of Abadi and Cardelli’s first-order Imperative Object Calculus into a typed π-calculus is presented. The interpretation validates the subtyping relation and the typing judgements of the Object Calculus, and is computationally adequate. The proof of computational adequacy makes use of (a π-calculus version) of ready simulation, and of a factorisation of the interpretation into a functional part and a very simple imperative part. The interpretation can be used to compare and contrast the Imperative and the Functional Object Calculi, and to prove properties about them, within a unified framework.

1 Introduction

In their book [1], Abadi and Cardelli present and investigate a Functional and an Imperative Object Calculus, and type systems for them. These calculi can express, as primitive or derived forms, various major object-oriented idioms; they have simple but interesting typing and subtyping rules. The syntactic simplicity of the calculi, and their clear object-oriented flavour, makes them an important basis for understanding object-oriented languages. All Object Calculi are sequential.

In this paper we study the interpretation of the (first order) Imperative Object Calculus (IOC) into a typed π-calculus. Our main motivations are:

1. There is a general lack of mathematical techniques for giving the semantics to, and proving properties about, object-oriented languages , especially the imperative ones. (For instance, it seems difficult to come up with reasonable notions of bisimulation for IOC. This contrasts with the Functional Object Calculus (FOC), for which one such notion has been developed.) However, most “real world” programming languages are imperative. Usually, objects encapsulate a state, which can be manipulated by activating the methods of the object.

∗BRICS, Department of Computer Science, Aalborg University, Denmark. Email:

kleist@cs.auc.dk

†INRIA Sophia-Antipolis, France. Email: davide.sangiorgi@sophia.inria.fr

The π-calculus has a rich algebraic theory and a high expressive power. Its emphasis on the notions of name and of mobility makes it appealing for describing objects and their local states.

2. IOC is an interesting core object-oriented language, because it is small and yet very expressive; for instance classes and functions, as well as the Functional Object Calculus (FOC), can be encoded in it. A study of IOC can provide a solid basis for investigating more complex languages, that may include also, for instance, constructs for distribution and concurrency.

3. We wish to understand what are objects from a π-calculus (and more generally, a process calculus) point of view.

The only work on behavioural equivalences for IOC that we are aware of is Gordon, Hankin and Lassen’s [7]. In this work, however, IOC is untyped. Gordon, Hankin and Lassen study contextual equivalence for this untyped IOC, prove that it coincides with a variant of Mason and Talcott’s CIU equivalence [15], and use the latter to validate some basic laws of the calculus.

More work exists on the semantics of the Functional Object Calculus FOC. Typed contextual equivalence and applicative bisimulation for FOC have been examined by Gordon and Rees [8], who show that these two notions of equivalence coincide. They also show that Abadi and Cardelli’s equational theory for FOC [1] is sound w.r.t. operational equivalence. Abadi and Cardelli [1, Chapter 14] shows that the equational theory for FOC is also sound with respect their denotational semantics of FOC. Aceto et al. [3] show that the denotational semantics is sound but not fully abstract w.r.t. operational equivalence. Extending the above-mentioned techniques, based on applicative bisimulation and denotational models, to the Imperative Object Calculus IOC appears rather hard.

An interpretation of IOC into a form of imperative polymorph λ-calculus with subtyping, recursive types and records has been found by Abadi, Cardelli and Viswanathan [2]. This interpretation has been used to validate the subtyping and typing judgements of IOC. However, it would be difficult to prove behavioural properties of IOC from this interpretation, because very little is known of the theory of the target imperative λ-calculus.

Some previous studies of encodings of imperative or OOLs into process calculi, namely [16, Chapter 8], [27], [11], [29, 14], and [24, 10], are an important basis for our work. We briefly comment on the differences. Milner [16, Chapter 8] showed how to translate a small imperative language into CCS. Vaandrager [27], Jones [11] and Walker, Liu and Philippou [29, 14, 20] have gone further, by translating parallel object-oriented languages derived from the POOL family. Walker, Liu and Philippou have also used the encodings for proving the validity of certain program transformations on the source languages. The main limitation of these works is that they do not show how to handle typed objectoriented languages — the source languages have rather simple type systems and the translations do not act on types. Dealing with types is important when the type system of the object-oriented language contains non-trivial features like subtyping and polymorphism, otherwise many useful program equalities are lost and the semantics cannot be used to validate the typing rules of the language. By contrast, types play a central role in our interpretation. For this reason, our interpretation of objects is different from those in the above-mentioned works. In [10, 24], interpretations of, respectively, untyped and typed FOC into the π-calculus are given. No use is made of the π-calculus interpretation for for validating behavioural properties of the source Object Calculus.

The syntax of FOC and IOC are similar, but their operational semantics are very different (for instance, the operational semantics of IOC makes an extensive use of stores and stacks, not needed for FOC because it is functional). Remarkably, despite these differences in the operational semantics, the π-calculus interpretation of IOC in this paper can be derived with a simple change from that of FOC in [24]. As a consequence we can use the π-calculus interpretations to compare and contrast the Imperative and Functional Object Calculi — for instance, their discriminating power — and to prove properties about them, within a single framework.

The type language we use for the π-calculus is taken from [21, 24]. In these type systems, as well as other type systems for the π-calculus like [12, 28, 9], types are assigned to names. The types in [21] show the arity and the directionality of a name and, recursively, of the names carried by that name; the difference in [24] is variant types in place of tupling. All values are “simple”, in the sense that they are built out of names only, and cannot contain, for instance, process expressions.

The main technical contents of this paper are the following. We give a translation of both IOC terms and IOC types and type environments into the typed π-calculus. We then provide correctness proofs. Precisely, we prove that (1) the translation validates the subtyping judgements of IOC, that is, A is a subtype of B iff the translation of A is a subtype of the translation of B; (2) a IOC type judgement E ⊢ a : A, asserting that object a has type A under the type assumptions E, is true iff its π-calculus translation is true, and (3) a well-typed IOC term reduces to a value iff its π-calculus interpretation does so (computational adequacy). From these results and the compositionality of the encoding, as a corollary we get the soundness of the translation w.r.t. behavioural equivalences like Morris-style contextual equivalence or barbed congruence [19]. Soundness assures us that the equalities on IOC terms provable from the interpretation are operationally valid on IOC. As for the translations of λ-calculi into π-calculus, the opposite implication fails.

The IOC language we interpret into the π-calculus has a first-order type system. The interpretation can be easily extended to accommodate other features, like recursive types, variant tags, and polymorphism.

Technically, the hardest part of our work is the proof of computational adequacy. The proof is split into two parts. First we factorize our encoding into a functional part, where processes are “stateless”, and a very simple imperative part, where processes have a state. This factorisation is useful because: (1) it allows us take full advantage of various π-calculus proof techniques for functional processes; (2) it shows what – we believe – are the simplest non-functional π-calculus processes that are needed for translating the imperative features of IOC. This factorised encoding is less compact than the original one; but it allows us to establish a close correspondence with Abadi-Cardelli’s operational semantics of IOC.

The second part of the proof of computational adequacy is to establish a relation between the original encoding and the factorised one. To this end, we could not use known behavioural equivalences of the π-calculus (for instance, known bisimilarities were too strong; trace equivalence too weak to yield the desired property). We solved the problem by adapting (a weak version of) the notion of ready simulation [4, 13] to the π-calculus. Roughly, ready simulation was introduced in CCS-like languages as the least congruence contained in trace inclusion induced by certain classes of operators. To our knowledge, our application of ready simulation to derive properties of processes is novel.

Having established the correctness of our interpretation, we give some examples of how the theory of the π-calculus can be used to reason about IOC. The advantage of using π-calculus for the proofs is that we can take advantage of the already available theory, including its algebraic laws and its co-inductive proof techniques. Here, we use the π-calculus to validate some basic equational theory for IOC. Something interesting about the coinductive π-calculus proofs is that non-trivial equalities can be proved using finitary relations (this is more rare with CIU equivalence on untyped IOC [7] or applicative bisimulation on FOC [8] because the definition, or the transition system, on which they are based, contains an infinite quantification on contexts, or terms, of the language).

Among the laws we prove is (Eq Sub Object). This law allows us to eliminate methods of objects that are not visible in the type assigned to the object. We are not aware of proposals of this, or similar laws, for IOC. In Abadi-Cardelli’s book, the analogous of law (Eq Sub Object) is at the heart of the equational theory of FOC, but no equational theory for IOC is proposed (in the book or, as far as we know, elsewhere). Strikingly, we can prove (Eq Sub Object) using a bisimulation relation consisting of just two elements. Essentially the same proof can be used for (Eq Sub Object) on FOC.

In this short version of the paper, for lack of space most of the proofs are omitted.

2 The Imperative Object Calculus

In this section we present the (first-order) Imperative Object Calculus (IOC) from [1]. Grammar, operational and typing rules are reported in Appendix A.

Syntax. An object [l_{i}=ς(x_{i}:A)b_{i} ^{i∈1..n}] consists of a collection of named methods l_{i} = ς(x_{i}:A)b_{i} for distinct names l_{i}, and where x_{j}’s are the self parameters. The letter ς (sigma) is a binder for the self variable in a method; ς(x:A)b is a method that when activated evaluates its body b with x bound to the enclosing object. A method activation a.l results in the activation of the method bound to l in a; this method is evaluated with a as argument for self. Instantiating this parameter at call time results in what is named late binding — the self of a method can change dynamically at runtime. A method update a.l⇐ς(x:A)b replaces the method named l in the object a with ς(x:A)b and evaluates to the modified object. Cloning creates a copy of the original object. A let x:A = a in b expression first evaluates the let-part, binding the result to x, then the in-part is evaluated with the variable x in scope. Sequential evaluation of objects a; b can be defined thus: let x:A = a in b for some x ∉ fv(b).

Operational semantics. Object terms are evaluated w.r.t. a global store σ. If the evaluation of an object terminates, the object reduces to a value [l_{i}=ι_{i} ^{i∈1..n}] and an updated store. The store σ contains closures; a closure is the pair ⟨ς(x)b, S⟩ of a method body ς(x)b together with a local stack. A stack S maps variables to values. For any mapping f we let dom(f) denote the domain of f. A stack S is well-formed w.r.t. a store σ, written σ · S ⊢ ⋄ if for all x ∈ dom(S) S(x) = [l_{i}=ι_{i} ^{i∈1..n}] all ι_{i} is defined in σ. A store σ is well-formed, written σ ⊢ ⋄ if the stacks in all closures in the store are well-formed w.r.t. the store.

If σ is a store, then we let σ, ι↦ ⟨ς(x)b, S⟩ denote the extension of σ with the new entry ⟨ς(x)b, S⟩ on the new location ι, assuming that σ · S ⊢ ⋄. We write σ[ι↦ ⟨ς(x)b, s⟩] for the update of location ι of store σ, assuming that ι ∈ dom(σ) and again σ · S ⊢ ⋄.

The operational semantics is untyped; type annotations are simply removed when evaluating terms. We write a⇓v · σ (“a converge to the value v and store σ”) if we can deduce ∅ · ∅ ⊢ a ⇝ v · σ and a⇓ iff a⇓v · σ for some v and σ. If there is no v and σ such that a⇓v · σ we write a⇑ (“a diverges”).

Type system. There are two forms of judgments for IOC: Type judgments and subtyping judgments. Type judgments are of the form E ⊢ a:A and state that the object a has type A under the assumptions in E, where E describes typing assumptions for free self variables. If E is empty we shall sometimes just write a:A instead of ∅ ⊢ a:A. Subtype judgments A <: B state that the type A is a subtype of B. Subtyping allows an object to be replaced by another with additional methods, but the common methods must have the same type. This invariance is necessary for the soundness of the reduction rules, i.e. avoiding requests on methods which do not exist.

3 A typed mobile calculus

In this section we present the typed π-calculus on which we shall interpret IOC.

Syntax. The syntax of the typed π-calculus is given in Table 1. The process constructs are those of the monadic π-calculus [18] with matching replaced by a case construct. The latter can be thought of as a more disciplined form of matching, in which all tests on a given name are localised to a single place. The construct wrong stands for a process in which a run-time type error has occurred — i.e., for instance a communication in which the variant tag or the arity of the transmitted value was unexpected by its recipient. A soundness theorem guarantees that a well-typed process expression cannot reduce to an expression containing wrong.

Names p, q, r … x, y, z

Variant Tags ℓ, l, h

Types

T ::= μ(X)T recursive type
| X  type variable
| [ ℓ_{1} T_{1}..ℓ_{n} T_{n}] variant type
| ⟨T_{1} … T_{n}⟩  tuple type
| T^{I}  channel type

I /O Tags

I ::= r input only
| w  output only
| b  either

Values

v ::= x  name
| ⟨v_{1}..v_{n}⟩ tuple value
| ℓ v  variant value

Processes

P ::= 0  nil process
| P |P  parallel
| (νx:T)P restriction
| p(x).P  input
| \overline{p}v.P  output
| !P  replication
| let x_{1}..x_{n} = v in P

tuple destructor

| case v of [_{j∈1..n} ℓ_{j} (x_{j}) ⊳ P_{j}]

case

| wrong  error

where:

• In a recursive type μ(X)T, variable X must be guarded in T, i.e., occur underneath a I/O-tag or underneath a variant tag;

• in the case statement, the tags ℓ_{i} (i ∈ 1..n) are pairwise distinct.

Table 1: The syntax of the typed π-calculus

Operational semantics. For the semantics of the π-calculus we adopt a labelled transition system. The advantage of a labeled semantics, compared to a reduction semantics [17, 24], is that it easily allows us to define labeled forms of bisimulation. Process transitions are of the form P \overline{}^{μ} P′, where μ is given by the following syntax:

μ ::= (νñ:T̃)p̄v | pv | τ | wrong

The label (νñ:T̃)p̄v denotes the output of the value v on the name p. The restriction (νñ:T̃) where ñ must be a subset of the names in v indicates that the names ñ are bound names having types T̃. The label pv denotes the input of the value v over the name p. The action τ denotes an internal action. Finally, wrong denotes a run-time error. The rules for the operational semantics are standard rules of the π-calculus; for instance the rules for input, and the communication rule are:

\frac{−}{p(x).P \overline{}^{pv} P \{^{v}/_{x}\}}  \frac{P \overline{}^{(νñ:T̃)p̄v} P′ Q \overline{}^{pv} Q′}{P | Q \overline{}^{τ} (νñ:T̃)(P′ | Q′)} ñ ∩ fn(Q) = ∅

The new, but expected, rules are those for let and case, in which run-time errors may be generated. For case we have (let is similar):

\frac{ℓ_{j} ∈ \{ℓ_{1} … ℓ_{n}\}}{case ℓ_{j} v of [ ℓ_{1} (x_{1}) ⊳ P_{1}; …; ℓ_{n} (x_{n}) ⊳ P_{n}] \overline{}^{τ} P_{j}\{^{v}/_{x}\}}

\frac{v ≠ ℓ_{j} v′ or ℓ_{j} ∉ \{ℓ_{1} … ℓ_{n}\}}{case v of [ ℓ_{1} (x_{1}) ⊳ P_{1}; …; ℓ_{n} (x_{n}) ⊳ P_{n}] \overline{}^{wrong} wrong}

We write P \overline{}^{μ} _{d} Q if P \overline{}^{μ} Q is the only transitions that P can perform. And as usual we let ⟹^{μ} denote weak transitions, and P ⟹ P′ means “P ⟹^{τ} P′ or P = P′”.

Typing and subtyping. We recall that I/O annotations [21] are to separate the capabilities of reading and writing on a channel (we use “read” and “write” as synonymous for “input” and “output”, respectively). For instance, a type p : ⟨S^{r} T^{w}⟩^{b} (for appropriate type expressions S and T) says that name p can be used both to read and to write and that any message at p carries a pair of names; moreover, the first component of the pair can be used by the recipient only to read, the second only to write.

Subtyping judgements, shown in Table 2, are of the form Σ ⊢ S <: T, where Σ represents the subtyping assumptions. We often write S <: T when the subtyping assumptions are empty. Note that type annotation r (an input capability) gives covariance, w (an output capability) gives contravariance, and b (both capabilities) gives invariance. A type environment Γ a finite assignment of types to names.

A typing judgement Γ ⊢ P asserts that process P is well-typed in Γ, and Γ ⊢ v : T (Table 2) that value v has type T in Γ. There is one typing rule for each process construct except wrong. The interesting rules are those for input and output prefixes and for case. In the rules for input and output prefixes, the subject of the prefix is checked to possess the appropriate input or output capability in the type environment. A subject reduction theorem guarantees us that if P is well-typed and P ⟹ Q, then Q does not contain the process wrong.

Some derived constructs. In the translation we shall use: Recursive definitions, A(x̃) =^{def} P which can be defined the standard way from replication (c.f. [17]); polyadic inputs a(x_{1} … x_{n}).P, defined as a(y).let ⟨x_{1} … x_{n}⟩ = y in P for y ∉ fn(P); variant inputs, like p[_{j∈1..n} ℓ_{j} [_{i∈1..m} ℓ_{i,j} (x̃_{i,j}) ⊳ P_{i,j}]]. The last abbreviation allows us to go down two levels into the structure of a variant value received in an input at p; in fact, this term interacts with output particles of the form \overline{p}ℓ_{r} ℓ_{s,r} w̃ (with r ∈ 1..n, s ∈ 1..m, and tuple w̃ of the same length as x̃_{r,s}) and, in doing so, it reduces to P_{r,s}{w̃/x̃_{r,s}}.

Barbed bisimulation and congruence. The behavioural equality we adopt for the π-calculus is barbed congruence. Barbed congruence is a bisimulation-based relation that has been used for a broad variety of calculi; its main advantage Subtyping rules:

\frac{Σ ⊢ S <: T Σ ⊢ T <: S}{Σ ⊢ S^{b} <: T^{b}}  \frac{I ∈ \{b, r\} Σ ⊢ S <: T}{Σ ⊢ S^{I} <: T^{r}}
\frac{I ∈ \{b, w\} Σ ⊢ T <: S}{Σ ⊢ S^{I} <: T^{w}}  \frac{Σ ⊢ S_{i} <: T_{i} i ∈ 1..n}{Σ ⊢ [ ℓ_{1} S_{1}..ℓ_{n} S_{n}] <: [ ℓ_{1} T_{1}..ℓ_{n+m} T_{n+m}]}
\frac{Σ ⊢ S_{i} <: T_{i} ∀i ∈ 1..n}{Σ ⊢ ⟨S_{1}..S_{n}⟩ <: ⟨T_{1}..T_{n}⟩}  \frac{−}{Σ, S <: T, Σ′ ⊢ S <: T}

\frac{Σ, μ(X)S <: T ⊢ S\{^{μ(X)S}/_{X}\} <: T}{Σ ⊢ μ(X)S <: T}  \frac{Σ, S <: μ(X)T ⊢ S <: T \{^{μ(X)T}/_{X}\}}{Σ ⊢ S <: μ(X)T}

Process typing:

\frac{−}{Γ ⊢ 0}  \frac{Γ ⊢ P Γ ⊢ Q}{Γ ⊢ P |Q}  \frac{Γ ⊢ P}{Γ ⊢ !P} \frac{Γ, x:S^{I} ⊢ P}{Γ ⊢ (νx:S^{I})P}

\frac{Γ ⊢ p : S^{w} Γ ⊢ w : S Γ ⊢ P}{Γ ⊢ \overline{p}w.P}  \frac{Γ ⊢ v : ⟨T_{1}..T_{n}⟩ Γ, x_{1}:T_{1}, … x_{n}:T_{n} ⊢ P}{Γ ⊢ let x_{1}..x_{n} = v in P}
\frac{Γ ⊢ p : S^{r} Γ, x:S ⊢ P}{Γ ⊢ p(x).P}  \frac{Γ ⊢ v : [ ℓ_{1} T_{1}..ℓ_{n} T_{n}] for each i, Γ, x_{i}:T_{i} ⊢ P_{i}}{Γ ⊢ case v of [ ℓ_{1} (x_{1}) ⊳ P_{1}; …; ℓ_{n} (x_{n}) ⊳ P_{n}]}

Value typing:

\frac{Γ(p) = T}{Γ ⊢ p : T}  \frac{Γ ⊢ v : S S <: T}{Γ ⊢ v : T}  \frac{Γ ⊢ v : T}{Γ ⊢ ℓ v : [ℓ T]}  \frac{Γ ⊢ v_{i} : T_{i} ∀i ∈ 1..n}{Γ ⊢ ⟨x_{1}..x_{n}⟩ : ⟨T_{1}..T_{n}⟩}

Table 2: Subtyping and typing for the π-calculus

is that it can be uniformly defined on different calculi, for it requires of the calculus little more than a notion of reduction – the τ-step of the π-calculus.

Barbed congruence is defined as the congruence induced by barbed bisimulation. We write P ⇓_{p} if P is observable at p, that is P can accept an input or an output communication with the environment along p; formally P ⇓_{p} is true if P ⟹^{μ} P′, for some P′ and μ where μ is an input or output action at p.

Definition 1 (barbed bisimulation and congruence) Barbed bisimulation is the largest symmetric relation . ≈ on processes s.t. P . ≈ Q implies:

1. whenever P ⟹ P′ then there exists Q′ such that Q ⟹ Q′ and P′ . ≈ Q′;

2. for each name p, P ⇓_{p} iff Q⇓_{p}.

Two processes P and Q are barbed congruent, written P ≈ Q, if C[P] . ≈ C[Q] for all contexts C.

In an untyped calculus, no contraint is made on processes or contexts. In a typed setting, process compared should have the same type, and should only be tested in contexts which respect such a type. We write P ≈_{Γ} Q if Γ ⊢ P, Q and C[P] . ≈ C[Q] holds, in all contexts that respect Γ. We omit the formal definitions of the typed relations.

Barbed congruence requires a quantification over all contexts. Therefore proving process equalities can be heavy. Against this, it is important to have powerful proof techniques. One such a technique consists in using labeled bisimilarities whose definition does not require context quantification. For instance, in the untyped π-calculus barbed congruence can be recovered using the wellknown early labeled bisimilarity. Its typed version, typed early labeled bisimulation is studied by Boreale and Sangiorgi [5]. These techniques of labeled bisimilarities can be made more powerful by combining then with up-to techniques, like “up to parallel composition” and “up to injective substitutions”.

4 The interpretation

To understand the π-calculus interpretation, it may be helpful to see first an intermediate interpretation into the Higher-Order π-calculus (HOπ) [23], an extension of the π-calculus where arguments of communications and recursive definitions may be, besides names, also abstractions, i.e., parameterised processes. For the interpretation of IOC, we only need abstractions in recursive definitions. More precisely, we need certain parameters of recursive definitions to be functions from names to processes. An example of such a recursive definition is

K(f, p) =^{def} p(x).(f⟨p⟩|K⟨f, x⟩)

Here, f is a function parameter, and p a name parameter; f⟨p⟩ is the process obtained by applying function f to name p. We write functions from names to processes using a lambda notation, like in λ(x, y).P. The interpretation into HOπ is shown in Table 3. We have omitted the type annotations.^{1}.

The translation {[a]}_{p} of an IOC term a is located at a channel p. When a is an object value, with methods l_{i} (i ∈ 1..n), its translation is a process whose first action is to signal its valuehood by providing an access s to its value-core, which is a process of the form OB⟨f_{1} … f_{n}, s⟩. This process is ready to accept along the access name s requests of selection, update and cloning for the methods l_{j}. The body of a method l_{j} is the function f_{j}; the set of these functions form the state of OB⟨f_{1} … f_{n}, s⟩.

We explain the behaviour of OB⟨f_{1} … f_{n}, s⟩ on operations of selection, update and cloning. In case of a select operation l_{j} sel p (which reads “activate method l_{j} and use p as location for the resulting object”) the body f_{j} of method l_{j} is activated, with arguments ⟨s, p⟩; argument s, the access name

1We are omitting type annotations for ease of reading; they would be however necessary to make the definition formal. Types are taken into account in the interpretations into the π-calculus in Table 4

\{[[l_{i}=ς(x_{i})b_{i} ^{i∈1..n}]]\}_{p} =^{def} (νs)(\overline{p}s | OB⟨λ(x_{1}, r).\{[b_{1}]\}_{r}, …, λ(x_{n}, r).\{[b_{n}]\}_{r}, s⟩)
\{[a.l_{j}]\}_{p} =^{def} (νq)(\{[a]\}_{q} | q(x).\overline{x}l_{j} sel p)
{[a.l_{j}⇐ς(x_{j})b]}_{p} =^{def} (νq)({[a]}_{q} | (νb)q(x).
\overline{x}l_{j} upd ⟨p, λ(x_{j}, r).\{[b]\}_{r}⟩)
\{[x]\}_{p} =^{def} \overline{p}x
\{[clone(a)]\}_{p} =^{def} (νq)(\{[a]\}_{q} | q(x).\overline{x}clone p)
{[let x = a in b]}_{p}^{E} =^{def} (νq)({[a]}_{q} | q(x).{[b]}_{p})

where OB is so defined:

OB(f_{1} … f_{n}, s) =^{def}

s[_{j∈1..n} l_{j} [ \begin{matrix}sel (x) ⊳ f_{j}⟨s, x⟩ | OB⟨f_{1} … f_{n}, s⟩; \\ upd (x, y) ⊳ x̄s | OB⟨f_{1} … f_{j−i}, y, f_{j+1} … f_{n}, s⟩ & ]; \end{matrix} clone (x) ⊳ OB⟨f_{1} … f_{n}, s⟩ | (νs′)(x̄s′ | OB⟨f_{1} … f_{n}, s′⟩)]

Table 3: The intermediate translation into HOπ (sketch)

of the value-core OB⟨f_{1} … f_{n}, s⟩, represents the self-parameter. An update request l_{j} upd ⟨p, f⟩ (which reads “replace current method body for l_{j} with f, and use p as the location of the resulting object”) results in a side effect on OB, whereby the j-th component of its state is updated to f. In a clone request clone p (which reads “create a copy of the current object with location p”), a new object is created that has the same value-core OB⟨f_{1} … f_{n}, s⟩. Note the recursive definition of OB⟨f_{1} … f_{n}, s⟩, that shows that OB⟨f_{1} … f_{n}, s⟩ may accept arbitrarily many requests at s.

Now, following the translation of HOπ into π-calculus [23], we can turn the previous interpretation into a π-calculus one. For this, it suffices to make a recursive call with a functional argument, like K⟨λx.P ⟩, into a first-order recursive call whose argument is a pointer to the function, like in:

(νb)(K⟨b⟩|!b(x).P)

Correspondingly, a function application becomes an output of the arguments of the function along the pointer to the function. The result of this transformation, with the addition of type annotations, is presented in Table 4.

As for interpretation of Object Calculi into the λ-calculus [2], so our translation of terms has an environment E as parameter in order to put the necessary type annotations in the translation of method selection. This parameter could be avoided by having, for instance, more type information on the syntax of method selection. We assume that p, q, r, b, s … are not IOC variables.

In the remainder of the paper, we shall call processes of the form OB^{A}⟨b_{1} … b_{n}, s⟩ an object manager (in the interpretation of an object, OB^{A}⟨b_{1} … b_{n}, s⟩ acts like an administrator for the object; it “owns” the object methods, in the sense that it is the only process which can reach them, via names b_{i}’s).

\{[[l_{i}=ς(x_{i}:A)b_{i} ^{i∈1..n}]]\}_{p}^{E} =^{def} (νs:\{[A]\}^{b})(\overline{p}s | (νb_{i}:T_{A,i}^{b} ^{i∈1..n})(OB^{A}⟨b_{1} … b_{n}, s⟩ |

∏_{j∈1..n}!b_{j}(x_{j}, r).{[b_{j}]}_{r}^{E,x_{j}:A}))

\{[a.l_{j}]\}_{p}^{E} =^{def} (νq:\{[[l_{j} : B_{j}]]\}^{w^{b}})(\{[a]\}_{q}^{E} | q(x).\overline{x}l_{j} sel p)
{[a.l_{j} ⇐ ς(x_{j}:A).b]}_{p}^{E} =^{def} (νq:{[A]}^{w^{b}})({[a]}_{q}^{E} | (νb:T_{A,j}^{b})q(x).

(\overline{x}l_{j} upd ⟨p, b⟩ | !b(x_{j}, r).\{[b]\}_{r}^{E,x_{j}:A}))

\{[x]\}_{p}^{E} =^{def} \overline{p}x
\{[clone(a)]\}_{p}^{E} =^{def} (νq:\{[A]\}^{w^{b}})(\{[a]\}_{q}^{E} | q(x).\overline{x}clone p)
{[let x:A = a in b]}_{p}^{E} =^{def} (νq:{[A]}^{w^{b}})({[a]}_{q}^{E} | q(x).{[b]}_{p}^{E,x:A})

The object manager OB^{A} is so defined:

OB^{A}(b_{1}:T_{A,1}^{w} … b_{n}:T_{A,n}^{w}, s:{[A]}^{b}) =^{def}

s[_{j∈1..n} l_{j} [ \begin{matrix}sel (x) ⊳ b̄_{j}⟨s, x⟩ | OB^{A}⟨b_{1} … b_{n}, s⟩; \\ upd (x, y) ⊳ x̄s | OB⟨b_{1} … b_{j−i}, y, b_{j+1} … b_{n}, s⟩ & ]; \end{matrix} clone (x) ⊳ OB^{A}⟨b_{1} … b_{n}, s⟩ | (νs′ : \{[A]\}^{b})(x̄s′ | OB^{A}⟨b_{1} … b_{n}, s′⟩)]

and where

• A = [l_{j} : B_{j}] and T_{A,j} =^{def} ⟨{[A]}^{w}, {[B_{j}]}^{w^{w}}⟩

• in the encoding of selection, B_{j} is the unique type s.t. E ⊢ a:[…, l_{j}:B_{j}, …] holds, if one such judgement exists (the unicity of this type if a consequence of the minimum-type property of IOC), B_{j} can be any type otherwise;

• in the rule for update, x does not occour free in b.

Table 4: The interpretation of IOC into π-calculus

Finally we need to show how to translate types. The translation of an object type must be a type that specifies a repeated selection, update and clone operations.

\{[[l_{j}:B_{j} ^{j∈1..n}]]\} =^{def} μX.[_{j∈1..n} l_{j} [ \begin{matrix}sel \{[B_{j}]\}^{w^{w}}; \\ upd ⟨X^{w^{w}}, ⟨X^{w}, \{[B_{j}]\}^{w^{w}}⟩^{w}⟩ & ]; \end{matrix} clone X^{w^{w}} ]

The pattern of occurrences of w tags is determined by the protocol which implements select and update operations. What is important, however, is the level of nesting of w tags: An even number of nesting gives covariance, whereas an odd number of nesting gives contravariance. Thus, the component {[B_{j}]} is in covariant position on selection, and in contravariance position on update: This explains the invariance of object types on the common components, in rule (OSub Obj) (the interpretation of IOC into the λ-calculus [2] does the same). Type environments are then interpreted componetwise:

\begin{matrix}\{[∅]\} & =^{def} & ∅ \\ \{[E, x:A]\} & =^{def} & \{[E]\}, x:\{[A]\}^{w} \end{matrix}

5 Simplifying the imperative part of the encoding

In the interpretation of IOC in Section 4, the key process is the object manager OB. This process is given as a recursive definition in which certain parameters may change during time. Having a state, this processes may be regarded as “imperative”. In this section we modify the encoding, so that the only imperative processes are cell-like processes, each of which just stores a name. All remaining processes will be stateless, and therefore may be regarded as “functional”. We thus obtain a clean separation of the interpretation into a functional part and a very simple imperative part. Technically, this factorisation allows us take full advantage of various π-calculus proof techniques for functional names and functional processes, discussed below.

A π-calculus name is functional if its response to incoming messages does not change over time. Typically, a name a is functional if it only appears in subexpressions of the form (νa)(!a(p).P |Q) where P and Q only possess the output capability on a, or of the form (νa)(a(p).P |Q) if, in addition, a can only be used once in output. (In [25] names obeying these constraints are called uniformly receptive.)

Functional names have advantages. First, they can be implemented more efficiently than arbitrary names as done, for instance, in the language PICT [22]. Another advantage of functional names is their algebraic properties, among which copying or distributivity laws like

(νa)(!a(b).P |Q|R) = (νa)(!a(b).P |Q) | (νa)(!a(b).Q|R),

whose effect is to localise computation. Another property is τ-insensitiveness: Interactions along a functional name may not affect a process behaviour. As a consequence, when comparing the behaviour of two processes there are fewer configurations to take into account. Let us call a process functional if all inputs made by the process during its lifetime are at functional names. Functional languages (the λ-calculus, the Functional Object Calculus FOC) may be interpreted into a sublanguage of the π-calculus in which all processes are functional.

The new, factorised, encoding is defined in Table 5. To enhance readability we drop types, as they are the same as in the previous encoding. Only the clause for evaluated objects changes. Previously, the access name of the methods was part of (the state of) the object manager. By contrast, now a level of indirection is introduced, such that when updating a method, the indirection, instead of the object manager, changes; this way the object manager becomes functional.

A cell Cell⟨ι, n⟩ stores a pointer n to a method; and can be accessed for read and write operations at ι. The cells are the only imperative processes in the encoding. Being imperative, a cell may be shared by several clients, but may not be copied among them. By contrast, all other resources are functional and they may be copied among their clients. The copy operator Copy is used to create new cells in a clone operation.

This factorised encoding is less compact, but has a simpler correctness proof, than the previous encoding of Section 4. In the next section, we use this factorised encoding for proving the correctness of the original one.

6 Correctness of the interpretation

6.1 Correctness of the interpretation of types

Theorem 2 (correctness for subtyping) For all A, B, it holds that ⊢ A ≤ B iff ∅ ⊢ {[A]} ≤ {[B]}.

Theorem 3 (correctness on type judgements)

1. If E ⊢ a:A then, for all p, it holds that {[E]}, p:{[A]}^{w^{w}} ⊢ {[a]}_{p}^{E}.

2. If {[E]}, p:[[A]]^{w^{w}} ⊢ [[a]]_{p}^{E}, then E ⊢ a:A.

6.2 Operational correctness

We first prove the operational correctness of the factorised encoding of Section 5; then we relate this encoding to the original one of Section 4.

Operational correctness of the factorised encoding. The proof of the correctness of the interpretation w.r.t. Abadi-Cardelli operational semantics has a few tricky points. First of all we need to extend the translation to deal with configurations (objects plus stores plus stacks) in the semantics. We therefore need to add translations of stores (σ), stacks (S) and values (v). We found it quite difficult to make such an extension of the original encoding {[−]} of Section 4, due to sharing of closures. We solve this problem by using instead the factorised encoding [[−]] Below, we let ι̃ denote ι_{1} … ι_{n}, and ι̃′ denote ι′_{1} … ι′_{n}.

[[[l_{i}=ς(x_{i}:A)b_{i} ^{i∈1..n}]]]_{p} =^{def} (νs)(p̄s | (νι̃)(OB_{f}⟨ι_{1} … ι_{n}, s⟩ |

∏_{i∈1..n}(νb_{i})(Cell⟨ι_{i}, b_{i}⟩ |!b_{i}(x_{i}, r).[[b_{i}]]_{r})))

The other clauses are as for the original translation in Table 4.

The object manager is now defined thus:

OB_{f}(ι̃, s) =^{def}

!s[_{i∈1..n} l_{i} [ \begin{matrix}sel (x) ⊳ (νg)(\overline{ι_{i}}read g.g(m).\overline{m}⟨s, x⟩); \\ upd (x, y) ⊳ \overline{ι_{i}}write y.\overline{x}s) & ]; \end{matrix} clone (x) ⊳ (νι̃′, s′)(OB_{f}⟨ι̃′, s′⟩ | Copy^{n}⟨ι̃, ι̃′, x, s′⟩) ]

where Cell(ι, m) and Copy^{n} (n ≥ 0) are so defined:

Cell(ι, m) =^{def} ι[ \begin{matrix}read (x) ⊳ \overline{x}m | Cell⟨ι, m⟩; \\ write (y) ⊳ Cell⟨ι, y⟩] \end{matrix}

Copy^{n}(ι̃, ι̃′, x, s) =^{def} (νg)\overline{ι_{n}}read g.g(m).(Cell⟨ι′_{n}, m⟩ | Copy^{n−1}⟨ι̃, ι̃′, x, s⟩)
Copy^{0}(ι̃, ι̃′, x, s) =^{def} \overline{x}s

Table 5: The factorised encoding

of Section 5. A location ι of a store holds a method closure (which is a method together its stack); we translate it using a cell located at ι that holds the address of the method closure (which is the translation of the method together with a private stack).

[[∅]] =^{def} 0
[[ι↦ ⟨ς(x)b, S⟩ : σ]] =^{def} (νdom(S), m)(Cell⟨ι, m⟩ | !m(x, r).[[b]]_{r} | [[S]]) | [[σ]]

A stack binds values to variables, so we translate it as an object manager located on the variable name.

[[∅]] =^{def} 0
[[x↦ [l_{i}=ι_{i} ^{i∈1..n}] : S]] =^{def} OB_{f}⟨ι_{1} … ι_{n}, x⟩ | S

We have two types of configurations in the operational semantics for Imperative Object Calculus; initial configurations on the form σ · S ⊢ a and final configurations on the form v · σ. They are translated as follows:

[[σ · S ⊢ a]]_{p} =^{def} (νdom(σ))([[σ]] | (νdom(S))([[S]] | [[a]]_{p}))
[[[l_{i}=ι_{i} ^{i∈1..n}] · σ]]_{p} =^{def} (νs, dom(σ))(p̄s | OB_{f}⟨ι_{1} … ι_{n}, s⟩ | [[σ]])

That is, in both cases we simply translate each component of the configurations and appropriately hide their access. Below, ∼ is the strong version of barbed congruence.

Theorem 4 If σ · S ⊢ a ⇝ v · σ′ then: [[σ · S ⊢ a]]_{p} ⟹_{d} ∼ [[v · σ′]]_{p}.

Lemma 5 Suppose a is well-typed. If a⇑ then [[∅ · ∅ ⊢ a]]_{p} has an infinite

computation [[∅ · ∅ ⊢ a]]_{p} \overline{}^{τ} _{d} P_{1} … \overline{}^{τ} _{d} P_{n} \overline{}^{τ} _{d} . . ..

Theorem 6 Suppose a is well-typed. If [[∅ · ∅ ⊢ a]]_{p}⇓_{p}, there exists a value v, and a store σ, s.t. σ · S ⊢ a ⇝ v · σ

Relating the original and the factorised encodings. We have not been able to prove that the translations of an IOC object, according to the factorised encoding {[−]} and to the original encoding [[−]] are equated by some known behavioural equivalence of the π-calculus — the factorised encoding yields richer behaviours. However, we have been able to extend the notion of ready simulation [4, 13] to the π-calculus and prove that the two translations of an object are in a ready simulation relation. This is a rather weak result, but, together with the correctness of the factorised encoding, it will suffice to prove the operational correctness of the original encoding.

Definition 7 (Ready simulation) Ready simulation is the largest relation ≺ s.t. P ≺ Q implies:

1. If P \overline{}^{μ} P′; then there exist a Q′ s.t. Q ⟹^{μ̂} Q′ and P′ ≺ Q′. With ⟹^{μ̂} =^{def}⟹ if μ = τ and ⟹^{μ} otherwise.

2. If Q \overline{}^{μ} ; then P ⟹^{μ}.

Theorem 8 {[a]}_{p} ≺ [[∅ · ∅ ⊢ a]]_{p}.

Lemma 9 Suppose a is well-typed. Then {[a]}_{p} cannot deadlock, i.e. whenever \{[a]\}_{p} ⟹ P then there are μ, P′ s.t. P \overline{}^{μ} P′.

Proof. Assume that {[a]}_{p} can deadlock, that is there exists a P such that {[a]}_{p} ⟹ P ↛^{μ}. Now since {[a]} ≺ [[∅ · ∅ ⊢ a]]_{p} there must exist a Q such that [[∅ · ∅ ⊢ a]]_{p} ⟹ Q with P ≺ Q.

By Theorem 4 if a converges then [[∅ · ∅ ⊢ a]]_{p} will also converge and by Lemma 5 if a diverges then [[∅ · ∅ ⊢ a]]_{p} will also diverge; so [[∅ · ∅ ⊢ a]]_{p} cannot deadlock. Then there must exist a μ s.t. Q \overline{}^{μ} . By the second clause of the definition of ready simulation we infer P ⟹^{μ}, which is a contradiction. □

Corollary 10 Suppose a is well-typed.

• {[a]}_{p}⇑ iff [[∅ · ∅ ⊢ a]]_{p}⇑

• {[a]}_{p}⇓ iff [[∅ · ∅ ⊢ a]]_{p}⇓

Proof. Both {[a]}_{p} and [[∅·∅ ⊢ a]]_{p} are deadlock-free. Then the corollary follows from Theorem 8 and the fact that [[∅ · ∅ ⊢ a]]_{p} either converges or diverges (it cannot do both, because of Theorem 4 and Lemma 5). □

Adequacy and soundness of the original interpretation. From Theorems 4 and 6 and Corollary 10, we infer:

Corollary 11 (computational adequacy) If ∅ ⊢ a : A for some type A, then a⇓ iff {[a]}_{p}⇓_{p}.

Behavioural equivalences like barbed congruence or the Morris-style contextual equivalence can also be defined in IOC (in fact, on IOC the two equivalences coincide). We write a ≃_{B} b if a and b are closed terms of IOC of type B and are barbed congruent.

We can show soundness of the translation using compositionality of the encoding and adequacy. This tells us that the equalities that can be proven using the translation are valid equalities.

Theorem 12 (soundness) Assume a:A and b:A. If {[a]}_{p} ≈_{p:{[A]}^{w^{w}}} {[b]}_{p} then a ≃_{A} b.

As for the encodings of the λ-calculi into π-calculus, so in the case of IOC the converse of soundness does not hold.

7 Comparisons with the interpretation of FOC

In their book, Abadi and Cardelli consider not only the imperative, but also the functional paradigm for Object Calculi. In this section we briefly compare the (first-order) Imperative and Functional Object Calculi, and their encodings into the π-calculus. The syntax of the Functional Object Calculus (FOC) is the same as for the imperative except that we do not have the the let and clone constructs. The operational semantics, however, is very different. In the functional case, stores and stacks are not necessary and a simple reduction semantics can be given, using the rules below, where a = [l_{i}=ς(x_{i}:A_{i})b_{i} ^{i∈1..n}]:

\begin{matrix}a.l_{k} ⇝ b_{k}\{^{a}/_{x_{k}}\} & (k ∈ 1..n) \\ a.l_{k}⇐ς(x:A)b ⇝ [l_{k}=ς(x:A)b, l_{i}=ς(x_{i}:A_{i})b_{i} ^{i∈1..n\\{k\}}] & (k ∈ 1..n) \end{matrix}

As a consequence of the differences in the operational semantics, certain basic laws of FOC, like a.l_{k} = b_{k}{^{a}/_{x_{k}}} (k ∈ 1..n), do not hold in IOC.

In [24] FOC is translated onto the same typed π-calculus we use in this paper. Remarkably, despite the strong differences in the operational semantics, the interpretations of IOC and FOC into the π-calculus are structurally very close. Roughly, the only difference between the two translations is in the object manager. The FOC manager, reported below, is a functional process (it is replicated, see the discussion on functional processes in Section 5). This difference has consequences on the update requests: On such a request, the FOC manager always generates a new object manager, whereas the IOC manager works by having side effect on itself.

OB^{A}(b_{1}:T_{A,1}^{w} … b_{n}:T_{A,n}^{w}, s:{[A]}^{b}) =^{def}

!s[_{j∈1..n} l_{j} [ \begin{matrix}sel (x) ⊳ b̄_{j}⟨s, x⟩; \\ upd (x, y) ⊳ (νs′:\{[A]\}^{b})(\overline{x}s′ | OB⟨b_{1} … b_{j−i}, y, b_{j+1} … b_{n}, s′⟩) & ]] \end{matrix}

The functional and the imperative nature of, respectively, FOC and IOC, is reflected in the functional and the imperative nature of the object managers of the π-calculus interpretations. The commonalities between the interpretations of FOC and IOC allow us to reuse certain proofs, most notably those on types (see Theorem 2 and 3), but also certain proofs about behavioural properties of objects (a good example of this is the proof of the law (Eq Sub Obj), in Section 8).

8 Reasoning about objects

In this section we give some examples of how the π-calculus interpretation can be used to validate some basic behavioural properties of IOC.

Lemma 13 Let o = [l_{i}=ς(x_{i}:A)b_{i} ^{i∈1..n}], A = [l_{i}:B_{i} ^{i∈1..n}], and o:A. Then

1. o.l_{j} ≃_{B_{i}} let x_{j}:A = o in b_{j}

2. If x:A ⊢ b:B_{j} then o.l_{j}⇐ς(x:A)b ≃_{A} [l_{j}=ς(x:A)b, l_{i}=ς(x_{i}:A)b_{i} ^{i∈1..n\{j}}]

3. clone(o) ≃_{A} o

4. If a⇓, a:B, b:C x ∉ fv(b), then let x:B = a in b ≃_{C} b.

5. If x ∉ fv(o), y ∉ fv(a), a:B and (let x:B = a in let y:A = o in b) : C, then

(let x:B = a in let y:A = o in b) ≃_{C} (let y:A = o in let x:B = a in b)

6. (law ( Eq Sub Object)): If m ≥ n, then o ≃_{A} [l_{i}=ς(x_{i}:B)b_{i} ^{i∈1..m}].

Laws 1-5 can be validated using the theory of the untyped π-calculus. For instance, using laws such as the expansion law, (νp)(p(x).P | \overline{p}v.Q) ≈ (νp)(P \{^{v}/_{x}\}|Q) and (νp)(!p(x).P |Q) ≈ Q if p is not free in Q, we can prove law (5) as follows.

{[let y = o in let x = a in b]}_{p}

= (νq)((νs, b_{1} … b_{n})(\overline{q}s | OB⟨b_{1} … b_{n}, s⟩ | ∏_{i∈1..n}!b_{i}(x_{i}, r).\{[b_{i}]\}_{r}) |

q(y).(νq′)([[a]]_{q′} | q′(x).{[b]}_{p}))

≈ (νq′)({[a]}_{q′} | q′(x).(νs, b_{1} … b_{n})({[b]}{^{s}/_{y}} | OB⟨b_{1} … b_{n}, s⟩ |

∏_{i∈1..n}!b_{i}(x_{i}, r).{[b_{i}]}_{r}))

≈ (νq′)([[a]]_{q′} | q(x).(νq)((νs)(\overline{q}s | OB⟨b_{1} … b_{n}, s⟩ |

∏_{i∈1..n}!b_{i}(x_{i}, r).{[b_{i}]}_{r}) | q(y).{[b]}_{p}))

= {[let x = a in let y = o in b]}_{p}

It is interesting to look at the difference between FOC and IOC on objects of the form o.l_{j}, for o = [l_{i}=ς(x_{i}:A)b_{i} ^{i∈1..n}] (j ∈ 1..n), using the π-calculus interpretations of FOC and IOC . In the case of FOC, o is interpreted as a functional process and we can therefore apply copy laws to derive {[o.l_{j}]}_{p} ≈ {[b_{j}{^{a}/_{x_{j}}}]}_{p}. By contrast, in the case of IOC, object o is interpreted as a process with a state, and we can only infer {[o.l_{j}]}_{p} ≈ {[let x_{j}:A = o in b_{j}]}_{p}, as by Lemma 13(1).

Law (Eq Sub Object) of Lemma 13 can be validated using the typed labeled bisimulation technique. Roughly, a typed bisimulation relations consists of triples (Γ, P, Q), and (Γ, P, Q) being in a typed bisimulation means that P and Q are undistinguishable by an observer whose use of names respect the type informations in Γ. We describe a typed bisimulation for proving (Eq Sub Object). Having fixed a and b, their translations are:

[[a]]_{p} = (νs:[[A]]^{w})(\overline{p}s | (νb_{i}:T_{A,i}^{b} ^{i∈1..n})(OB^{A}⟨s, b_{1} … b_{n}⟩ | ∏_{i∈1..n}!b_{i}(x_{i}, r).[[b_{i}]]_{r}))
[[b]]_{p} = (νs:[[A′]]^{w})(\overline{p}s | (νb_{i}:T_{A,i}^{b} ^{i∈1..m})(OB^{A′}⟨s, b_{1} … b_{m}⟩ | ∏_{i∈1..m}!b_{i}(x_{i}, r).[[b_{i}]]_{r}))

Now, let Γ′ = s:[[A]]^{w}, b_{1}:T_{A,1}^{r}, …, b_{n}:T_{A,n}^{r} and Γ′′ = p:[[A]]^{w^{r}}, b_{1}:T_{A,1}^{r}, …, b_{n}:T_{A,n}^{r}.

where T_{A,j} =^{def} ⟨{[A]}^{w}, {[B_{j}]}^{w^{w}}⟩. Consider the relation consisting of these two triples:

1)  (Γ′, OB^{A}⟨b_{1} … b_{n}, s⟩,

(νb_{i}:T_{A,i}^{b} ^{i∈n+1..m})(OB^{A′}⟨b_{1} … b_{m}, s⟩ | ∏_{i∈n+1..m}!b_{i}(x_{i}, r).[[b_{i}]]_{r}))

2)  (Γ′′, (νs:[[A]]^{w})(p̄s | OB^{A}⟨b_{1} … b_{n}, s⟩,

(νs:[[A′]]^{w})(νb_{i}:T_{A,i}^{b} ^{i∈n+1..m})(p̄s | OB^{A′}⟨b_{1} … b_{m}⟩ | ∏_{i∈n+1..m}!b_{i}(x_{i}, r).[[b_{i}]]_{r}))

This relation is typed bisimulation up to parallel composition and up to injective substitutions.

This is the first proof of (Eq Sub Object) for IOC we are aware of. The proof can be easily adapted to the analogous law for FOC.

9 Extensions and further work

Our interpretation of IOC can be extended to accommodate other type features discussed in [1], like variant tags, recursive types, polymorphic types. Variant tags are tags on method names which allow only selection or update operations on a method, so to have a richer subtyping relation. These tags yield the same form of subtyping on IOC types as that induced by the tags {r, w, b} on the πcalculus types. We can capture them with a simple refinement of the encoding of types. For recursive types, we just map type variables of a IOC type to type variables of the π-calculus types. Similarly, is possible to handle polymorphic types, using polymorphic extensions of the π-calculus [26].

The extensibility of the interpretation of imperative objects, and its resemblance to the interpretation of functional objects, suggests that the representation of objects into the π-calculus is a robust one, and that it could be used for giving the semantics to, and proving properties of, a wide range of objectoriented languages, possibly combining imperative, functional and concurrent features. We have began examining the case of Obliq [6], which has imperative objects and constructs for concurrency and distribution.

We hope the study of the Object Calculi from within the π-calculus will help to develop concurrent or distributed versions of the Object Calculi.

An interesting and challenging question is finding a direct characterisation of the equivalence induced on IOC terms by the encoding into the π-calculus (where two IOC terms are equated if their process translations are behaviourally equivalent).

References

[1] M. Abadi and L. Cardelli. A Theory of Objects. Monographs in Computer Science. Springer Verlag, 1996.

[2] M. Abadi, L. Cardelli, and R. Viswanathan. An interpretation of Objects and Objects Types. In Proc. 23th POPL. ACM Press, 1996.

[3] L. Aceto, H. Hüttel, A. Ingólfsdóttir, and J. Kleist. Relating semantic models for the object calculus. In Proceedings of Express 97 Workshop, volume 7 of Electronic Notes in Theoretical Computer Science. Elsevier Science B.V., 1997.

[4] B. Bloom, S. Istrail, and A. R. Meyer. Bisimulation can’t be traced. Journal of the Association for Computing Machinery, 42(1):232–268, Jan. 1995.

[5] M. Boreale and D. Sangiorgi. Bisimulation without matching. To appear.

[6] L. Cardelli. Obliq — a language with distributed scope. Research report 122, Digital Equipment Coporation, Systems Research Center, 1994.

[7] A. D. Gordon, P. D. Hankin, and S. B. Lassen. Compilation and equivalence of imperative objects. In Proceedings of 17th FST&TCS Conference, 1997.

[8] A. D. Gordon and G. D. Rees. Bisimilarity for a first-order calculus of objects with subtyping. In Proceedings of the Twenty-Third Annual ACM Symposium on Principles of Programming Languages, 1996.

[9] K. Honda. Composing processes. In Proc. 23th POPL. ACM Press, 1996.

[10] H. Hüttel and J. Kleist. Objects as mobile processes. Technical report RR-96-38, BRICS - Basic Research in Computer Science, 1996.

[11] C. Jones. A π-calculus semantics for an object-based design notation. In E. Best, editor, Proc. CONCUR ’93, volume 715 of Lecture Notes in Computer Science, pages 158–172. Springer Verlag, 1993.

[12] N. Kobayashi, B. Pierce, and D. Turner. Linearity and the pi-calculus. In Proc. 23th POPL. ACM Press, 1996.

[13] K. G. Larsen and A. Skou. Bisimulation through probabilistic testing. Information and Computation, 94(1):1–28, Sept. 1991.

[14] X. Liu and D. Walker. Partial confluence of processes and systems of objects. Submitted for publication, 1996.

[15] I. A. Mason and C. L. Talcott. Equivalence in functional languages with effects. Journal of Functional Programming, 1(3):287–327, 1991.

[16] R. Milner. Communication and Concurrency. Prentice Hall, 1989.

[17] R. Milner. The polyadic π-calculus: a tutorial. Technical Report ECS– LFCS–91–180, LFCS, Dept. of Comp. Sci., Edinburgh Univ., Oct. 1991. Also in Logic and Algebra of Specification, ed. F.L. Bauer, W. Brauer and H. Schwichtenberg, Springer Verlag, 1993.

[18] R. Milner, J. Parrow, and D. Walker. A calculus of mobile processes, (Parts I and II). Information and Computation, 100:1–77, 1992.

[19] R. Milner and D. Sangiorgi. Barbed bisimulation. In W. Kuich, editor, 19th ICALP, volume 623 of Lecture Notes in Computer Science, pages 685–695. Springer-Verlag, 1992.

[20] A. Philippou and D. Walker. On transformations of concurrent object programs. In Proc. CONCUR ’96, Lecture Notes in Computer Science, pages 131–147. Springer Verlag, 1996.

[21] B. Pierce and D. Sangiorgi. Typing and subtyping for mobile processes. In Proceedings of LICS’93, pages 376–385. IEEE Computer Society Press, 1993.

[22] B. C. Pierce and D. N. Turner. Pict: A programming language based on the pi-calculus. Indiana University Technical report, 1997., 1997.

[23] D. Sangiorgi. Expressing Mobility in Process Algebras: First-Order and Higher-Order Paradigms. PhD thesis CST–99–93, Department of Computer Science, University of Edinburgh, 1992.

[24] D. Sangiorgi. An interpretation of typed objects into typed π-calculus. Technical Report RR-3000, INRIA — Sophia Antipolis, 1996.

[25] D. Sangiorgi. The name discipline of uniform receptiveness. In Proceedings of ICALP’97, 1997.

[26] D.N. Turner. The polymorphic pi-calculus: Theory and Implementation. PhD thesis, Department of Computer Science, University of Edinburgh, 1996.

[27] F. Vaandrager. A process algebra semantics of POOL. In Applications of process algebra, volume 17 of Tracts in Theoretical Computer Science, pages 173–236. Cambridge University Press, 1990.

[28] V. Vasconcelos and M. Tokoro. A typing system for a calculus of objects. In Proc. Object Technologies for Advanced Software ‘93, volume 742 of Lecture Notes in Computer Science, pages 460–474. Springer Verlag, 1993.

[29] D. Walker. Objects in the π-calculus. Information and Computation, 116:253–271, 1995.

A Grammar and rules for IOC

Syntax:

Type Environments  E ::= ∅ | E, x : A
Types  A, B ::= [l_{i}:B_{i} ^{i∈1..n}]
Method names  l,
Variables  x, y, z
Terms  a, b ::=
x  Variable
| [l_{i}=ς(x_{i}:A)b_{i} ^{i∈1..n}] Object
| a.l  Method activation
| a.l⇐ς(x:A)b  Method override
| clone(a)  Cloning
| let x:A = a in b  Local definition

Operational semantics:

(OC Var)

\frac{σ · S ⊢ ⋄ x ∈ dom(S)}{σ · S ⊢ x ⇝ S(x) · σ}

(OC Obj) where σ′ = (σ, ι_{i}↦ ⟨ς(x_{i})b_{i}, S⟩ ^{i∈1..n})

\frac{σ · S ⊢ ⋄ ι_{i} ∉ dom(σ) ι_{i} distinct ∀i ∈ 1..n}{σ · S ⊢ [l_{i}=ς(x_{i}:A)b_{i} ^{i∈1..n}] ⇝ [l_{i}=ι_{i} ^{i∈1..n}] · σ′}

(OC Sel)

\frac{\begin{matrix}σ · S ⊢ a ⇝ [l_{i}=ι_{i} ^{i∈1..n}] · σ′ σ′(ι_{j}) = ⟨ς(x_{j})b_{j}, S′⟩ \\ x_{j} ∉ dom(S′) j ∈ 1..n σ′ · S′, x_{j}↦ [l_{i}=ι_{i} ^{i∈1..n}] ⊢ b_{j} ⇝ v · σ′′ \end{matrix}}{σ · S ⊢ a.l_{j} ⇝ v · σ′′}

(OC Upd)

\frac{σ · S ⊢ a ⇝ [l_{i}=ι_{i} ^{i∈1..n}] · σ′ j ∈ 1..n ι_{j} ∈ dom(σ′)}{σ · S ⊢ a.l_{j}⇐ς(x:A)b ⇝ [l_{i}=ι_{i} ^{i∈1..n}] · σ′[ι_{j}↦ ⟨ς(x)b, S⟩]}

(OC Clone)

\frac{σ · S ⊢ a ⇝ [l_{i}=ι_{i} ^{i∈1..n}] · σ′ ∀i ∈ 1..n ι′_{i} ∉ dom(σ′) ι′_{i} distinct}{σ · S ⊢ clone(a) ⇝ [l_{i}=ι_{i} ^{i∈1..n}] · (σ′, ι′_{i}↦ σ(ι_{i}) ^{i∈1..n})}

(OC Let)

\frac{σ · S ⊢ a ⇝ v′ · σ′ σ′ · S, x↦ v′ ⊢ b ⇝ v′′ · σ′′}{σ · S ⊢ let x:A = a in b ⇝ v′′ · σ′′}

Subtyping rules:

(OSub Obj) ; \overline{[l_{i}:B_{i} ^{i∈1..n+m}] <: [l_{i}:B_{i} ^{i∈1..n}]}

Typing rules: (the order of assignments in a type environment is ignored)

(OT Subsumption)

\frac{E ⊢ a:A A <: B}{E ⊢ a:B}

(OT var) where x ∈ dom(E)

\frac{E(x) = A}{E ⊢ x:A}

(OT Obj) where A = [l_{i}:B_{i} ^{i∈1..n}]

\frac{E, x_{j}:A ⊢ b_{j}:B_{j} ∀j ∈ 1..n}{E ⊢ [l_{i}=ς(x_{i}:A)b_{i} ^{i∈1..n}] : A}

(OT Sel) where A = [l_{i}:B_{i} ^{i∈1..n}]

\frac{E ⊢ a : [l_{i}:B_{i} ^{i∈1..n}] j ∈ 1..n}{E ⊢ a.l_{j}:B_{j}}

(OT Upd) where A = [l_{i}:B_{i} ^{i∈1..n}]

\frac{E ⊢ a:A E, x:A ⊢ b:B_{j} j ∈ 1..n}{E ⊢ a.l_{j}⇐ς(x:A)b : A}

(OT Clone)

\frac{E ⊢ a:A}{E ⊢ clone(a):A}

(OT Let)

\frac{E ⊢ a:A E, x:A ⊢ b:B}{E ⊢ let x:A = a in b : B}

Recent BRICS Report Series Publications

RS-98-52 Josva Kleist and Davide Sangiorgi. Imperative Objects and Mobile Processes. December 1998. 22 pp. Appears in Gries and de Roever, editors, IFIP Working Conference on Programming Concepts and Methods, PROCOMET ’98 Proceedings, 1998, pages 285–303.

RS-98-51 Peter Krogsgaard Jensen. Automated Modeling of Real-Time Implementation. December 1998. 9 pp. Appears in The 13th IEEE Conference on Automated Software Engineering, ASE ’98 Doctoral Symposium Proceedings, 1998, pages 17–20.

RS-98-50 Luca Aceto and Anna Ingólfsdóttir. Testing Hennessy-Milner Logic with Recursion. December 1998. 15 pp. Appears in Thomas, editor, Foundations of Software Science and Computation Structures: Second International Conference, FoSSaCS ’99 Proceedings, LNCS 1578, 1999, pages 41–55.

RS-98-49 Luca Aceto, Willem Jan Fokkink, and Anna Ingólfsdóttir. A Cook’s Tour of Equational Axiomatizations for Prefix Iteration. December 1998. 14 pp. Appears in Nivat, editor, Foundations of Software Science and Computation Structures: First International Conference, FoSSaCS ’98 Proceedings, LNCS 1378, 1998, pages 20–34.

RS-98-48 Luca Aceto, Patricia Bouyer, Augusto Burgueño, and Kim G. Larsen. The Power of Reachability Testing for Timed Automata. December 1998. 12 pp. Appears in Arvind and Ramanujam, editors, Foundations of Software Technology and Theoretical Computer Science: 18th Conference, FST&TCS ’98 Proceedings, LNCS 1530, 1998, pages 245–256.

RS-98-47 Gerd Behrmann, Kim G. Larsen, Justin Pearson, Carsten Weise, and Wang Yi. Efficient Timed Reachability Analysis using Clock Difference Diagrams. December 1998. 13 pp. To appear in Computer-Aided Verification: 11th International Conference, CAV ’99 Proceedings, LNCS, 1999.

RS-98-46 Kim G. Larsen, Carsten Weise, Wang Yi, and Justin Pearson. Clock Difference Diagrams. December 1998. 18 pp. Presented at 10th Nordic Workshop on Programming Theory, NWPT ’10 Abstracts, 1998. To appear in Nordic Journal of Computing.