Program Verifications, Object Interdependencies, and Object Types

(1)

Program Veri ations, Obje t Interdependen ies,

and Obje t Types

Cong-CongXing

∗

Department ofMathemati s andComputerS ien e,Ni hollsStateUniversity

mps- xni holls.edu

Abstra t

Obje t types are abstra t spe i ations of obje t behaviors; obje t behaviors are

ab-stra tly indi ated by obje t omponent interdependen ies; and program veri ations

arebasedonobje tbehaviors. In onventionalobje ttype systems, obje t omponent

interdependen ies are not taken into a ount. As a result, distin t behaviors of

ob-je tsare onfusedin onventional obje t type systems, whi h anleadto fundamental

typing/subtyping loopholes and program veri ation troubles. In this paper, we rst

identify a program veri ation problem whi h is aused bythe loose onventional

ob-je t typing/subtyping whi h isin turn aused bythe overlookingof obje t omponent

interdependen ies. Then,asanewobje ttypings heme,weintrodu eobje ttypegraphs

(OTG) in whi h obje t omponentinterdependen ies areintegratedinto obje t types.

Finally, we showhowthe problemexisting in onventional obje t type systems anbe

easilyresolvedunderOTG.

1 Introdu tion and Related Work

Although mu h of there ent year'swork onobje t-oriented programming (OOP) has

fo- used on large entities su h as omponents, environments, and tools, investigations on

issues related to obje t-oriented languages themselves are still an on-going resear h and

many newimprovements anbeexpe ted. Inparti ular, typing and programveri ation

are still a riti al issue and a problem-prone area in the formal study of obje t-oriented

languages, espe ially when type-related subje ts, su h as subtyping and inheritan e, are

onsidered. Inthe ontexts of OOP theory resear h, there are three major lines:

Abadi-Cardelli's

ς

- al ulus [2℄, Fisher-Mit hell's lambda al ulus of obje ts [14, 19, 18, 4℄, and Bru e's PolyTOIL [7, 6 ℄. The type systems of all these al uli are onventional in the

following sense: the major behavior indi ator of obje ts obje t omponent

interdepen-den ies isnotree ted inobje t types.

The resultof nothaving su h omponent interdependen y information represented in

obje ttypesisthattwobehaviorallydistin tobje tswhi hdeservetobetypeddierently,

mayhavethesametype. Forexample,letobje ts

a

and

b

bedened,usingthe

ς

- al ulus[2℄ notation, as follows:

a

def

= [l

1 = 1, l

2 = 1]

,

b

def

= [l

1 = 1, l

2 = ς(s : Self )s.l

1 ]

where

s

isthe self

variable and

Self

is the type of

s

. The behavioral dieren e between

a

and

b

an be revealed by thefollowing omputations: Suppose wewouldliketo update

l

1

in

a

to2.

(2)

Itis easy to see that before and after thisupdating operation, the status of

l

2

in

a

remains thesame, namely,

a.l

2 = 1

and

(a.l

1 ⇐ 2).l

2 = [l

1 = 2, l

2 = 1].l

2 = 1

1

. However,

when the same operation (updating

l

1

to 2) isapplied to

b

, the status of

l

2

in

b

would be hanged after the operation, namely,

b.l

2 = 1

but

(b.l

1 ⇐ 2).l

2 = [l

1 = 2, l

2 = ς(s :

Self

)s.l

1 ].l

2 = 2

dueto the fa t that

l

2

depends on

l

1

(

l

2

alls

l

1

) in

b

. In onventional type systems, this behavioral dieren e between

a

and

b

is not aptured in their types;

a

and

b

are of the same type:

[l

1 : int, l

2 : int]

. As a result, elusive programming errors and programveri ation problems will inevitably o ur whensubtyping is onsidered(as

shown inthe nextse tion).

Inthispaper,we introdu e,as anewway torepresentobje ttypes,obje t type graphs

(OTG)inwhi hobje t omponentinterdependen yinformationisabstra tlyrevealed,and

show thatOTGprovidesanee tivesupportforprogramveri ations. Se tion2presents

aprogramveri ationproblem ausedbyobje ttyping. Se tion3denesaformal

obje t-orientedlanguageTOOLinwhi hobje t omponent interdependen iesaretobestudied.

Se tions 4 and 5 dene OTG and typing/subtyping under OTG respe tively. Se tion 6

demonstrates how the program veri ation problem shown in Se tion 2 an be resolved

under OTG. Se tion7 on ludes thispaper.

Therearesomeresear hworkintheliteraturethatare(somehow)relatedtoourwork.

Behavioral subtyping is introdu ed in [20 ℄. Although obje t behavior and subtyping are

the ommon interests in both [20 ℄ and our paper, our typing approa h is fundamentally

dierentfromthatin[20 ℄whereobje tinterdependen iesarenot onsidered. Labeled types

and width subtyping are proposed in [3, 4 , 19℄, where the typeof a method is labeled by

aset of methods thatit uses. Whilethe idea oflabeled typesis somewhat related to our

idea of obje t interdependen y, they dier substantially in quality and in quantity. For

example,thenotionofobje tinterdependen yispre iselydenedinourworkwhereas the

issue of method usages is not formally addressed in labeled types. Furthermore, in our

work, obje t interdependen ies fully parti ipate and de isively reshape obje t subtyping

whereasinlabeledtypesthemethodusagesinformationisbarelyusedinobje tsubtyping.

The notion ofobje t state typing anbe found in,for example, [9 ,21 ℄. Just like [20℄(as

opposedtoourwork),thisapproa hdealswiththeissueofobje tbehaviorand subtyping

ina fundamentally dierentway from ours,whi h makesitorthogonaland omplemental

toourapproa h.

2 The Problem and Motivation

Pointswithadditionalattributes(e.g., olorpoints[5 ,8 ,15 ℄,movablepoints[2,4,15℄)have

been an interesting study- ase in the fundamental resear h of obje t-oriented languages.

Here, we observea new problem thatis asso iated with movablepoints. We rst present

thisproblemona theoreti albasisand thendemonstrateitusing Java.

1

(3)

2.1

ς

- al ulus Des ription of the Problem

Westipulatethatapointis olored(ornon- olored,respe tively),ifthispoint(obje t)has

a (or hasno, respe tively) olor attribute. Letus onsider non-negative movable points 2

.

For 1-d movable points, we assume that all points greater than 1 are olored points and

all other points are non- olored points (Figure 1). For 2-d movable points, similarly, we

assumethatallpointswithadistan efromtheorigingreaterthan1are oloredpointsand

allotherpointsarenon- oloredpoints(Figure2). Thisassumption anbeeasilyextended

forhigher-dimensional points.

1

0 pts w/o color

pts w/ color

x

Figure1: 1-dColoredand non- oloredpoints

1

0 y

x

pts w/ color

pts w/o

color

Figure2: 2-dColoredand non- oloredpoints

Forinstan e,usingthe

ς

- al ulus(se ond-order) notation[2℄,we andenea1-d non- olored movablepoint and a1-d oloredmovable pointas follows:

p

1n

def

=





x = 0.5

mvx

= ς(s : Self )λ(i : real )(s.x

⇐s.x + i)

dist

= ς(s : Self )s.x





,

p

1c

def

=







x = 2.0

mvx

= ς(s : Self )λ(i : real )(s.x

_{⇐s.x + i)}

dist

= ς(s : Self )s.x

clr

= blue







,

where

mvx

moves the point to a new position on the

x

-axis and

dist

returns the dis-tan e from the origin to the urrent position of the point. The

⇐

is the method updat-ing/overriding operation in

ς

- al ulus. The intentions ofelds

x

and

clr

areobvious.

2

(4)

To hara terize the behaviors of1-dmovable points,we dene thefollowing types:

P

def

=

ς

(Self )





x : real

mvx

: real

_{→ Self}

dist

: real





,

CP

def

=

ς

(Self )







x : real

mvx

: real

_{→ Self}

dist

: real

clr

: color







,

N CP

def

= P,

where

P

isthe type of all1-d movable points,

CP

isthe type of1-d olored points, and

N CP

is the type of 1-d non- olored points. Given the obje ts and types dened as the above, it iseasy to he k that in onventional obje t type systems, we have

p

1n

: N CP

,

p

1c

: CP

,

CP <: P

, and

N CP <: P

.

Now,supposewewouldliketowriteaprogram,

ms

(moveandsee),whi htakesa1-d point and moves it along the

x

-axis. Due to the o-existen e of olored and non- olored pointsonthe

x

-axis,themovement annot bearbitrary. Wespe ifythebehaviorof

ms

as follows: (a)

ms

moves the argument point toits right a ertain amount of distan e if the argumentpoint is olored (sothatitwillnotmixwithnon- oloredpoints). (b)

ms

moves theargumentpointtoitslefthalfofthedistan e fromtheorigintothe urrentpositionof

theargumentpointiftheargumentpointisnon- olored(sothatitwillnotmixwith olored

points). ( )Let

p

′

bethenewlyresultedpointin ases(a)and(b). In ase(a),

ms

usesthe property

p

′

_{.dist > 1}

of

p

′

to arryout the omputation

arcsin(1/p

′

_.dist)

; in ase (b),

ms

uses the property

p

′

_.dist

_{≤ 1}

of

p

′

to arry outthe omputation

arcsin(p

′

_.dist)

. Be ause

of subtyping and subsumption, inevitably,

ms

will take higher dimensional points as its arguments. Toensurethat

ms

worksnewithhigherdimensionalpoints,werequirethat, in su h ases,thehigher dimensionalpoint be moved (right or left)alongthe

x

-axis,and theamountofdistan etobemovedfollowsthesameguidelinestatedabove. Forexample,

givena2-dpoint

p

with oordinates

(x, y)

,if

p

is olored(whi hmeans

px

2 _{+ y}

2 _{> 1}

),we

moveittotherightalongthe

x

-axisoveradistan e

δ > 0

. Thedistan efromtheoriginto the new position ofthe point thenwould be

p(x + δ)

2 _{+ y}

2 _>

_px

2 _{+ y}

2 _{> 1}

, indi ating

thatthepointisstillinthe olored point areaonthe

x

-

y

plane. If

p

isnon- olored(whi h means

px

2 _{+ y}

2 _{≤ 1}

),wemoveittotheleftalongthe

x

-axishalfof

x

. Thedistan efrom

the origin to thenew positionof thepoint then wouldbe

q

(

1

2 x)

2 + y

2 <

px

2 + y

2 ≤ 1

, indi ating that the point is still in the non- olored point area. Thus the spe i ation of

(5)

Withlittle eort,we anwrite

ms

asfollows:

ms

def

= λ(p : P )

if(

p

.dist > 1

) //

p

is olored

sin

-

1 (

1 /(p.mvx (δ)).dist)

//

δ > 0

else //

p

isnon- olored

sin

-

1 ((p.mvx (

−

1

2 p.x)).dist)

endif

Figure3: Thefun tion

ms

Now,thequestionwehaveis: does

ms

performtoitsspe i ation withallpermissible arguments? Orsimply, is

ms

reliable? Can weverifyits orre tness?

It is easy to he k that

ms

works as expe ted with

p

1n

and

p

1c

. We now dene one olored 2-dpointand twonon- olored2-d pointsas follows:

p

2c

def

=







x = 2.0

y = 2.0

mvx

= ς(s : Self )λ(i : real )(s.x

_{⇐s.x + i)}

mvy

= ς(s : Self )λ(i : real )(s.y

⇐s.y + i)

dist

= ς(s : Self )p(s.x)

2 _{+ (s.y)}

2 clr

= blue







,

p

2n

def

=







x = 0.5

y = 0.3

mvx

= ς(s : Self )λ(i : real )(s.x

_{⇐s.x + i)}

mvy

= ς(s : Self )λ(i : real )(s.y

⇐s.y + i)

dist

= ς(s : Self )p(s.x)

2 _{+ (s.y)}

2 





,

p

′

2n

def

=







x = 0.5

y = ς(s : Self )

_4(s.x)

1 mvx

= ς(s : Self )λ(i : real )(s.x

_{⇐s.x + i)}

mvy

= ς(s : Self )λ(i : real )(s.y

⇐s.y + i)

dist

= ς(s : Self )p(s.x)

2 _{+ (s.y)}

2 





.

Notethat

p

2c

and

p

2n

anberegardedasfree2-dpointssin etheir

x

and

y

eldsare independent ea hother,whereas

p

′

2n

anberegardedasa onstrained 2-dpointsin eits

y

oordinate depends onits

x

oordinate. Also note that

p

′

2n

is alegitimate non- olored point sin e its oordinate is

(0.5, 0.5)

whi h shows that the distan e from the origin to thispoint islessthan 1. Moreover,notethat although

p

2c

,

p

2n

,and

p

′

2n

are dened from s rat h, they ould havebeendenedthrough inheritan e from(the lassesof)

p

1c

or

p

1n

in lass-basedobje t-oriented languages(as shown inthe nextsubse tion).

(6)

Under onventional obje ttype systems,

p

2c

and

p

2n

havetypes

CP

2

def

=

ς

_{(Self )}







x : real

y : real

mvx

: real

→ Self

mvy

: real

→ Self

dist

: real

clr

: color







and

N CP

2

def

=

ς

(Self )







x : real

y : real

mvx

: real

_{→ Self}

mvy

: real

_{→ Self}

dist

: real







respe tively, and

p

′

2n

has the same type as

p

2n

. That is,

p

′

2n

: N CP

2

. Furthermore,

CP

2 <: P

and

N CP

2 <: P

, so

ms

(p

2c

)

,

ms

(p

2n

)

and

ms

(p

′

2n

)

alltype- he k.

It is easy to he k that

ms

(p

2c

)

and

ms

(p

2n

)

work just ne. What about

ms

(p

′

2n

)

? It issupposed to return the degree of anangle. Unfortunately, the exe ution of

ms

(p

′

2n

)

produ esarun-timeerror,asoutlined below: The urrentpositionof

p

′

2n

is

(0.5, 0.5)

with

p

′

2n

.dist =

√

0.5

2 _{+ 0.5}

2 _{< 1}

. Soitismovedtotheleft

0.5

2 = 0.25

unitsofdistan eresulting in anotherpoint,say,

p

′′

2n

. The position of

p

′′

2n

is

(0.25,

1 4×0.25

) = (0.25, 1)

and thedistan e from the origin to

p

′′

2n

is

p

′′

2n

.dist =

√

0.25

2 _{+ 1}

2 _{> 1}

. The exe ution

sin

-

1 (p

′′

2n

.dist)

thus rashes be ause

sin

-

1

isundenedfor argumentgreater than1.

What goes wrong is lear: when the

x

- oordinate of

p

′

2n

is moved (de reased), its

y

- oordinate is impli itly moved too (in reased) due to the interdependen y between

x

and

y

(

y =

1 4(s.x)

). The ombination of these two movements makes

p

′

2n

(a non- olored point) go into the olored point area of the

x

-

y

plane, resulting in a point with distan e greater than 1 and reating semanti s onfusions. The importan e of obje t omponent

interdependen ies to obje t behaviors an be seen learly here. Con eptually, for

ms

to safelyfulll itsspe i ations, itshouldnot take anarbitrary pointas its argument. Any

points inwhi h some methods dependon

x

and ae t distatthe same time,for example

p

′

2n

, willpotentiallymakethebehaviorof

ms

unpredi tableand endangertheexe ution of

ms

whentheyare submittedto

ms

. Thus, allowing pointslike

p

′

2n

tobesubmitted to

ms

isawrong idea,in thesense that

ms

(p

′

2n

)

doesnotwork asspe iedandtherefore

ms

is unreliable.

How an we x this problem? Is the fun tion

ms

omposed in orre tly? Is there a way to rewrite

ms

so that we an prove that

ms

works as spe ied for all permissible arguments? Itseemsunlikely. Notethat

ms

iswrittenwith

P

asthetypeofitsargument.

ms

annotforeseewhatkindofextramethodsthereareinitsa tualarguments. When

p

′

2n

issubmitted to

ms

,

p

′

2n

's

y

- oordinate isinvisibleto

ms

.

ms

doesnot know theexisten e ofthe

y

- oordinate, and of ourse, hasno way ofknowing the interdependen ies between

(7)

y

and other methods and the ensuing behavior of

p

′

2n

. This is espe ially the ase if

p

′

2n

is onstru ted via inheritan e from

p

1c

or

p

1n

. This situation auses the behavior of

ms

(with various permissible arguments) unpredi table, and is inevitable in OOP supported

by onventional obje t typesystems.

2.2 Java Version of the Problem

To show that theproblem existsnotonly inobje t-based languages,butin lassed-based

languages as well, we present a Java version of the problem with two running s ripts in

Figure 4.

ClassesP,CP,CP2,and NCP2 orrespondtotypes

P

(and

N CP

),

CP

,

CP

2

,and

N CP

2

respe tively. Similarly, obje ts p1n,p1 ,p2n,p2 and p2na orrespond topoints

p

1n

,

p

1c

,

p

2n

,

p

2c

, and

p

′

2n

respe tively. MPP and MPP1 are two appli ations that use these points. Duetothe lass-serves-as-type featureofJava,theJavaversionoftheproblemistwisted

a bit: The types of p2n and p2na are NCP2 and NCP2a respe tively. These two types are

not the same but enjoy a subtyping relationship NCP2a

<:

NCP2. This is dierent from

ς

- al uluswhere

p

2n

and

p

′

2n

havethesametype,butdoesnotae ttheillustration ofthe problem.

Notethat in lassNCP2a ofFigure 4, in orderto faithfullyimplement the desired fa t

that

y

- oordinatedepends on

x

- oordinate, we need touse the ombination ofthe eld y and themethod y()tosimulate it. Thisisdueto theimperative featureofJava. Field

y,asaninstan evariable,on ea quiresavalue, willevaluatetothesamevalueea htime

it is evaluated. So eld y does not depend on anyone in thissense. Then how an we

ode

y

- oordinatedepends on

x

- oordinate? The useof anauxiliarymethod y()whi h depends onx (as desired) omesintohelp.

Fromthe exe utions riptofMPP,we an learlyseethat submittingthe onstrained

point p2na to the fun tion ms auses a run-time bug, whi h demonstrates that the type

NCP2aofp2nashouldnotberegardedasasubtypeofthetypePalthoughNCP2aisinherited

(indire tly)fromP.Consideringthatallms(p1 ),ms(p2 ), ms(p2n)work neandallthe

lasses (types) ofthethree obje ts p1 ,p2 , p2nareinherited (indire tly)fromP too, we

need todistinguish (all)inheritan es inJava so thatsome inheritan es (e.g., thoseas CP,

CP2, and NCP2) may imply subtyping and others (e.g., those as NCP2a) do not. This an

be done by using obje t interdependen y as a measurement. Unfortunately, Java thinks

all inheritan e is subtyping. What is more interesting is that due to the way in whi h

Javahandles NaN(Anyarithmeti operationinvolvingNaNandotheroperandsprodu esa

NaN, but any relational operation involving NaN and other operands produ es either true

or false 3

.), this run-time bug an be ome hidden and di ult to nd if the relevant

ex-pression is (deeply)involved with other omputations. MPP1 issu h an example; by just

examiningtheexe utions riptofMPP1,itishardtotellthatms(p2na)hasa tually aused

a run-timebug.

3

ThereareothermeansinJavatomaketheillegalvalueNaNlegal,e.g.,(int)(Math.asin(2)) evaluatesto0,

(8)

// lassP.Notethatthis isalso lass

//NCPsin eNCPisdefinedasP.

publi lassP{

prote ted doublex=0.5;

publi double getx()

{returnx;}

publi voidmvx(doublei)

{ x=x+i;}

publi double dist()

{returngetx();}

}

// lassCP,inheritedfromP

publi lassCPextendsP{String lr="blue";

publi CP()

{x=2.0;}

}

// lassCP2,inherited fromCP

publi lassCP2extendsCP{

prote ted doubley;

publi CP2()

{y=2.0;}

publi doublegety()

{returny;}

publi voidmvy(doublei)

{y=y+i;}

publi doubledist()

{returnMath.sqrt(getx () *g etx () +gety()*gety()) ;}

}

// lassNCP2,inheritedfrom P

publi lassNCP2extendsP{

prote ted doubley;

publi NCP2()

{y=0.3;}

publi doublegety()

{returny;}

publi voidmvy(doublei)

{ y=y+i;}

publi doubledist()

{returnMath.sqrt(getx () *g etx () +gety()*gety()) ;}

}

// lassNCP2a, inheritedfromNCP2.Needthe ombination

//ofyandy()tosimulate"ydependsonx". Note that

//"ydependsonx"iswhatwewanttodo,withouttheuse

//ofy(),fields xandywouldbeindependent

publi lass NCP2aextendsNCP2

{

publi NCP2a()

{y=y();} // allingy()toget

//valuefory

publi doubley() //implementationof

{return1/(4*x);} //"ydependsonx"

publi doublegety()

{y=y(); // allingy()toget

returny; //valuefory

}

//Appli ationthatuses P,CP,CP2,NCP2,andNCP2a

publi lassMPP{

publi stati voidms(P p)

{if(p.dist() >1)

{System.out.pri nt ln (" Thisisa oloredpoint");

p.mvx(1); //movepasspe ified

System.out.pri nt ln (" Theresultis:"+Math.asin(1/ p. dis t( )) );

}

else

{System.out.pri nt ln (" Thisisanon- oloredpoint");

p.mvx(-0.5*p.g et x( )); //movepasspe ified

System.out.pri nt ln (" Theresultis: "+Math.asin(p.d ist () )) ;

}

publi stati voidmain(String args[℄)

{ Pp1n=newP();

CPp1 =newCP();

CP2p2 =newCP2();

NCP2p2n=newNCP2();

NCP2ap2na=newNCP2a();

System.out.pri nt ln ("m ak in g all ms(p1n)...");ms(p1n);

System.out.pri nt ln ("m ak in g all ms(p1 )...");ms(p1 );

System.out.pri nt ln ("m ak in g all ms(p2n)...");ms(p2n);

System.out.pri nt ln ("m ak in g all ms(p2 )...");ms(p2 );

System.out.pri nt ln ("m ak in g all ms(p2na)...");ms(p2na);

}

//Appli ationthatuses P,CP,CP2,NCP2,andNCP2a

publi lassMPP1{

publi stati void ms(Pp)

{ System.out.prin t(" Che ktoseeiftheresult >PI/4:");

if(p.dist()>1) {p.mvx(1); //move passpe ified if(Math.asin(1/p .d is t( )) >(Math.PI)/4) System.out.pri nt ln (" yes"); else System.out.pri nt ln (" no"); } else

{ p.mvx(-0.5*p.ge tx () ); //movepasspe ified

if(Math.asin(p.d is t( ))>(Math.PI)/4) System.out.pri nt ln (" yes"); else System.out.pri nt ln (" no"); } }

publi stati void main(Stringargs[℄)

{//omitted,same asthepartinMPP}

}

C:\MyJavaProgr am s\ Po in t\m ov ab leptproblem>javaMPPmaking allms(p1n)...

Thisisanon- olored point

Theresult is: 0.2526802551420 786 5

making allms(p1 )...

Thisisa oloredpoint

Theresult is:0.339836909454 12 19

making allms(p2n)...

Theresult is: 0.4011882129972 597 6

Thisisa oloredpoint

Theresult is:0.281034901502 81 36

making allms(p2na)...

Theresult is: NaN

C:\MyJavaProgr am s\ Po in t\m ov ab leptproblem>javaMPP1making allms(p1n)...

Che ktoseeiftheresult>PI/4: no

making allms(p2n)...

making allms(p2na)...

(9)

Summarizing what isdes ribedin thisse tion,we anstate theproblem as follows:

•

InOOPsupportedby onventionalobje ttypesystems,thereisnowaytoimplement programs like

ms

reliably and verifyits orre tness.

Motivatedbythisproblem,wepropose,inthesubsequentse tions,anewtypings heme

forobje ts.

3 A Simple Typed Obje t-Oriented Language

Toillustrate ourapproa h,wedene asimpletypedobje t-oriented language (TOOL)in

thisse tion.

3.1 Syntax

The termsand typesof TOOLaredened asfollows.

M ::= x

_{| λ(x:σ).M | M}

1 M

2 | M.l | M.l⇐ς(x:S(A))M

′

| [l

i

= ς(x :

S(A))M

i

]

n

_i=1

σ ::= κ

_{| t | σ}

1 → σ

2 | µ(t)σ | A | S(A)

A ::= ι(t)[l

i

(L

i

) : σ

i

]

n

i=1

L

i

⊆ {l

1 , . . . , l

n

}

forea h

i

Terms in TOOL are standard

λ

-terms and

ς

-terms [2 ℄. In parti ular,

[l

i

= ς(x :

S(A))M

i

]

n

_i=1

represents an obje t,

M.l

represents method invo ation, and

M.l

⇐ ς(x :

S(A))M

′

represents methodupdating.

Types in TOOL are standard ground type, fun tion type, re ursive type, and the

newlyproposedobje ttype. Inobje ttype

ι(t)[l

i

(L

i

) : σ

i

]

n

i=1

,

ι

istheself-typebinder,ea h method

l

i

hastype

σ

i

,and

L

i

isthesetoflinksof

l

i

(denedinthenextsubse tion).

S(A)

denotes theselftypeindu ed bythe obje ttype

A

.

A = ι(t)[l

i

(L

i

) : σ

i

(t)]

n

i=1

ifand only if

A = [l

i

(L

i

) : σ

i

(

S(A))]

n

_i=1

.

Weprovidea simpleexampletoillustrate the syntaxoftypesand terms. Let

A

def

= ι(t)





l

1 (

{l

2 , l

3 }) : t

l

2 (

∅) : int

l

3 (

{l

2 }) : int → int





.

It spe ies that

l

1

,

l

2

, and

l

3

are of self type (asso iated with

A

),

int

, and

int

→ int

respe tively. The setsoflinksfor

l

1

and

l

3

are

{l

2 , l

3 }

and

{l

2 }

.

l

2

hasnolinks. Anobje t oftype

A

ouldbe

a

def

=





l

1 = ς(s :

S(A))s

l

2 = 1

l

3 = ς(s :

S(A))λ(x:int )(x + s.l

2 )





.

(10)

3.2 Denition of Links

Links are used to signify the stru ture of omponent dependen y of obje ts. Informally,

in obje t type

ι(t)[l

i

(L

i

) : σ

i

]

n

i=1

,

l

j

∈ L

i

means that the value of method

l

i

depends (partially)on the value of method

l

j

. The link me hanism makes the types of obje ts in TOOLsubstantiallydierent fromthat in onventional obje t typesystems.

Denition 1 (Link) Given an obje t

a = [l

i

= ς(s :

S(A))M

i

]

n

i=1

, (1)

l

i

is said to be dependent on

l

j

(i

6= j)

if there exists a

M

su h that

a.l

i

and

(a.l

j

⇐ ς(s : S (A))M).l

i

evaluate to dierent values; (2)

l

i

is said to be dire tly dependenton

l

j

(i

6= j)

if (a)

l

i

isdependent on

l

j

, and (b) if all su h

l

k

(i

6= k, j 6= k)

where

l

i

is dependent on

l

k

and

l

k

isdependent on

l

j

, are removed from

a

,

l

i

isstilldependent on

l

j

; (3) The setof linksof

l

i

(or equivalently, of

M

i

withrespe t to obje t

a

), denoted by

L(l

i

)

(or equivalently, by

L

a

(M

i

)

), ontains exa tlyallsu h

l

j

onwhi h

l

i

isdire tlydependent.

Example 1 Take the obje t

a

and its type

A

dened at the end of se tion 3.1, by the denitionoflinks,we seethatthe linksofthemethodsin

a

are:

L(l

1 ) = L

a

(s) =

{l

2 , l

3 }

L(l

2 ) = L

a

(1) =

∅

L(l

3 ) = L

a

(λ(x : int )(x + s.l

2 )) =

{l

2 }

whi hmat hthe orresponding linkspe i ations intype

A

.

4 Obje t Type Graphs

4.1 Denitions

Toreveal thestru ture ofobje t omponentinterdependen ies more learlyand fa ilitate

the study of obje t subtyping and behaviors, we introdu e a graphi al representation of

obje t types obje t typegraphs. Wedene dire ted oloredgraphsrst.

Denition 2 (Dire ted Colored Graph) A dire ted olored graph

G

is a 6-tuple

(G

N

, G

A

, C, sr, tg, c)

onsisting of: (1) a set of nodes

G

N

, and a set of ar s

G

A

; (2) a olor alphabet

C

;(3)asour e map

sr : G

A

→ G

N

,andatargetmap

tg : G

A

→ G

N

, whi hreturnthesour enodeandtargetnodeofanar ,respe tively;and(4)a olor map

c : G

N

∪ G

A

→ C

,whi h returnsthe olorof anodeoranar .

Denition 3 (Ground Type Graph) A ground type graph is a single-node olored

di-re tedgraph whi h is oloredby aground type.

Denition 4 (Fun tionTypeGraph) Afun tion type graph

(s, G

1 , G

2 )

(G

N

,G

A

,C,sr,tg,c)

is adire ted olored graph onsisting exa tly of a starting node

s

∈ G

N

, and two type graphs

G

1

and

G

2

, su h that, (1)

c(s) =

→

; (2) there are two ar s asso iated with the starting node

s

, left ar

l

∈ G

A

and right ar

r

∈ G

A

, su h that

c(l) = in

,

c(r) = out

;

(11)

l

onne ts

G

1

to

s

by

sr(l) = s

G

1

,

tg(l) = s

, and

r

onne ts

s

to

G

2

by

sr(r) = s

,

tg(r) = s

G

2

, where

s

G

1

and

s

G

2

are the starting nodes of

G

1

and

G

2

, respe tively; (3)

G

1

and

G

2

are disjoint; (4) if there isan ar

a

∈ G

A

with

c(a) = rec

, then

sr(a) = s

G

i

,

tg(a) = s

,

c(s

G

i

) =

→

,

i = 1, 2

.

Denition 5 (Obje t Type Graph) Anobje t type graph

(s, A, R, L, S)

(G

N

,G

A

,C,sr,tg,c)

isadire ted oloredgraph onsistingexa tlyofastarting node

s

∈ G

N

,asetofmethod ar s

A

⊆ G

A

, aset ofre - olored ar s

R

⊆ G

A

, a set oflink ar s

L

⊆ G

A

, and aset of typegraphs

S

, su h that(1)

c(s) =

self. (2)

∀a ∈ A

,

sr(a) = s

,

tg(a) = s

F

for some type graph

F

∈ S

, and

c(a) = m

forsome methodlabel

m

;

c(a)

6= c(b)

for

a, b

∈ A

,

a

6= b

. (3)

∀r ∈ R

,

c(r) = rec

,

tg(r) = s

,

sr(r) = s

F

for some

F

∈ S

, and

c(s

F

) =

self. (4)

∀l ∈ L

,

sr(l) = s

F

,

tg(l) = s

G

forsome

F, G

∈ S

, and

c(l) = bym

forsome methodlabel

m

. Remarks: Dire ted oloredgraph isthefoundation ofgraphgrammar theory[10,11,

12 , 13 , 22℄. Obje t type graphs are adapted from dire ted olored graphs. Ground type

graphs are trivial. Fun tion type graphs are straightforward. They need to be dened

be ause an obje t type graph may in lude them as subgraphs. An obje t type graph is

formed by astartingnode

s

and a set

S

oftypegraphswith ea h

F

∈ S

being onne ted to

s

by amethod ar that goes from

s

to

F

. Thestartingnode

s

is oloredby selfand is used todenotethe selftype. The method interdependen ies are spe ied by ar s in

L

. If

L(m)

is theset oflinks of method

m

, thenfor ea h

l

∈ L(m)

there is anar ( olored by byl) that goes from

l

to

m

. Re ursive obje t types are spe ially indi ated by re - olored ar s in

R

.

Forthe sakeofbrevity, we dropthesubs riptsin

(s, G

1 , G

2 )

(G

N

,G

A

,C,sr,tg,c)

and

(s, A, R, L, S)

_(G

_N

,G

A

,C,sr,tg,c)

whenever possiblethroughout thepaper.

4.2 Examples of Obje t Type Graphs

We nowprovidesomeexamples toillustrate thedenition ofobje t typegraphs.

Example 2 InFigure5,

A

,

B

,and

C

arethetypegraphsforgroundtypes

int

,

real

,and

bool

respe tively.

D

isthetypegraphforfun tiontype

int

→ int

and

E

isthetypegraph for

(int

→ real) → (real → int)

.

int

in

out

in

out

in

out in

out

int

real

int

real

bool

A

B

C

D

E

(12)

Example 3 InFigure6,graph

A

denotestheobje ttype

[x : int, y : int]

,wheremethods

x

and

y

areindependentofea hother. Graph

B

denotesthetype

[x : int, y(

{x}):int]

where

y

dependson

x

. Notethatthedire tion ofthelinkar in

B

isfrom

x

to

y

,(notfrom

y

to

x

),signifyingthefa t that hangesmadetomethod

x

willae t method

y

.

x

y

self

s

int

x

y

self

s

int

byx

A

B

Figure6: Examplesofobje ttype graphs

Example 4 In Figure 7, graph

C

represents the obje t type

µ(t)ι(s)[a : int, b : t, c : s]

. Method

a

is oftype

int

; method

b

isof re ursive obje t type

C

. Method

c

isof the self type indu ed by the obje t type

C

. Note the stru tural dieren e between the type of

b

andthetypeof

c

revealedinthetypegraph

4

. Graph

D

representsthetypeofasimplied 1-d movable point

[x = 1, mvx = ς(s :

S(D))λ(i : int)(s.x⇐ s.x + i)]

. Thefa ts that

mvx

depends on

x

and returns a modied self are indi ated by the byx- olored ar and the out- olored ar in

D

.

a

b

self

int

x

_mvx

self

s

int

byx

A

B

c

rec

int

in

out

Figure7: Examplesofobje ttype graphs

Example 5 Two more obje t type graphsare shown in Figure 8. They are thetypes of

somevariationsofpoint obje ts. Graph

A

isthe typeofthe obje t





x = 1,

m

1 = ς(s :

S(A))λ(i:int)p

m

2 = ς(s :

S(A))λ(i:int)s





4

Thisstru turalsetting,potentially,willallowthetypeof

c

toremainasselftypeandthetypeof

b

to be hangedaftersomeoperationsongraph

C

areperformed.

(13)

where

p

issome pointobje toftype

A

. Graph

B

isthetype oftheobje t







x = 1

y = 2

d = ς(s :

_{S(B))(s.x + s.y)/2}

e

1 = ς(s :

S(B))λ(p:B)(p.x = s.x ∧ p.y = s.y)

e

2 = ς(s :

S(B))λ(p:S(B))(p.x = s.x ∧ p.y = s.y)







.

m1

m2

self

A

x

rec

self

int

in

out

in

out

byx

self

B

rec

real

int

in

out

in

out

bool

self

bool

x

y

d

e1

_e2

byx

byy

bym1

Figure8: Examplesofobje ttypegraphs

5 Obje t Typing/Subtyping Under OTG

We nowinvestigatethe issueoftyping/subtyping underOTG. Werst dene obje t

sub-typing through a series ofdenitions and then present the typing/subtyping rules witha

briefdis ussion. NotethatOTGisjust anotherway(agraphi al way, spe i ally) to

rep-resent obje t types. There isanatural 1-1 orresponden e between OTGand thenormal

textual representations of obje t types in TOOL. So the typing rules presented in this

se tion naturallyapplytoobje ttypegraphs. What makes OTGsigni antisits

fa ilita-tion of the formulation of obje t subtyping with thepresen e of links in obje t types (as

addressed below).

Denition 6 (Type Graph Premorphism) Let

Φ

be theset ofground types. Giventwo type graphs

G = (G

N

, G

A

, C, sr, tg, c)

and

G

′

_{= (G}

′

N

, G

′

A

, C

′

, sr

′

, tg

′

, c

′

)

, a type graph premorphism

f : G

→ G

′

is apair of maps

(f

N

: G

N

→ G

′

N

, f

A

: G

A

→ G

′

A

)

, su h that (1)

∀a ∈ G

A

,

f

N

(sr(a)) = sr

′

_(f

A

(a))

,

f

N

(tg(a)) = tg

′

_(f

A

(a))

, and

c(a) = c

′

_(f

A

(a))

; (2)

∀v ∈ G

N

, if

c(v)

∈ Φ

,then

c

′

_(f

N

(v))

∈ Φ

;otherwise

c(v) = c

′

_(f

N

(v))

.

Denition 7 (Base, Subbase) Givenanobje t type graph

G = (s, A, R, L, S)

. The base of

G

, denoted by

Ba(G)

, is the graph

(s, A, t(A), L)

, where

t(A) =

{tg(a) | a ∈ A}

. A subbase of

G

isa subgraph

(s, A

′

_{, t(A}

′

_{), L}

′

₎

of

Ba(G)

, where

A

′

_{⊆ A}

,

L

′

_{⊆ L}

,

t(A

′

_{) =}

{tg(a) | a ∈ A

′

_}

, and for ea h

l

∈ L

′

there exist

a

1 , a

2 ∈ A

′

su h that

sr(l) = tg(a

1 )

and

(14)

self

x

y

z

u

int

self

int

real

in

out

m

n

byx

byz

byy

self

u

x

int

self

u

x

int

byx

y

byx

byy

(a) G

byx

self

x

y

z

u

int

self

byx

byz

byy

byx

self

(b) Ba(G)

(c) D

(d) Cl(D)

Figure9: (a)Anobje ttypegraph

G

;(b)Thebase

Ba(G)

of

G

; ( )Asubbase

D

of

G

;(d) The losure

Cl(D)

Denition 8 (Closure, Closed) The losure of a subbase

D = (s, A

′

_{, t(A}

′

_{), L}

′

₎

of an

obje ttypegraph

G = (s, A, R, L, S)

,denotedby

Cl(D)

,istheunion

D

∪E

1 ∪E

2

,where(1)

E

1 =

{l ∈ L | ∃a

1 , a

2 ∈ A

′

with

tg(a

1 ) = sr(l), tg(a

2 ) = tg(l)

}

, and (2)

E

2 =

{l, h, a, t(l) |

l, h

_{∈ L, a ∈ A, a 6∈ A}

′

_{, tg(l) = sr(h) = tg(a),}

and

∃a

1 , a

2 ∈ A

′

su hthat

tg(a

1 ) =

sr(l), tg(a

2 ) = tg(h)

}

. A subbase

D

issaidto be losedif

D = Cl(D)

.

Denition 9 (Covariant,Invariant)Givenanobje ttypegraph

(s, A, R, L, S)

. Let

t(A) =

{tg(a) | a ∈ A}

. Forea h

v

∈ t(A)

, if

v

isnotin ident withanylinks,or if

v

isthetarget node ofsome links but notthe sour e node ofany links,then

v

issaid tobe ovariant; otherwise,

v

issaid tobeinvariant.

Denition 10 (Obje tSubtyping)Giventwoobje ttypegraphs

G = (s

G

, A

G

,

∅, L

G

, S

G

)

and

F = (s

F

, A

F

,

∅, L

F

, S

F

)

.

F <: G

ifandonlyifthefollowing onditionsaresatised: (1) Thereexistsapremorphism

f

from

Ba(G)

to

Ba(F )

su hthat

f (Ba(G)) = Cl(f (Ba(G)))

. That is,

f (Ba(G))

is losed. (2) For ea h node

v

in

f (Ba(G))

, let

u

be its preimage in

Ba(G)

under

f

,

F

v

∈ S

F

bethe type graph with

v

as its startingnode, and

G

u

∈ S

G

be thetypegraph with

u

as itsstarting node. (i)If

v

isinvariant,then

F

v

∼

= G

u

. (ii) If

v

is ovariant,then

F

v

<: G

u

.

Remarks: Type graph premorphism is adapted from graph morphism whi h is a

fundamental on ept in algebrai graph grammars [13 , 10, 22, 11, 12℄. It preserves the

dire tions and olorsof ar s and the olors ofnodes up to ground types. The baseof an

obje ttypegraphsinglesthemethodinterdependen yinformationoutoftheentireobje t

type graph so that the stru ture of the method interdependen ies an be better studied.

The losure of asubbase aptures the omplete behavior of the subbase by in luding, in

addition to all methods and links in the subbase, a set

E

2

of methods (and asso iated links) outside ofthe subbasein the following way: for any method

l

in

E

2

, (1)

l

depends onsomemethodsinsidethesubbase,and (2)thereexistsome methodsinsidethesubbase

thatdependon

l

. Anexampleofbase, subbase, and losure isshownin Figure 9. Obje t subtypingisdenedusingtheideasoftypegraphpremorphism,base,subbase, losure,and

(15)

Then, itusesthevarian einformationofea hmethodto he k thesubtypingfeasibilityof

ea hmethodtype(graph)inasubobje twithits ounterpartinasuperobje t 5

. Notethat

in the denition of obje t subtyping, we only onsider the ase

R =

∅

(i.e., no re ursive obje t types). The ase

R

6= ∅

requires ompli ated graph grammar operations and is beyond the s opeofthispaper.

Thetyping/subtypingrulesofTOOLareshowninTable1. Therulesthatareae ted

by linksare(TObj)and (TUpd). Notethatintheserules,the setoflinks omputed from

termsare he ked againstthe setof linksspe iedintypes.

∅ ⋄

(

TC

∅)

Γ σ

x

6∈ dom(Γ)

Γ, x : σ ⋄

(

TCVar

)

Γ M : σ

x

6∈ dom(Γ)

Γ, x : τ M : σ

(

T

x)

Γ ⋄

Γ κ

(

TyCons

)

Γ σ

Γ τ

Γ σ → τ

(

TyFun

)

Γ σ

i

∀i ∈ {1, . . . , n}

Γ ι(t)[l

i

(L

i

) : σ

i

(t)]

n

_i=1

(

TyObj,

L

i

⊆ {l

1 , . . . , l

n

}

forea h

i)

Γ ⋄

x: σ ∈ Γ

Γ x : σ

(

TVar

)

Γ, x : σ M : τ

Γ λ(x : σ).M : σ → τ

(

TAbs

)

Γ M : σ → τ

Γ N : σ

Γ M N : τ

(

TApp

)

Γ, s : S(A) M

i

: σ

i

L

i

= L

a

(M

i

)

∀i ∈ {1, . . . , n}

Γ a : A

(

TObj,

a

= [l

i

= ς(s : S(A))M

i

]

n

i=1

A

= ι(t)[l

i

(L

i

) : σ

i

(t)]

n

i=1

)

Γ M : A

j

∈ {1, . . . , n}

Γ M.l

j

: σ

j

(A)

(

TInv1,

A

= ι(t)[l

i

(L

i

) : σ

i

(t)]

n

i=1

= [l

i

(L

i

) : σ

i

(S(A))]

n

i=1

)

Γ s : S(A)

j

∈ {1, . . . , n}

Γ s.l

j

: σ

j

(A)

(

TInv2,

A

= ι(t)[l

i

(L

i

) : σ

i

(t)]

n

i=1

= [l

i

(L

i

) : σ

i

(S(A))]

n

i=1

)

Γ N : A

Γ, s : S(A) M : σ

i

L

i

= L

N

(M )

i

∈ {1, . . . , n}

Γ N.l

i

⇐ ς(s : S(A))M : A

(

TUpd,

A

= ι(t)[l

i

(L

i

) : σ

i

(t)]

n

i=1

)

Γ σ

Γ σ <: σ

(

SRe

)

Γ σ <: τ

Γ τ <: δ

Γ σ <: δ

(

STran

)

Γ a : A

Γ A <: B

Γ a : B

(

SSump

)

Γ σ

′

_{<: σ}

_{Γ τ <: τ}

′

Γ σ → τ <: σ

′

_{→ τ}

′

(

SFun

)

Γ G

A

<: G

B

Γ A <: B

(

SObj

,

G

A

and

G

B

aretheOTGsof

A

and

B

respe tively

A

= ι(t)[l

i

(L

i

) : σ

i

(t)]

n

i=1

, B

= ι(t)[l

i

′

(L

′

i

) : σ

′

i

(t)]

n

′

i=1

)

Table1: TypingandsubtypingrulesforTOOL

We would like to emphasize that the purpose of obje t type graphs is to fa ilitate

the formulation and reasoning of obje t subtyping when method interdependen ies are

onsidered in obje t types. This an be seen in the obje t subtyping rule (SObj) where

the determination of

A <: B

for obje t types

A

and

B

dependson whether their obje t typegraphs

G

A

and

G

B

have asubtyping relationshipwhi h, inturn, an be de idedby

5

(16)

the Denition 10. (Denition 10 suggests an immediate algorithm for how to ompute

G

A

<: G

B

.)

6 Veri ation of the Program

ms

under OTG

Wehaveshown,inse tion2,thatunder onventionalobje ttypesystems,thereisnoway

to ode the fun tion

ms

satisfa torily in the sense that we are unable to prove that

ms

performs to its spe i ation for allpermissible arguments. In thisse tion, we show that

thisproblem anbe easily resolvedunder OTG typing/subtyping. That is,we show that

ms

anbe oded reliably under OTG typing/subtyping and prove that itperforms to its spe i ation in allsituations.

Given the odeof

ms

in Figure 3and under the OTGnotation, the type ofthepoint

p

1n

(whi hisalsothetypeoftheparameter inthefun tion

ms

)and thetypeofthepoint

p

′

2n

aredepi tedas

P

and

Q

′

2n

inFigure10 6

. Let

f

bethepremorphism frombase

Ba(P )

tobase

Ba(Q

′

2n

)

,

f (Ba(P ))

andits losure

Cl(f (Ba(P )))

arealsoshowninFigure10. By the OTG obje t subtyping denition (Denition 10), we an see that

Q

′

2n

6<: P

be ause

f (Ba(P ))

_{6= Cl(f(Ba(P )))}

(i.e.,

f (Ba(P ))

is not losed). Hen e,

p

′

2n

annot be viewed as having type

P

and

ms(p

′

2n

)

does not type- he k. The run-time error of

ms(p

′

2n

)

is therefore preventedby type he king at ompile-time. Hen e, the odeof

ms

in Figure 3 issafeunder theOTG typing/subtyping.

self

real

x

mvx

byx

in

real

out

dist

x

y

mvx

mvy

byx

byy

real

self

real

byx

byy

in

out

in

out

byx

P

Q’

_2n

dist

x

mvx

byx

real

self

dist

x

y

mvx

byx

byy

real

self

real

byx

f(Ba(P))

Cl(f(Ba(P )))

Figure10: ResolutionofthemovablepointprobleminOTG

Tofullyrevisit ofthe movable point problem in the ontext ofOTG, the type graphs

of

p

1c

,

p

2c

, and

p

2n

are depi ted inFigure 11as

Q

1c

,

Q

2c

, and

Q

2n

, respe tively. We an easily he k, using Denition 10, that

Q

1c

<: P

,

Q

2c

<: P

, and

Q

2n

<: P

all hold. This shows that the desired exe utions

ms(p

1c

)

,

ms(p

2c

)

, and

ms(p

2n

)

are all supported by OTGtyping/subtypings heme.

From Figure 10 and Figure 11, we see that the type of

p

′

2n

and the type of

p

2n

are dierentunderOTG(asopposedtothesamein onventional typesystems). Thefa tthat

method

y

depends on method

x

in

p

′

2n

and method

y

does not depend on method

x

in

p

2n

(i.e.,

p

2n

and

p

′

2n

have dierent behaviors) isfaithfully aptured in their type graphs

6

(17)

self

real

x

mvx

byx

in

real

out

dist

x

y

mvx

mvy

byx

byy

real

self

real

byx

byy

in

out

in

out

dist

x

y

mvx

mvy

byx

byy

real

self

real

byx

byy

in

out

in

out

byx

Q

1c

2c

Q

2n

clr

color

clr

Figure11: Typesof

p

1c

,

p

2c

,and

p

2n

inOTG

as the presen e/absen e of a link from method

x

to method

y

. Indeed, this distin tion is ne essary in order to prevent run-time errors su h as those aused by

ms(p

′

2n

)

. This observationleads tothe following proposition.

Proposition1 Let

A

be the type of an obje t

a

in whi h there is a link between method

x

and method

y

. Let

B

be the type ofan obje t

b

whi h is modied from

a

by deletingthe link between method

x

and method

y

. Then

A

6= B

.

Also note that in Figure 10 and Figure 11, we have

Q

′

2n

6<: Q

2n

(we aneasily verify thisbyDenition10). Thisdisallowan eofsubtypingisalsone essaryinordertostati ally

prevent similarrun-timeerrors ausedby

ms(p

′

2n

)

. Thus,

Proposition2 Let

A

and

B

be asspe ied inProposition1. Then

A

6<: B

.

We now show the orre tness of

ms

in Figure 3 under the OTG typing s heme. We assume that all arguments (1-d points, 2-d points,

. . .

) submitted to

ms

are orre tly oded. In parti ular, if

p

is an

n

-dimensional point with oordinates

x

1 , . . . , x

n

, then its method

dist

must have

px

2

1 +

· · · + x

2 n

as the body; and its method

mvx

must have

λ(i : real )s.x

_{⇐(s.x + i)}

as thebody;how othermethodsin

p

are odedisirrelevant tothe proof. This isa reasonable assumption, for if

p

is odedin orre tly or arbitrarily (say,

p

's

dist

bodyis

px

2

1 + 4x

2

2 +

· · · + n

2 x

2 n

),thentherewouldbenowaytoexpe twhatkind ofbehavior

ms

anhavewith

p

asitsargument.

Tofa ilitate theproof,we rewritethe fun tionalprogram

ms

in Figure 3equivalently intoanimperativeonein Figure12, where

a

holdsthe omputationresult. Wewouldlike to prove, under theframework ofHoarelogi (e.g. [16 ,17℄),thatthetwoHoaretriples

(

_{|p.dist > 1 ∧ p:P |)ms(p)(|p.dist > 1 ∧ p:P |)}

(

_{|p.dist ≤ 1 ∧ p:P |)ms(p)(|p.dist ≤ 1 ∧ p:P |)}

are valid for any point

p

oftype

P

in Figure 10. The rst triple spe ies that

ms

keeps a olored point in the olored point areaafter moving it. These ond triplespe ies that

ms

keepsanon- oloredpointinthenon- oloredpointareaaftermovingit. Beforeproving the validity of the triples, we prove a lemma rst. Let olored points and non- olored

(18)

ms

def

= f un(p : P )

{

real a

; if(

p

.dist > 1

){

p.mvx(δ)

; //

δ > 0

a = sin

-

1 (

1 /p.dist)

; } else{

p.mvx(

₋

1

2 p.x)

;

a = sin

-

1 (p.dist)

; } }

Figure12: Theimperative versionoftheprogram

ms

.

Lemma 1 Given an

n

-dimensional point

p

, if

p

is a non- olored point and is of type

P

in Figure 10, then after being moved, along the

x

-axis and towardsthe origin, half of the proje tion of the distan e from the originto

p

's urrent positionover the

x

-axis,

p

is still inthe non- olored point area inthe spa e.

Proof: Without loss of generality, we assume that the oordinates of

p

are

x

1 , x

2 , . . . , x

n

(

n > 1

) with

x

1

being the

x

- oordinate,

x

2

being the

y

- oordinate,

. . .

. Sin e

p

isa non- oloredpoint,wehave

px

2

1 +

· · · + x

2 n

≤ 1

. After

p

ismovedasspe ied, its

x

- oordinate wouldbe hanged to

1

2 x

1

. Sin e

p

is

n

-dimensional and

n > 1

, the a tual typeof

p

must beasubtypeof

P

. BythedenitionofOTGsubtyping (Denition 10),weknowthat the

x

- oordinate hange of

p

will not ae t any other oordinates

x

2 ,

· · · , x

n

of

p

be ause all

x

2 ,

· · · , x

n

o ur in the method

dist

of

p

and

dist

appears in type

P

7

. Thus,

x

2 , . . . , x

n

all retain their old values after

p

's move. Therefore, the distan e from the origin to the new positionof

p

is

q

(

1

2 x

1 )

2 + x

2

2 + · · · + x

2 n

<

px

1

2 + x

2

2 + · · · + x

2 n

≤ 1

, indi ating the

p

isstill

inthe non- oloredpointarea.

2

Thevalidity ofthese ond Hoaretripleisgiven inTheorem 1below. The proofof the

rstHoare tripleissimilarand omitted.

Theorem 1 Given the program

ms

inFigure 12,the Hoare triple

(

_{|p.dist ≤ 1 ∧ p:P |)ms(p)(|p.dist ≤ 1 ∧ p:P |)}

is valid.

Proof: Theproof,showninFigure13,isanappli ationofthestandardimperativeprogram

veri ationrules(seee.g.[17 ℄). InFigure13,

p.d

and

p.m

standfor

p.dist

and

p

.mvx

,and

A

,

B

,

C

,

D

,

E

,

F

,

G

standforthefollowing triples respe tively: 7

Here isasubtlepoint indi atedbytheOTGobje tsubtyping: ifanyofthe oordinates

x

2 , . . . , x

n

, say

x

i

,doesnot o urinmethod

dist

(orinanyothermethodin ludedintype

P

),thenweallow

x

i

be ae tedbythe hangesof

x

1

whilerequiringthatthetypeof

p

isasubtypeoftype

P

.

(19)

(

_{|p.d ≤ 1 ∧ p : P |){p.m(−}

1 ₂

p.x)

_{}(|p.d ≤ 1 ∧ p : P |)}

,

(

_{|p.d ≤ 1 ∧ p : P |){a = sin}

-

1 (p.d)

_{}(|p.d ≤ 1 ∧ p : P |)}

,

(

_{| ⊥ |){p.m(δ); a = sin}

-

1 (

1 /p.d)

_{}(|p.d ≤ 1 ∧ p : P |)}

,

(

|p.d ≤ 1 ∧ p : P |){p.m(−

1

2 p.x); a = sin

-

1 (p.d)

}(|p.d ≤ 1 ∧ p : P |)

,

(

|p.d ≤ 1 ∧ p : P ∧ p.d > 1|){p.m(δ); a = sin

-

1 (

1 /p.d)

}(|p.d ≤ 1 ∧ p : P |)

,

(

_{|p.d ≤ 1 ∧ p : P ∧ p.d ≤ 1|){p.m(−}

1 ₂

p.x); a = sin

-

1 (p.d)

_{}(|p.d ≤ 1 ∧ p : P |)}

,

(

_{|p.d ≤ 1 ∧ p : P |)ms(p)(|p.d ≤ 1 ∧ p : P |)}

.

Thevalidity oftriple

A

onthetopoftheprooftreeisprovided byLemma 1.

2 C

E

(impli ation)

A

(Lemma1)

B

(assignment)

D

( omposition)

F

(impli ation)

G

(

if-statement

)

Figure13: Theproofof

ms

'sproperty

7 Con lusion and Future Work

Typing isane ient meansinprogram veri ations. Obje t omponent interdependen y

informationis riti alindeterminingandpredi tingobje tbehaviorsandinshapingobje t

types. Ifthis information isnot aptured in obje t typing,as is the ase in onventional

obje ttypesystems,thenastati allywell-typedprogrammaygowrongatrun-time ausing

run-timeerrorsandprogramveri ationtroubles. Weproposedobje ttypegraphs(OTG)

as aninitial treatment for handlingobje t omponent interdependen ies in obje t typing

and program veri ations. We have seen that due to OTG's ability of revealing more

information aboutobje tbehaviors,

•

Programs that go wrong at run-time in onventional obje t type systems an be ee tivelydete tedat ompile-time under OTGtyping/subtyping.

•

Programveri ationsthat annotbedonewith onventionalobje ttypesystems an be easily arried outwiththesupportofOTG typing/subtyping.

This demonstrates that OTG is a safer typing s heme than onventional ones, and

provides a valuable support for OOP program veri ations. The following issues are of

immediate interests forfuturework:

•

Devise alink omputationalgorithmand assessits omplexity.

•

Prove/disprove that thestandardpropertiesoftype systems,su has subje t redu -tion andsoundness, holdunder OTG.

•

As far as applying the idea of OTG to pra ti al obje t-oriented languages is on- erned,webelievethatadire t approa hwouldbetoadaptOCaml[1℄bymodifying

(20)

obje t-forea hofits lasses. Inasense,thetypeofa lassinOCamlisthe(moreabstra t)

typeoftheobje tgeneratedbythat lass. Thisisatypi al asewhere pra ti e

ben-ets from theory, and itwould bevery interesting to keep extending OCaml along

thisline.

Referen es

[1℄ http:// aml.inria.fr/o aml/. 2007.

[2℄ M.AbadiandL.Cardelli. ATheory ofObje ts. Springer-Verlag,NewYork,1996.

[3℄ V. Bono, M. Bugliesi, M. Dezani-Cian aglini, and L. Liquori. Subtyping for Extensible,

In ompeteobje ts. FundamentaInformati ae,38(4):325364,1999.

[4℄ V. Bono and L. Liquori. A subtyping for the Fisher-Honsell-Mit hell lambda al ulus of

obje ts. In Pro . of International Conferen e of Computer S ien e Logi , number 933 in

LNCS,pages1630.1995.

[5℄ K.Bru e. Aparadigmati obje t-orientedprogramminglanguage: Design,stati typingand

semanti s. Journal ofFun tionalProgramming,4(2):127206,1994.

[6℄ K.Bru e. FoundationsofObje t-Oriented Languages. MITPress,2002.

[7℄ K.Bru e,A.S huett,R.van Gent,andA.Fie h. Polytoil: Atype-safepolymorphi

obje t-orientedlanguage. ACM Transa tions on Programming Languagesand Systems,25(2):225

290,2003.

[8℄ W.Cook,W.Hill,andP.Canning. Inheritan eisnotsubtyping. InPro eedingsofthe17the

AnnualACMSymposium onPrin iples ofProgrammingLanguages,pages125135,1990.

[9℄ R.DelineandM. Fahndri h. Typestatesforobje ts. In ECOOP2004, 2004.

[10℄ H.Ehrig. Introdu tiontothealgebrai theoryofgraphgrammars.In Graph-Grammars and

TheirAppli ationstoComputerS ien eandBiology,volume73ofLe tureNotesinComputer

S ien e,pages169.Springer-Verlag,1978.

[11℄ H.Ehrig,G.Engels,H.-J.Kreowski,andG.Rozenberg,editors.HandbookofGraphGrammars

andComputingbyGraphTransformation,volume2. WorldS ienti ,1999.

[12℄ H. Ehrig, H.-J. Kreowski, U. Montanari, and G. Rozenberg, editors. Handbook of Graph

GrammarsandComputing byGraph Transformation,volume3. World S ienti ,1999.

[13℄ H. Ehrig, M. Pfender, and H. J. S hneider. Graph grammars: An algebrai approa h. In

IEEEConferen eofAutomataand Swit hingTheory,pages167180,1973.

[14℄ K.Fisher,F.Honsell,andJ.Mit hell.Alambda al ulusofobje tsandmethodspe ialization.

Nodi JournalofComputing,1:337,1994.

[15℄ J.Hi key. Introdu tionto OCaml,http:// aml.inria.fr/tutorials-eng.html. 2002.

[16℄ C.A.R.Hoare.Anaxiomati basisfor omputerprogramming.Communi ationsoftheACM,

12:576580,1969.

[17℄ M.HuthandM.Ryan. Logi inComputerS ien e.CambridgeUniversityPress,2ndedition,

2004.

(21)

[19℄ L.LiquoriandG.Castagna. ATypedLambdaCal ulusofObje ts. Number1179inLe ture

NotesinComputerS ien e,pages129141.SpringerVerlag,1996.

[20℄ B.LiskovandJ.Wing. ABehavioralNotionofSubtyping. ACM Transa tions on

Program-mingLanguagesandSystems,16(6):18111841,1994.

[21℄ O. L. Madsen. TowardsIntegrationof StateMa hines and Obje t-Oriented Languages. In

Te hnologyofObje t-OrientedLanguagesandSystems(TOOLSEurope'99),1999.

[22℄ G.Rozenberg,editor. Handbookof Graph GrammarsandComputing byGraph