Ob jects, Types and Modal Logics
Dan S. Andersen
Lars H. Pedersen Josva Kleist December 13, 1996
Abstract
Hans H ttel
In this paper we present a modal logic for describing properties of terms in the object calculus of Abadi and Cardelli AC96]. The logic is essentially the modal mucalculus of Koz83]. The fragment allows us to express the temporal modalities of the logic CTL BAMP83]. We investigate the connection between the type system Ob1<: and the mucalculus, providing a translation of types into modal formulae and an ordering on formulae that is sound w.r.t. to the subtype ordering of Ob1<: .
1 Introduction
In AC94a, AC94b, AC94c, AC96] Abadi and Cardelli present and investigate several versions of the & calculus, a calculus for describing central features of objectoriented programs, with particular emphasis on various type systems. In this paper we present a modal logic for describing dynamic properties of terms in the object calculus. By dynamic properties we mean properties speci cally related to the behaviour over time of a term. We also examine the relation between the type system with recursive types Ob < for the & calculus and the modal mucalculus Koz83]. It turns out that there are close correspondences between the type system and a fragment of the mucalculus using maximal xedpoints. In particular, there is a sound and complete translation from types to logical formulae preserving typability and
1 :
Address: Dep. of Computer Science, Aalborg University, Frederik Bajersvej 7, 9220 Aalborg, Denmark. Email: fhans,kleistg@cs.auc.dk
1
the subtype ordering, when we interpret subtyping as containment. Phrased di erently, the translation establishes a CurryHowardstyle result in that it allows us to view & calculus terms as realizers of certain mucalculus formulae.
2 The & calculus and its reduction semantics
There are various versions of the & calculus. In this paper we shall consider what is essentially the simple object calculus of AC94b] with booleans added. The set of object terms, Obj, is de ned by the following abstract syntax: objects self variables j method activation j ( method override j j recursive fold/unfold j j j booleans Here xi 2 SVar range over self variables, li 2 MNames range over method names and Ai 2 Types. We let m(a) denote the set of method names and fv(a) the set of free self variables in a. The original presentation of the & calculus uses a smallstep reduction semantics, which is also used in the labelled transition semantics in the following section. Let a = li = & (xi :Ai)bi ]i2I . Then the reduction rules are given by
j
a ::= li = & (xi :Ai )bi]i2I x a:l a:l & (x:A)b fold(A; a) unfold(a) if (a; a; a) true false
(k I ) a:lk ; bk a=xk a:lk & (x:A)b ; li = & (xi :Ai )bi; lk = & (x:A)b]i2I nfkg (k I ) if (true; a ; a ) ; a if (false; a ; a ) ; a unfold(fold(A; a)) ; a The activation of the method lk results in the method body being activated
f g 2 ( 2
1 2 1 1 2 2
with the self variable being bound to the original object. Method override results in an object with the overridden method exchanged with the new method. The reduction order is leftmost; this we express through evaluation contexts (C ]) which have the following abstract syntax (with ] denoting the hole of the context): C ] ::= ]:l j ]:l ( & (x:A)b j unfold( ) j fold( ) j if( ; a ; a )
1 2
2
and an evaluation strategy given by the transition rule
a;b C a] ; C b]
In the labelled transition semantics we will need to talk about objects converging to a value. This notion is of course de ned modulo some notion of value; suppose that we have a wellde ned notion of value, that a is an object and v a value. We then write a + v ( a converges to the value v ) if there is a terminating reduction sequence a ; a ; v. We write a * ( a diverges ) if there is no v such that a + v.
1
3 Types
One of the main motivation for the & calculus is that of studying various type systems of objectoriented programming languages within a uni ed framework. In this paper we shall consider the type system Ob < from AC94b] as presented in GR96].
1 :
The set of Ob < type expressions Type is de ned via the following abstract syntax: A ::= Bool j li:Ai ] j Top j (X )A j X Here Bool denotes the only ground type, namely that of truth values. li:Ai ] denotes an object record type, where the method li has type Ai . Top denotes the most general or unspeci ed type, (X )A is a recursive type and X ranges over TypeVar, the set of type variables.
1 :
3.1 The type language
3.2 Assigning types to objects
1 :
state that the object a has type A under the assumptions in ?, where ? describes typing assumptions of self variables. For instance, ?(x) = A states that we assume that the free self variable x has type A. The type system Ob < also incorporates a notion of subtyping, whose intended informal interpretation is that of capturing some types being more
1 :
Ob < has two kinds of judgments. Type judgments on the form ? a : A,
`
3
general than others. The expression A <: B denotes that A is a subtype of B and thus that objects of type A may be used instead of objects of type B . Subtyping judgments ? ` A <: B state that the type A is a subtype of B , given the subtyping assumptions in ?. Here the typing assumptions in ? describe subtyping constraints on type variables. ?(X ) = E states that we assume X <: E . In order to ensure uniqueness of recursively de ned types Abadi and Cardelli de ne a syntactic predicate of formal contractivity on type variables. A Y should be read as `variable Y is formally contractive in type expression A'. Informally, this means that any occurrence of Y occurs within the scope of a method label in the type expression E . The rules de ning the predicate are shown in Table 1.
X=Y X Y
6
Top
Y
li :Ai] Y
A Y (X )A Y
Table 1: Formal contractivity A type of Ob < is wellformed if it can be formed using the inference rules of Table 2. The subtyping relation is expressed in the inference rules of Table 3. Finally, an object a has type A under assumptions ? if ? ` a:A can be inferred by the type assignment rules in Table 4. An object term a is said to be typable if for some type A we can infer that ; ` a:A.
1 :
Type Object] ? ` Ai 8i 2 I
? ` li :Ai ]i2I
Type top]
? ` Top ? ` (X )A
Type X ]
X 2 dom(?) ?`X
Type Rec] ? X <: Top] ` A A X
Table 2: Wellformed types 4
?`A Sub Re ] ? ` A <: A
Sub X ]
i j Sub obj] K ` L :A2 L <:2 lK:A?] ` Ai ? li i ]i2L j j j 2K
Sub rec]
?(X ) = A ? ` X <: A
< A Sub Trans] ? ` A1 ? :`A2 ? :`A 2 <: A3 A1 < 3
Sub top]
?`A ? ` A <: Top
? ` (X1 )A1 ? ` (X2 )A2 ? X2 <: Top; X1 <: X2 ] ` A1 <: A2 ? ` (X1 )A1 <: (X2 )A2
Table 3: The subtyping relation
4 A labelled transition semantics
The correspondence between object types and modal logic is based on the labelled transition semantics used to interpret logical formulae. As our labelled transition semantics, we shall use that proposed by Gordon and Rees in GR96]. The syntax has been altered very slightly in that boolean values can now appear. Transitions are on the form a  b this transition describes that the object term a admits the observation and then becomes the object term b. In the labelled transition semantics, terms are always annotated with their type. The types of Ob < are divided into two classes, active and passive. Active types are the types of values. Only Bool is active, so in our presentation all values are booleans. Recursive types, object types and Top are passive types. At active types a program must converge to a value before it can be observed; at passive types a program performs observable actions unconditionally, whether or not it converges. The observations, 2 Obs, take the following forms:
1 :
::= true j false j l j l ( & (x)e j unfold
These observations should be interpreted as follows: An object term allows the observation true (resp. false) if the term is of type Bool and has the value true (resp. false.) An object term allows the observation l if it has a method 5
Var]
?(x) = A ? ` x:A
Select]
: ` I A Update] ? ` a:A ? x?A] a:lb:Bj &jx2A)b : A li :Bi ]i2I ` j( ( : A (X )A ? ` a:A A (X )A ? ` a:AfA=X g Unfold] Fold] ? ` fold(A; a) : A ? ` unfold(a) : AfA=X g ? ` a:Bool ? ` a1 ; a2 : A If] Subsump] ? ` a:A1 ? ` A1 <: A2 ? ` if (a; a1 ; a2 ) : A ? ` a : A2
`b i i2I l Object] ? xi :A]? ` i :lB= 8(x :A)b ] A : Ai :Bi ]i2I i & i i i2I
? ` b: li :Bi ]i2I j 2 I ? ` b:lj :Bj
Table 4: Type assignment labelled l. An object term allows the observation l ( & (x)e if the object can have its method labelled l rede ned as & (x)e. And nally, an object term always allows the observation unfold intuitively, this corresponds to `unfolding' the object by substituting self variables by their corresponding objects. The labelled transition semantics is de ned by the minimal family of relations
f

j
2
closed under the rules in Table 5. The notion of bisimulation equivalence is de ned as usual Par81, Mil89]. De nition 1 (Bisimulation) Bisimilarity is the greatest binary relation on & calculus terms that satis es the following: a b if and only if
Act
g
 a0 2. b  b0
1. a
b0 s.t. (b  b0 a0 b0 ) a0 s.t. (a  a0 a0 b0): If a b we say that a and b are bisimilar.
) 9 ^ ) 9 ^
6
Trans Bool] Trans Select]
a v true,false aBool v 0 A li:Ai]i2I j I aA l a:lj A
+ 2 f g 2
j j
Trans Update] A
li:Ai]i2I j I x:A e:Aj e aA l (& x  a:lj & (x:A)eA Trans Unfold] A (X )A  B A A=X ] aA unfold unfold(a)B
2 `
j
( )
(
Table 5: The rules of the labelled transition semantics We sometimes index bisimilarity w.r.t. types, writing a A b if a:A and b:A and a and b are bisimilar. It should be noted, though, that De nition 1 not only relates terms aA and bA on their type A, but also on all of their supertypes. That is, if the subtype relation
A <: B <: B <:
1 2
<: Bn bB
holds, then De nition 1 states that the following must hold:
aA bA
)
aB1 bB1 ; : : : ; aB
n
n
In the following we refer to the bisimulation of De nition 1 as GordonRees bisimulation or bisimulation in the sense of Gordon and Rees.
5 A logic for objects
The logic we shall use is a version of the modal mucalculus Koz83] interpreted over the labelled transition system de ned in the previous section. This logic also corresponds to the HennessyMilner logic of HM85] extended with (local) recursive de nitions Lar90]. 7
5.1 Syntax of formulae
F ::= F
j h
1 _ 2
The set of mucalculus formulae is given by
F F F F true tt false tt tt ff ::= l unfold l & (x)e
j
1 ^ 2
j h j
i
j
]F j X j X:F
j
X:F
i
j h
i
j
j
j
(
Here X ranges over the set of formula recursion variables FormVar. tt and ff are atomic formulae, not to be confused with the boolean values of the & calculus. The modalities of the logic are indexed by the observations from the labelled transition semantics. Intuitively, a formula h iF is true for an object o if o allows some observation such that F is true for the resulting object. Similarly, a formula ]F is true for the object o if all observations of will result in an object for which F is true. A syntactic constraint is imposed on the form of formulae including true and false, as the only way an object can allow a boolean observation is by terminating. We interpret our logic over the labelled transition system of the previous section. If a formula F is true for an object a, we say that a satis es F . The denotation of a formula is the set of object terms that satisfy F . As formulae may contain free variables. the denotation of a formula is seen relative to an environment : FormVar ,! P (Obj) which for a given variable, returns the set of objects which satis es the formula bound to that variable. We can extend operations and predicates on sets of objects to environments. For any two environments ; we write i for all variables we have that (X ) (X ). If S is a set of objects, we write S if for all X we have that (X ) S . Similarly, is the environment such that (X ) = (X ) (X ). The semantics of formula not using the recursion operators can then be de ned as:
1 2 1 2 1 2 1 2 1 2
5.2 Semantics of formulae
tt]] = Obj ff ]] =
;
8
F ]] = F ]] F ]] F ]] = Obj F ]] X ]] = (X ) l F ]] = a b : a l b and b F ]] l]F ]] = a b with a l b : b F ]] l & (x)a F ]] = a b : a l(& x a b and b F ]] l & (x)a]F ]] = a b with a l(& x a b : b F ]] The operators X:F and X:F are local recursion operators. For any recursive formula X:F or X:F we de ne a declaration function (Obj)) (Obj) by F ( ) = F ]] F : (FormVar , Both recursion operators denote a solution to the equation X = F , that is, we want an environment such that X ]] = F ]] . A with this property
1 _ 2 1 2
F
:
n
h i
f
j 9
2
g
f
j 8
2
g
h
(
i
f
j 9
( )
2
g
(
f
j 8
( )
2
g
D
! P
! P
D
is called a model. One may easily show that (FormVar ,! P (Obj); ), the set of environments ordered under inclusion, constitutes a complete lattice and that the function DF is a monotonic function for any recursive formula X:F or X:F . Consequently, Tarski's xedpoint theorem Tar55] for complete lattices and monotonic functions, guarantees that models always exist for any recursive formula. Theorem 2 (Maximal and minimal model) Given a recursive formula F of the form X:F or X:F , there exist models max and min given by:
max = min = max
\
f
j j D
D
F ( )g
g
f
is the maximal model w.r.t. and the minimal model w.r.t. . The operator is taken to indicate that we want the model max , whereas the operator is taken to indicate that we want the model min and thus the semantics of the recursion operators is
F( ) min is
From Theorem 2 we obtain the following de nition of pre and postmodels. 9
X:F ]] = X:F ]] =
max (X ) min (X )
De nition 3 (Pre and postmodels) Given a formula X:F or X:F ,
an environment is a premodel if 2 f j DF ( ) g. is a postmodel if 2 f j DF ( )g. Consequently, Theorem 2 says that the semantics of a formula is the union of all its postmodels and that the semantics of a formula is the intersection of all its premodels. When relating types and logical properties, we are primarily interested in maximal models.
6 Specifying objects
The modal mucalculus is very powerful when used a temporal logic of labelled transition systems. It is wellknown that the temporal modalities of the propositional branching time temporal logic CTL Eme94] are expressible within the mucalculus (in fact, it can be shown that all of CTL Eme94] can be expressed within the mucalculus). In this short section we shall describe how properties of & calculus can be described this way. We let the set Act denote the set of possible observations; we write Act]F as an abbreviation of V 2Act ]F and similarly, we write W hActiF as an abbreviation of 2Act h iF . The CTL temporal modalities can be de ned as
AGF EGF EFF AFF
= = = = s UF;G = w UF;G =
X:F X:F X:F X:F X:G X:G
^ ^
^h ^ _ _
Act]X ( Act]ff Act X ) Act X ( Act tt Act]X ) (F Act tt Act]X ) (F Act]X )
_h i i h i ^ ^ h i ^ ^
The intuitive interpretation of these modalities is of any transition path of o. EGF : EGF is satis ed by an object o if there exists some transition path of a such that F is satis ed by all states of the path. 10
AGF : An object o satis es AGF , a 2 AG] max , if F is satis ed by all states
EFF : The dual of AGF . An object o satis es PF if F is satis ed by some
state along some transition path.
AFF : Guarantees that F will sooner or later be true along any transition
path.
Us (F; G); Uw (F; G): The meanings of Uw (F; G) and Uw (F; G) only di er slightly. The idea is that an object o satis es Us(F; G) or Uw (F; G) if F is sat
is ed by o until G at some point is satis ed. The di erence is that Uw (F; G) does not guarantee that G will ever be satis ed. Us (F; G) is called strong until, and Uw (F; G) weak until.
So notice that invariance properties are expressed using maximal recursion, whereas eventuality properties are expressed using minimal recursion. The following example illustrates how an object can be speci ed using the CTL modalities: Example 1 In AC96] a calculator object is described. The behaviour of the calculator can informally be stated as follows: Either one of the methods enter, add or sub can be invoked, which will result in a new calculator, or the method equals can be invoked resulting in termination. In the following let Act be de ned as Act = fenter; add; subg. The formula F shown below speci es the observations that must be allowed by a calculator object of recursive type. The formula G describes what must always hold about the methods enter, add and sub of the calculator object:
F = unfold tt unfold]tt Act]ff; G = ( add ]tt add tt) ( sub]tt sub tt) ( enter]tt enter tt) unfold]ff:
h i ^ ^ ^ h i _ ^ h i _ ^ h i ^
To express that it holds that F is satis ed until G at some point will be satis ed we use the connective strong until and write:
Us (F; G):
We write that Us(F; G) must always hold as
AGUs(F; G)
11
The speci cation of the calculator object is then a combination of AGUs(F; G) and the speci cation for the equals method: Feq = hunfoldi( equals]tt ^ hequalsitt) ^ unfold]( equals]tt ^ hequalsitt) The nal correctness speci cation looks as follows: AGUs (F; G) _ Feq :
2
7 Types as logical formulae
In this section we shall show an intimate correspondence between the types of Ob < and the formulae of Form. Types are certain invariance properties and subtyping corresponds to inclusion between logical properties.
1 :
7.1 The translation
In order to be able to express the typings of objects in our modal logic we introduce the atomic formula isBool, which is the logical formula corresponding to Bool. isBool has the following semantics: isBool] = fa j a:Boolg The reason for introducing a special atomic formula, which models the basic type Bool, is that the mucalculus connectives alone cannot express that an object of type Bool will allow precisely the observations true or false in order to achieve this, we would need in nite conjunctions. Further, the fact that an object of type Bool can diverge in the reduction semantics cannot be expressed. In other words, it seems reasonable that the base types should be modelled by atomic formulae. Only certain formulae can occurs as the translations of Ob < types. We shall call such formulae type formulae. The abstract syntax of type formulae is as follows: ^ ^ F ::= tt j ( hliit(Fi)) ^ ( li]t(Fi )) j isBool i2I i2I j X j X:hunfoldit(F ) ^ unfold]t(F )
1 :
12
We denote the set of type formulae by Formt . We are now able to introduce the translation T : Type ! Formt from types to type formulae as follows: T (Top) = tt T (Bool) = isBool ^ ^
T
( li :Ai ]i2I ) = (
T
Not surprisingly, the type Top is assigned the formulae tt, since all typable objects have type (or supertype) Top. The type Bool is as a special case translated to the atomic formula isBool. The mucalculus translation of an object type re ects the possible method invocations that can be performed with respect to objects of the object type. The speci cation for a recursive object type is an invariance property. It states that it must always be possible to perform a transition on unfold leading to the speci cation for an object type, and that we must therefore consider the maximal interpretation of the logic formula. In other words, the becomes a when passing from types to formulae. The translation de ned by T is similar to the notion of characteristic formula IS94] for the typings of objects. It is not the case, though, that these characteristic formulae express all possible behaviours of objects. In particular, it is not possible to prove that the logic for object types fully characterizes the bisimulation of Gordon and Rees, as the types and thus the type formulae say nothing about the possibility of method overrides. (This is exempli ed towards the end of this section.)
( (X )A) = X:hunfoldiT (A) ^ unfold]T (A) T (X ) = X
i2I
h
li (Ai)) ( li] (Ai))
iT ^
i2I
T
7.2 Soundness and completeness of the translation
The translation presented here is correct in a very precise sense. In order to express this, we need to formulate the logic counterparts of the typability notions. De nition 4 expresses the notion of subtyping with respect to the modal formulae for types. De nition 4 Let A; B 2 Type and ? some well formed environment. We say that ? models the subtyping relation A <: B written
? j= A <: B
13
if for some postmodel it holds that T (A)]] T (B )] ] and (X ) T (C )] ] for all (X <: C ) 2 ?. Lemma 5 relates the standard subtype judgments, which are of the form ? ` A <: B , to the inclusion relation between logical properties. The lemma is interesting in its own right and is also going to be useful in the proof of Theorem 6. Lemma 5 Let A; B 2 Type, ? some well formed environment and ? ` A <: B . Then ? j= A <: B . Proof. By induction in the proof tree of ? ` A <: B , that is, by inspecting the rules for subtyping.
Sub Re : It follows directly that (A)]] (A)]] . Sub Top: Since (Top)]] = Obj it must hold that (A)]] (Top)]] for all types A Type. Sub Object: Let li :Ai]i2I <: li :Ai]i2J for some indexing sets I; J for which
T T T T T 2
Sub X : Follows from the well formedness of ?. Sub Rec: Assume there is a postmodel such that (X )
1 2
it holds that J I . By de nition of t, T ( li :Ai]i2I ) must impose at least the same restrictions on objects as T ( li:Ai ]i2J ). It follows that li :Ai]i2I ] li :Ai ]i2J ] . all X <: C 2 ?, (X ) (X ) and T (A)]] T (B )] . We must ] nd a postmodel 0 such that 0(X ) T (A)]] for all X <: C 2 ? 0 and T ( X :A)]] T ( X :B )] . Take ] de ned by
T
(C )]] for
8 > (X ) < 0 (X ) = > (X ) : (X ) By the assumptions ( X :A)]]
1 2
1
2
T T
(A)]] (B )]]
T
if X = X if X = X otherwise
1
2
need to check that
0
0
is a postmodel, i.e. that
T
T
1
0
( X2 :B )]] 0 . Thus, we only
T
(X1 )
(A)]] 0 and 0 (X2 )
(B )]] 0 :
By de nition of 0 , (X ) 0 (X ) for all X . Then, since ] is monotonic on it must hold that F ] F ] 0 for all F 2 Formt . 14
We want our translation to be sound and complete with respect to the usual typings of objects. In particular we wish to prove a statement resembling
? ` a:A
,
2
for some ? and . It turns out that this is possible, if we assume certain properties of the typing environment ?. Theorem 6 gives us the soundness of our translation. Theorem 6 (Soundness) Let a 2 Ob < , A; B 2 Type and ? ` a:A, where ? is some well formed environment. If it holds that (x:B ) 2 ? implies x] 2 T (B )]] for all x 2 dom(?) and some postmodel , then a 2 T (A)]] . Proof. By induction in the proof tree of ? ` a:A. Val True: Obviously true 2 T (Bool)]] , since by Trans Bool ] true true 0. Val False: Similar. Val Subsumption: We have that a 2 T (A)]] and T (A)]] T (B )] . ] Then by Lemma 5 it must hold that a 2 T (B )]] . Val Select: Assume that a 2 T ( li:Ai]i2I )]] . Then it is also the case that
1 :
a
2
T
(A)]]
a
2
(
^
i2I
h
^ li (Ai)) ( li] (Ai))]] :
iT ^
i2I
T
By the transition rule Trans Select ] and the semantics of hliiF it is given that a:lj 2 T (Aj )]] for all j 2 I . Val Unfold: Assume that a 2 T ( (X )A)]] . Then it is also the case that
a
2
X
2
) h
unfoldiT (A) ^ unfold]T (A)]] :
This implies that
a
h
unfoldiT (A) ^ unfold]T (A)]] :
T
Since is a postmodel it must hold that unfold(a) 2 by Trans Unfold ] a X A unfold  unfold(a)A.
( )
(A)]] , since
The completeness of the translation is given by Theorem 7. 15
2
a type A such that ; ` a:A, where T (A) = F . Proof. By induction on the possible forms of F .
Theorem 7 Let a Ob < and F Formt. If a
2
1 :
2
2
F ] then there exists
Top: If F = tt then it must hold that a:Top, where (Top) = tt. Bool. If F = isBool then, obviously, a:Bool. where (Bool) = isBool. Object: Assume that
T T
F =(
^
i2I
h
^ li (Ai)) ( li] (Ai)):
iT ^
i2I
T
It must be the case that a can perform the transitions a l a:li , where a:li 2 T (Ai )]] , for all i 2 I . That is, a must at least have the type li :Ai]i2I . We do not know if a may have further possibilities for transitions, a l a:lj for j 2 J , I \ J = ;, which results in the typing
i j
li:Ai; lj :Aj ]i2I J ;
but we do not care about this, since
li:Ai ; lj :Aj ]i2I J <: li:Ai ]i2I :
Unfold: Assume that
F = X unfold (A) unfold] (A): Then, obviously, a: (X )A.
) h iT ^ T
Var: Trivial.
As mentioned earlier, the characteristic formulae for object types do not fully characterize the bisimulation equivalence of objects due to Gordon and Rees. This is due to the fact that the typing of an object does not take into account the possible method overrides that can be performed on the object. In fact it is possible, with respect to an object, to do in nitely many method overrides. That is, the & calculus is not nite branching. This lack of information about the possible behaviour of an object carries through to the type formulae. 16
2
Example 2 Consider the two objects:
a = l = true; l = false] b = l = true; l = & (x:A) x:l ]
1 2 1 2 1
Both have the type
A = l :Bool; l :Bool];
1 2
and supertypes B and C :
B = l :Bool]; C = l :Bool] It can be shown that a B b and a C b but a A b, since after the method overrides a:l & (x)x:l and b:l & (x)x:l , a converges while b diverges. The encodings of A,B and C look as follows (A) = ( l (Bool) l (Bool)) ( l ] (Bool) l ] (Bool)) = ( l isBool l isBool) ( l ]isBool l ]isBool) (B ) = l (Bool) l ] (Bool) = l isBool l ]isBool (C ) = l (Bool) l ] (Bool) = l isBool l ]isBool
1 2
6
1 (
2
1 (
2
T
h 1 iT h 1i
^ h 2 iT
^
1 T
^
2 T
^ h 2i ^
^
1
^
2
T
h 1 iT h 1i
1 T
^
1
T
h 2 iT h 2i
^
2 T
^
2
If the type formulae should characterize GordonRees bisimulation, then it should be the case that a; b 2 T (B )]] and a; b 2 T (C )]] , but a; b 62 T (A)] . Obviously this is not the case, since a; b 2 T (A)] . ] ] 2
8 Conclusions and further work
In this paper we have described how certain properties of & calculus terms can be described within the modal mucalculus. A natural next step is to investigate how one can use the mucalculus to verify interesting properties of objects. The notion of model checking, that is, algorithmically checking whether a term satis es a given modal formula SW89], is already well understood in the context of process calculi. It remains to be seen how far we can proceed within the & calculus. 17
We have also shown a correspondence between the type system Ob < for the & calculus and the modal mucalculus, which captures both type assignment and subtyping. A natural question is how much further we can go in this direction. We can easily deal with arrow types, if we introduce a simple notion of intuitionistic implication into our logic. Let us say that F implies G for some object o if o is an object abstraction which, whenever given an argument satisfying the property F becomes an object satisfying the property G.
1 :
F
We then get
)
G]] = o o0
f j 8
2
F ]] : oo0
2
G]]
g
T
It is straightforward to see that this extended interpretation is sound w.r.t. the subtyping rules for arrow types, and in particular for the rule Sub Arrow] which states that the arrow type is contravariant in its rst second and covariant in its second argument. This leads straight to the question of the possibility of dealing with the variance annotations suggested by Abadi and Cardelli in AC96]. This seems to require the introduction of negation into the syntax of the logic and is a topic of further study. The interpretation of types as modal formulae also suggests a somewhat alternative account of the semantics of types to that presented in AC96], where the semantics of a type is a per (partial equivalence relation). This is a topic of ongoing work by one of the authors.
? ` A0 <: A ? ` B <: B 0 ? ` A ! B <: A0 ! B 0
(A1 ! A2 ) = T (A1 ) ) T (A2 )
References
AC94a] AC94b] Martin Abadi and Luca Cardelli. A semantics of object types. In Proceedings of the 9th IEEE Symposium on Logics in Computer Science, pages 332 341. IEEE Computer Society Press, 1994. Martin Abadi and Luca Cardelli. A theory of primitive objects untyped and rstorder systems. In Theoretical Aspects of Computer Software, pages 296 320. SpringerVerlag, 1994. 18
AC94c]
Martin Abadi and Luca Cardelli. A theory of primitive objects: Secondorder systems. In Proceedings of European Symposium on Programming, number 788 in Lecture Notes in Computer Science, pages 1 25. SpringerVerlag, 1994. Martin Abadi and Luca Cardelli. A Theory of Objects. SpringerVerlag, 1996.
AC96]
BAMP83] M. BenAri, Z. Manna, and A. Pnueli. The temporal logic of branching time. Acta Informatica, 20:207 226, 1983. Eme94] GR96] E.A. Emerson. Handbook of Theoretical Computer Science, chapter Temporal and Modal Logic, pages 995 1072. Elsevier, 1994. Andrew D. Gordon and Gareth D. Rees. Bisimilarity for a rstorder calculus of objects with subtyping. In Proceedings of the TwentyThird Annual ACM Symposium on Principles of Programming Languages, 1996. M. Hennessy and R. Milner. Algebraic laws for nondeterminism and concurrency. Journal of the ACM, 32(1):137 161, January 1985. Anna Ing lfsd ttir and Bernhard Ste en. Characteristic formulae for processes with divergence. Information and Computation, 110:149 163, April 1994. D. Kozen. Results on the propositional calculus. Theoretical Computer Science, 27:333 354, 1983. Kim G. Larsen. Proof systems for satis ability in HennessyMilner logic with recursion. Theoretical Computer Science, 72:265 288, 1990. R. Milner. Communication and Concurrency. PrenticeHall International, 1989. D.M.R. Park. Concurrency and automata on in nite sequences. In P. Deussen, editor, Proceedings of 5th GI Conference LNCS 104, pages 167 183. SpringerVerlag, 1981. 19
HM85] IS94] Koz83] Lar90] Mil89] Par81]
SW89] Tar55]
C. Stirling and D. Walker. Local model checking in the modal mucalculus. In LNCS 351, pages 369 383. SpringerVerlag, 1989. A. Tarski. A latticetheoretical xpoint and its applications. Paci c Journal of Mathematics, 5:285 309, 1955.
20