Logic and Computational Complexity, Wroclaw, Poland, July 15, 2007

1

arXiv:0706.2293v1 [] 15 Jun 2007

Resource control of object-oriented programs
Jean-Yves Marion and Romain Péchoux
Loria, Carte project, B.P. 239, 54506 Vandœuvre-lès-Nancy Cedex, France,
and École Nationale Supérieure des Mines de Nancy, INPL, France.
jean-yves.marion@loria.fr romain.pechoux@loria.fr

February 9, 2018

Abstract
A sup-interpretation is a tool which provides an upper bound on
the size of a value computed by some symbol of a program. Supinterpretations have shown their interest to deal with the complexity
of first order functional programs. For instance, they allow to characterize all the functions bitwise computable in Alogtime. This paper is
an attempt to adapt the framework of sup-interpretations to a fragment
of oriented-object programs, including distinct encodings of numbers
through the use of constructor symbols, loop and while constructs and
non recursive methods with side effects. We give a criterion, called
brotherly criterion, which ensures that each brotherly program computes objects whose size is polynomially bounded by the inputs sizes.

1

Introduction

A sup-interpretation is a tool introduced in [13] in order to deal with the
Implicit Computational Complexity of first order functional programs. Basically, the sup-interpretation of a first order functional program provides
upper bounds on the size of any value computed by some function symbols of
the program. The notion of sup-interpretation is a descendant of the notion
of quasi-interpretation. See [5] for a survey on quasi-interpretations. It has
been demonstrated in [12], that the notion of polynomial sup-interpretation
strictly generalizes the notion of polynomial quasi-interpretation. In other
words, every polynomial quasi-interpretation is a polynomial sup-interpretation and there are programs which admit a sup-interpretation and no quasiinterpretation. As a consequence, sup-interpretation provides more intentionality than quasi-interpretation, i.e. it allows to capture the complexity
of more algorithms. Such a flexibility is very interesting when we consider
small complexity classes. For example, in [6], sup-interpretations allow to
characterize all the functions bitwise computable in alternating logarithmic

2 OBJECT-ORIENTED PROGRAMS

2

time. Another interesting consequence develloped in [13] consists in an application of the sup-interpretation tool to termination criteria such as the
dependency pairs [3] or the size change principle [11].
The notion of quasi-interpretation has already been extended to Bytecode verification and to reactive programs. See for example [1, 2, 7]. Consequently, a major issue consists in the adaptation of the sup-interpretation
analysis to imperative and object-oriented programs. We try to tackle this
problem in this paper by enlarging the framework of sup-interpretations to
a fragment of object-oriented programs without recursion. Our language
is very similar to the language studied in [9]. However, since we consider
assignments, it is closer to a fragment of [8] where we add loop and while
constructs. A consequence is that we have to control side effects. Our work
is inspired by recent studies on the Implicit Computational Complexity of
imperative programs [14, 10]. Contrarily to these seminal works, we work
on polynomial algebra instead of matrix algebra. There are at least two reasons for such an approach. Firstly, the use of polynomials gives a clearest
intuition and pushes aside a lot of technicalities. Secondly, polynomials give
more flexibility in order to deal with method calls.
The paper is organized as follows. After introducing our language and
the notion of sup-interpretation of an object-oriented program, we give a criterion, called brotherly criterion, which ensures that each brotherly program
computes objects whose size is polynomially bounded by the inputs sizes,
even if the program is defined with function calls. To our knowledge, previous works on the implicit computational complexity of imperative programs
did not support such a flexibility. Consequently, this criteria seems to be a
great improvement on the study of the complexity of imperative programs.

2
2.1

Object-oriented Programs
Syntax of programs

We consider object-oriented programs. Basically a program is composed by
three sets of disjoint symbols X , P and F and a set Class ⊆ F. The set
X represents the set of attributes. Throughout the following paper, we use
capital letters X, Y, Z, . . . for attributes. The set P is the set of parameters
which are passed as arguments of a method. The symbols of Class are the
class identifiers. They provide distinct data encodings such as the unary
encoding, using the identifier S for a class having one attribute and the
identifier ǫ for a class without any attribute, or the binary encoding, using
the class identifiers 1 and 0. Each function symbol f ∈ F must be defined
by one method of some class. A class C ∈ Class is composed by attribute
and method declarations, including a particular constructor method, which
are described by the following grammar:

2 OBJECT-ORIENTED PROGRAMS

3

Attributes ∋ A
Expressions ∋ e
Commands
∋ Cm
Methods
Class

::= var X; | var X; A
::= x | X | X.f(e1 , · · · , en ) | new C(e1 , · · · , en )
::= skip | X := e | Cm1 ; Cm2 | loop X {Cm}
| if e then Cm1 else Cm2 | while e {Cm}
∋M
::= f(x1 , ..., xn ) {Cm ; return X; }
∋C
::= Class C {A ; Cons ; M1 ; . . . ; Mn ; }
main ::= Class main {A ; Cm}

where X ∈ X , x, x1 , · · · , xn ∈ P, f ∈ F, e1 , · · · , en ∈ Expressions and
M1 ; . . . ; Mn ∈ Methods. The method Cons is a special constructor method
of the shape C(x1 , ..., xn ) {X1 := x1 ; . . . ; Xn := xn } which appears in each
class C ∈ Class whenever the class C has n attributes X1 , · · · , Xn . As a
consequence, we have Class ⊆ F. This particular method can only be used
in a command of the shape X := new C(e1 , · · · , en ). All attributes appearing
in the methods of a given class Class must belong to the attributes of this
class. Finally, we define the main class main to be a special class defined by
attributes declarations and commands.
We suppose that the attributes and methods of two distinct classes are
pairwise distinct.
For notational convenience, we sometimes refer to e as a sequence of
expressions e1 , · · · , en , whenever n is clear from the context.
Given a program p, we define a precedence ≥F on function symbols of F.
Set f ≥F g if the method defining f is of the shape f(x) {Cm ; return X; }
and the function symbol g appears in Cm. Take the reflexive and transitive
closure of ≥F , that we also note ≥F . It is not difficult to establish that ≥F is
a preorder. Lastly, we say that f >F g if f ≥F g and g ≥F f does not hold.
Intuitively, f >F g means that f cannot call g. Throughout the following
paper, we suppose that for each method of the shape f(x) {Cm ; return X; }
and for each function symbol g which occurs in Cm, f >F g, i.e. there is no
recursive call in the program.
For each expression e of a program, we suppose that function symbols
f ∈ F − Class appear only in the outermost position of an expression e.
This restriction allows to deal with side effects in a clearest fashion. This is
not a severe restriction since every program can be transformed efficiently
in an equivalent program which does fit this requirement, by adding new
attributes for the intermediate computations. For example, a command of
the shape X := V.f(U.g(X)) is transformed into Y := U.g(X); X := V.f(Y )
with Y a fresh attribute. For simplicity, we suppose, that no function symbol
appears in the expression e of the commands if e then Cm1 else Cm2 and
while e {Cm}.
The attribute X is not allowed to occur in the command Cm of an iteration
of the shape loop X {Cm}. The attribute X is not allowed to occur in
a method of the shape f(x) {Cm′ ; return Y ; }, if the function symbol f

4

2 OBJECT-ORIENTED PROGRAMS

appears in the command Cm of an iteration loop X {Cm}. In other words,
the program is not allowed to read and to write the attribute X during the
execution of a loop X {Cm}.
Example 2.1: Here is an example of a program of our language:
Class Position {
var X; var Y ;
Position(x, y) {X := x; Y := y; }
move(x, y) {X := X.add(x); Y := Y.add(y) ; return X; }
getX() {skip ; return X; }
}
Class main {
var W ; var U ; var V ; Var Z;
Cm1 : V := new Position(W, U );
Cm2 : Z := V.move(W, W );
Cm3 : U := V.getX();
}
where Cm1 , · · · , Cm3 are labels used to refer to commands and add is a method
which is not described in the program and which corresponds to the unary
or binary addition depending on the kind of defined objects.

2.2

Semantics

The domain of computation is the set of objects defined inductively by:
Objects ∋ v ::= b | b(v1 , · · · , vn )

b ∈ Class

Given a main class having n attributes X1 , · · · , Xn , an object vi is stored in
each Xi at any time.
A ground substitution σ represents a store which consists in a total
mapping from X to objects in Objects. Given a ground substitution σ and
an attribute X, the notation σ {X := u} means that the object stored in
Xσ is updated to the object u in σ. A parameter substitution β is a total
mapping from P to objects in Objects. Given an expression e and a ground
substitution σ, we use the notation he, σi → hu, σ ′ i whether the expression
e evaluates to u and the store σ is updated to σ ′ . We use the notation
hCm, σi → hσ ′ i, if σ is updated to σ ′ during the execution of the command
Cm. Given a program p of main class Class main {A; Cm} and a store σ, p
computes a store σ ′ defined by hCm, σi → hσ ′ i.
The operational semantics of our language is inspired by the operational
semantics of the java fragment given in [8] and is described in Figure 1.

5

2 OBJECT-ORIENTED PROGRAMS

h⋄, σi → h⋄σ, σi
he, σi → hu, σi

⋄∈X ∪P

f(x) {Cm ; return Y ; }

∃β, xβ = u

hCmβ, σi → σ ′

hX.f(e), σi → Y σ ′ , σ ′
he, σi → hu, σi
hnew C(e), σi → hC(u), σi

C ∈ Class

he, σi → u, σ ′
hX := ei → hσ {X := u}i
hskip, σi → hσi
hCm1 , σi → σ ′

Cm2 , σ ′ → σ ′′

hCm1 ; Cm2 , σi → σ ′′
he, σi → h1, σi , h0, σi or hu, σi
hif e then Cm1 else Cm2 , σi → hCm1 , σi , hCm2 , σi or hskip, σi
D

|vi |

hloop Xi {Cm} , σi → Cm

,σ

with u > 1

E with Cmn = Cm; Cmn−1 and Cm0 = skip

he, σi → h1, σi or h1, σi
hwhile e {Cm} , σi → hCm; while X {Cm} , σi or hskip, σi

with u 6= 1

Figure 1: Call-by-value semantics
If f is defined by a method of the shape f(x) {Cm ; return Y ; }, then the
evaluation of X.f(u) is performed by first evaluating the body Cmβ, with β
a parameter substitution such that xβ = u, in the context of the object X
and then returning the value stored in the attribute Y of the object X.
The command skip does nothing. The command X := e assigns the
value of e to the attribute X. The command X := new C(e1 , · · · , en ) first
evaluates the expressions e1 , · · · , en to the objects v1 , · · · , vn , then, it creates a new object of the class C by assigning the value C(v1 , · · · , vn ) to the
attribute X. The execution of Cm1 ; Cm2 corresponds to the sequential execution of Cm1 and Cm2 . if b then Cm1 else Cm2 executes the command Cm1 ,
Cm2 or skip depending on whether the expression b is respectively evaluated
to an encoding of 1, 0 or another natural number. The size |v| of a value v
is defined to be the number of symbols of strictly positive arity in v. The
command loop X {Cm} executes |v| times the command Cm if v is the value

3 SUP-INTERPRETATIONS AND WEIGHTS

6

stored in X, i.e. Xσ = v. Finally the command while b {Cm} is evaluated to
Cm; while b {Cm} if b is evaluated to an encoding of 1 and to skip otherwise.
Example 2.2: Consider the program of Example 2.1. For each objects
u, v, w, z such that σ = {U := u, V := v, W := w, Z := z}, we have:
hnew Position(W, U ), σi → hPosition(w, u), σi
hV := new Position(W, U ), σi → hσ {V := Position(w, u)}i
Moreover if v = Position(w, u) then:
hV.getX(), σi → hw, σi
hU := V.getX(), σi → hσ {U := w}i

3

Sup-interpretations and weights

3.1

Assignments

Definition 3.1: Given a class C having n attributes X1 , · · · , Xn , the assignment I of the class C is a mapping of domain dom(I) ⊆ F which assigns a
function I(f) : (R+ )m+1 7−→ R+ to every symbol f ∈ F − Class of arity m,
which corresponds to a method of the class C, and which assigns a function
I(C) : (R+ )n 7−→ R+ to the constructor method of C.
Given a program p, the assignment I of p consists in the union of the
assignments of each class C of Class.
A program assignment I is defined over an expression e if each symbol
of F in e belongs to dom(I). Suppose that the assignment I is defined over
an expression e, The partial assignment of e w.r.t. I, that we note I ∗ (e) is
the canonical extension of the assignment I defined as follows:
1. If ⋄ is in X ∪ P, then I ∗ (⋄) = ⋄
2. If e is a sequence of expressions e1 , · · · , ek , I ∗ (e) = I ∗ (e1 ), . . . , I ∗ (ek ).
3. If C is a symbol in Class of arity m and e1 , · · · , em are expressions,
then, we have:
I ∗ (new C(e1 , · · · , em )) = I(C)(I ∗ (e1 ), . . . , I ∗ (em ))
4. If f ∈ F − Class is a symbol of arity m and e1 , · · · , em are expressions,
then, we have:
I ∗ (X.f(e1 , · · · , em )) = I(f)(I ∗ (e1 ), . . . , I ∗ (em ), X)

3 SUP-INTERPRETATIONS AND WEIGHTS

7

Notice that the assignment I ∗ (e) of an expression e with m parameters x occurring in a class C having n attributes denotes a function from
(R+ )n+m → R+ . Consequently, we use the notation I ∗ (e)(X1 , · · · , Xn , x)
when we apply such a function.
Definition 3.2: Let Max-Poly {R+ } be the set of functions defined to
be constant functions in R+ , projections, max, +, × and closed by composition. Given a class with n attributes, an assignment I is said to be polynomial if for every symbol b of dom(I), I(b) is a function of Max-Poly {R+ }.
Definition 3.3: The assignment of a class symbol C ∈ Class of arity
m > 0 is additive if
I(C)(⋄1 , · · · , ⋄m ) =

m
X

⋄i + αC where αC ≥ 1

i=1

If the assignment of each class symbol of strictly positive arity is additive
then the assignment is additive.
Definition 3.4: The size of an expression e is noted |e|Pand defined
by |e| = 0 if e is a 0-ary symbol and |b(e1 , . . . , em )| = 1 + i |ei | if e =
b(e1 , . . . , em ) with m > 0.
Lemma 3.1: Given a program p having an additive assignment I, there
is a constant α such that for each object v ∈ Objects, the following inequality is satisfied:
|v| ≤ I ∗ (v) ≤ α × |v|
Proof: Define α = maxc∈C (βc ) where βc is taken to be the constant αc of
definition 3.1 if c is of strictly positive arity and βc is equal to the constant
I ∗ (c) otherwise. The inequalities follow directly by induction on the size of
a value.

3.2

Sup-interpretations

Definition 3.5: Given a program p of main class having n attributes
X1 , . . . , Xn , a sup-interpretation is an additive assignment θ of p which
satisfies:
1. The assignment θ is weakly monotonic. That is, for each symbol b ∈
dom(θ), the function θ(b) satisfies:
∀i, ⋄i ≥ ⋄′i ⇒ θ(b)(. . . , ⋄i , . . .) ≥ θ(b)(. . . , ⋄′i , . . .)
2. For each function symbol f ∈ dom(θ) − Class of arity m, for each m
tuple of objects v, and for each store σ if hXi .f(v), σi → hv, σ ′ i then
θ(f)(θ ∗ (v), θ ∗ (Xi σ)) ≥ max(θ ∗ (v), θ ∗ (Xi σ ′ ))

8

3 SUP-INTERPRETATIONS AND WEIGHTS

Intuitively, the sup-interpretation is a special interpretation of a symbol.
Instead of yielding the symbol denotation, a sup-interpretation of a function
symbol provides an upper bound on the outputs sizes of the function denoted
by the symbol. It is worth noticing that sup-interpretation is a complexity
measure in the sense of Blum [4].
Example 3.3: Suppose that the method add of Example 2.1 is defined
over an encoding of unary numbers using two class constructor symbols S
and ǫ of respective arity 1 and 0. It admits the following additive and polynomial sup-interpretation θ(add)(⋄1 , ⋄2 ) = ⋄1 +⋄2 , θ(S)(⋄) = ⋄+1 and θ(ǫ) = 0.
Indeed, this function is monotonic. For every unary number Sv (ǫ), we let the
reader check that θ ∗ (Sv (ǫ)) = |Sv (ǫ)| = v. Moreover, for every unary number
Sv (ǫ) and for every store σ such that Xσ = Su (ǫ),with Sn+1 (ǫ) = S(Sn (ǫ))
and S0 (ǫ) = ǫ, if hX.add(Sv (ǫ)), σi → Sv+u (ǫ), σ X := Sv+u (ǫ) , then:
θ ∗ (add)(θ ∗ (Sv (ǫ)), θ ∗ (Su (ǫ))) = θ ∗ (Su (ǫ)) + θ ∗ (Sv (ǫ))
=u+v

By Dfn of θ
θ ∗ (Sv (ǫ)) = v

≥ max(u + v, u)
= max(θ ∗ (Su+v (ǫ)), θ ∗ (Su (ǫ)))
So that, Condition 2 of Definition 3.2 is checked.
Lemma 3.2: Given a program p of main class having n attributes
X1 , . . . , Xn and having a sup-interpretation θ defined over an expression
e, then, for each parameter substitution β, θ ∗ (eβ) denotes a function from
(R+ )n to R+ which satisfies:
For each store σ, if heβ, σi → hv, σ ′ i then
θ ∗ (eβ)(θ ∗ (X1 σ), . . . , θ ∗ (Xn σ)) ≥ θ ∗ (v)
Moreover, if e = Xi .f(e1 , · · · , en ), we have:
θ ∗ (eβ)(θ ∗ (X1 σ), . . . , θ ∗ (Xn σ)) ≥ θ ∗ (Xi σ ′ )
Example 3.4: Consider the program of Example 2.1. As demonstrated
in Example 3.2, θ(add)(⋄1 , ⋄2 ) = ⋄1 +⋄2 , θ(S)(⋄) = ⋄+1 and θ(ǫ) = 0 define a
sup-interpretation for the method add. The method move admits the following sup-interpretation θ(move)(x, y, ⋄) = x + y + ⋄ and θ(Position)(x, y) =
x + y + 1. Indeed, θ(move) and θ(Position) are monotonic and, for each
store σ = {U := u, V := Position(Su1 (ǫ), Su2 (ǫ)), W := Sw (ǫ), Z := z}, we
have:

hV.move(w, w), σi → Su1 +w (ǫ), σ V := Position(Su1 +w (ǫ), Su2 +w (ǫ))

3 SUP-INTERPRETATIONS AND WEIGHTS

9

Since θ ∗ (Sn (ǫ)) = n = |Sn (ǫ)|, we have to check Condition 2 of Definition 3.2:
θ ∗ (V.move(W σ, W σ))(θ ∗ (u, Position(Su1 (ǫ), Su2 (ǫ)), Sw (ǫ), z))
= θ(move)(θ ∗ (W σ), θ ∗ (W σ), V )(θ ∗ (u, Position(Su1 (ǫ), Su2 (ǫ)), Sw (ǫ), z))
= θ(move)(θ ∗ (W σ), θ ∗ (W σ), θ ∗ (Position(Su1 (ǫ), Su2 (ǫ))))
= θ ∗ (W σ) + θ ∗ (W σ) + θ ∗ (Position(Su1 (ǫ), Su2 (ǫ)))
= θ ∗ (Sw (ǫ)) + θ ∗ (Sw (ǫ)) + u1 + u2 + 1
≥ max(w + u1 , 2 × w + u1 + u2 + 1)
= max(θ ∗ (Su1 +w (ǫ)), θ ∗ (Position(Su1 +w (ǫ), Su2 +w (ǫ))))

3.3

Weights

Now, we are going to define the notion of weight which allows to control the
size of the objects held by the attributes during loop and while iterations.
Basically, a weight is a partial mapping over commands. The weights depend
strongly on the considered command, so that we have to make the distinction
between commands.
For that purpose, define the relation ⊑ over commands by Cm1 ⊑ Cm
• if there are Cm2 and Cm3 such that Cm = Cm2 ; Cm1 ; Cm3 ,
• Cm = if e then Cm2 else Cm3 and Cm1 ⊑ Cm2 or Cm1 ⊑ Cm3 ,
• Cm = loop X {Cm2 } and Cm1 ⊑ Cm2 ,
• or Cm = while e {Cm2 } and Cm1 ⊑ Cm2 ,
and its reflexive and transitive closure, that we also note ⊑. ⊑ defines a
partial ordering over commands. The strict relation ⊏ is defined by Cm1 ⊏ Cm
if Cm1 ⊑ Cm and Cm1 6= Cm
Definition 3.6: A command Cm is said to be:
• flat if there is no Cm1 of the shape Cm1 = while e {Cm2 } or Cm1 =
loop X {Cm2 } such that Cm ⊑ Cm2 .
• minimum if there are no commands Cm1 and Cm2 and no expression e
such that Cm = Cm1 ; Cm2 or Cm = if e then Cm1 else Cm2
• whiled if there is a command Cm1 = while e {Cm2 } such that Cm ⊑ Cm1
or Cm1 ⊑ Cm
• looped if if there is a command Cm1 = loop X {Cm2 } such that Cm ⊑
Cm1 and the command Cm2 is not whiled.
Definition 3.7: Given a program p having a main class with n attributes, the weight of a command ω is a partial mapping. It assigns to:

4 CRITERIA TO CONTROL RESOURCES

10

• every flat, minimum and looped command Cm, a total function ωCm
from (R+ )n+1 to R+
• every flat, minimum and whiled command Cm, a total function ωCm
from (R+ )n to R+
which satisfy:
1. ωCm is weakly monotonic ∀i, ⋄i ≥ ⋄′i ⇒ ωCm (. . . , ⋄i , . . .) ≥ ωCm (. . . , ⋄′i , . . .)
2. ωCm has the subterm property ∀i, ∀⋄i ∈ R+ ωCm (. . . , ⋄i , . . .) ≥ ⋄i
A weight ω is polynomial if each ωCm is a function of Max-Poly {R+ }.

4

Criteria to control resources

4.1

Brotherly criterion

The brotherly criterion gives constraints on weights and sup-interpretations
in order to bound the size of the objects computed by the program by some
polynomial in the size of the inputs.
Definition 4.8: A program having a main class with n attributes
X1 , · · · , Xn is brotherly if there are a polynomial sup-interpretation and a
polynomial weight such that:
1. For every flat, minimum and looped command Cm of the main class,
we have:
- For every expression of the shape Xj .f(e1 , · · · , em ) occurring in Cm:
ωCm (T +1, X1 , · · · , Xn ) ≥ ωCm (T, X1 , . . . , Xj−1 , θ ∗ (e)(X), Xj+1 , . . . , Xn )
- For every assignment Xi := e ⊑ Cm, we have:
ωCm (T +1, X1 , · · · , Xn ) ≥ ωCm (T, X1 , . . . , Xi−1 , θ ∗ (e)(X), Xi+1 , . . . , Xn )
with T is a fresh variable.
2. For every flat, minimum and whiled command Cm of the main class,
we have:
- For every expression of the shape Xj .f(e1 , · · · , em ) occurring in Cm:
ωCm (X1 , · · · , Xn ) ≥ ωCm (X1 , . . . , Xj−1 , θ ∗ (e)(X), Xj+1 , . . . , Xn )
- For every assignment Xi := e ⊑ Cm, we have:
ωCm (X1 , · · · , Xn ) ≥ ωCm (X1 , . . . , Xi−1 , θ ∗ (e)(X), Xi+1 , . . . , Xn )

11

REFERENCES

Intuitively, the first condition ensures that the size of the objects held
by the attributes remains polynomially bounded. The fresh variable T can
be seen as a temporal factor which takes into account the number of iterations allowed in a loop. Such a number is polynomially bounded by the
size of the objects held by the attributes. The second condition on whiled
commands is very similar, however there is no more temporal factor, since
we have no piece of information about the termination of a whiled command.
Theorem 4.1: Given a brotherly program p of main class Class main {A; Cm}
having n attributes X1 , · · · , Xn , there exists a polynomial P such that for
any store σ if hCm, σi → hσ ′ i then
P (|X1 σ|, . . . , |Xn σ|) ≥ max (|Xi σ ′ |)
i=1..n

Example 4.5: The program of example 2.1 is brotherly since it admits a
polynomial sup-interpretation θ and it has no looped and whiled command.
Example 4.6: Consider the following program, over unary numbers:
Class main {
var X1 ;
var X2 ;
var X3 ;
loop X1 {
X3 := X3 .add(X2 );
};
}
Cm = loop X1 {X3 := X3 .add(X2 )} is the only minimum, flat and looped
command. Applying the brotherly criterion, we have to find a polynomial
weight ωCm and a polynomial sup-interpretation θ such that:
ωCm (T + 1, X1 , X2 , X3 ) ≥ ωCm (T, X1 , X2 , θ ∗ (X3 .add(X2 )))
with T is a fresh variable.
Since θ(add)(⋄1 , ⋄2 ) = ⋄1 + ⋄2 is a sup-interpretation of the method add,
previous inequality is satisfied by taking ωCm (T, ⋄1 , ⋄2 , ⋄3 ) = T × ⋄3 + ⋄1 + ⋄2
and the program is brotherly.

References
[1] R. Amadio, S. Coupet-Grimal, S. Dal-Zilio, and L. Jakubiec. A functional scenario for
bytecode verification of resource bounds. In CSL, volume 3210 of LNCS, pages 265–279.
Springer, 2004.
[2] R. Amadio and S. Dal-Zilio. Resource control for synchronous cooperative threads. In
Concur, pages 68–82, 2004.

REFERENCES

12

[3] T. Arts and J. Giesl. Termination of term rewriting using dependency pairs. Theoretical
Computer Science, 236:133–178, 2000.
[4] M. Blum. A machine-independent theory of the complexity of recursive functions. Journal
of the Association for Computing Machinery, 14:322–336, 1967.
[5] G. Bonfante, J.-Y. Marion, and J.-Y. Moyen. Quasi-interpretation a way to control resources.
Submitted to Theoretical Computer Science, 2005.
[6] G. Bonfante, J.-Y. Marion, and R. Péchoux. A characterization of alternating log time by
first order functional programs. In LPAR 2006, volume 4246 of LNAI, pages 90–104, 2006.
[7] S. Dal-Zilio and R. Gascon. Resource bound certification for a tail-recursive virtual machine.
In APLAS 2005, volume 3780 of LNCS, pages 247–263. Springer-Verlag, 2005.
[8] S. Drossopoulou and S. Eisenbach. Describing the semantics of Java and proving type soundness. Formal Syntax and Semantics of Java, pages 41–82, 1999.
[9] A. Igarashi, B.C. Pierce, and P. Wadler. Featherweight Java: A Minimal Core Calculus for
Java and GJ. ACM Transactions on Programming Languages and Systems, 23(3):396–450,
2001.
[10] L. Kristiansen and N.D. Jones. The flow of data and the complexity of algorithms. New
Computational Paradigms, 3526:263–274.
[11] C.S. Lee, N.D. Jones, and A.M. Ben-Amram. The size-change principle for program termination. In Symposium on Principles of Programming Languages, volume 28, pages 81–92.
ACM press, january 2001.
[12] J.-Y. Marion and R. Péchoux. Sup-interpretations, a semantic method for static analysis of
program resources. Submitted to TOCL.
[13] J.-Y. Marion and R. Péchoux. Resource analysis by sup-interpretation. In FLOPS 2006,
volume 3945 of LNCS, pages 163–176, 2006.
[14] K.-H. Niggl and H. Wunderlich. Certifying polynomial time and linear/polynomial space for
imperative programs. SIAM Journal on Computing.

