An abstract description of the data model of Featherweight Java is provided,
aimed at a clear definition of the notions of
object, class, instance-of and inheritance.
This document has been created without any prepublication review
except those made by the author himself.
Table of contents
Introduction
Featherweight Java,
or FJ for short,
is a formalism for the description of core features of the Java programming language.
It has been proposed by
A. Igarashi, B.C. Pierce and P. Wadler in October 1999
[]
(with a revised and extended version
[]
published two years later)
as a minimal core calculus for modelling Java's type system.
Since then, FJ became the most popular formalism of its kind,
with a number of similarly named successors like
Middleweight Java[],
Lightweight Java[],
Welterweight Java[],
Extended Featherweight Java[],
Feature Featherweight Java[],
Featherweight Multi Java[],
Imperative Featherweight Java[],
Corecursive Featherweight Java[]
or
FeatherTrait Java[].
Being the most popular scientific simplification of the world's most popular
object-oriented programming language,
Featherweight Java is of importance to the foundations of object-oriented programming.
It is therefore worthwhile to consider FJ from the foundational point of view
and explore alternative ways in which the formalism can be described.
The present document provides such an alternative – an axiomatic description.
Featherweight Java is presented as a family of mathematical structures
devoid of any syntax.
There are just base sorts,
entities derived from these sorts via cumulative application of set-theoretic
constructs and relations between the entities
(some of these relations being definitory and some derived).
The description aims at providing a connection between FJ and the
object models described in other author's documents,
in particular, the F&D model presented in
[].
The what is … questions of FJ
Let us note that the primary goal of the FJ article
[][]
was modelling Java's type system,
focused on a possible application to
Generic Java.
There is no explicitly stated claim that the article is meant to
provide foundations for (core features of) object-oriented programming.
Such an idea appeared rather as an afterthought,
promoted by the authors themselves
(cf.
direct treatment of a core object-oriented language based on Java
on page 247 in
[]
or
A tiny model of (Java-like) class-based OOPLs
in the Table of Contents of
[]).
As a consequence, a reader interested in foundations of OOP
might miss some definitions.
In particular, one might stumble on the following two questions:
(A)
What is an object in Featherweight Java?
(B)
What is a class in Featherweight Java?
The article does not provide a straightforward answer in either case.
After some effort
(depending on the familiarity with type-theoretic conventions)
the reader might figure out the following answer to (A):
In FJ, object is synonymous to well-typed value.
The article does not provide such identification explicitly.
Instead there is just a recursive definition of a value,
v ::= new C(v_{1}, …, v_{n}),
which reads:
A value is an
object creation all of whose arguments are values.
Consequently, the reader is supposed to figure out and accept
that an object is a special case of object creation.
Moreover, the new keyword used in the FJ syntax can be misleading
as to the identity of objects.
For example, using the sample classes Pair and A
from the paper's introduction,
the expression new Pair(new A(), new A())
is an object (a well-typed value) with two fields, named 'fst'
and 'snd',
whose values are identical.
(The A class, having no fields declared or inherited,
has exactly one direct instance, namely new A().
That is, new does not mean new.)
The (B) question is even harder to answer.
A careful reading of the text
reveals that there is in fact no definition of what a class is.
The text only defines class names as abstract entities,
class declarations as composite syntactic forms
and
class table as a mapping from class names to class declarations.
Starting with section 2.1 of
[]
(where the formal definition of FJ begins)
the first occurrence of the standalone term class
(not being a subterm of either
class name or
class declaration)
appears in the following sentence on page 405:
The class declaration
class C extends D {Cf; K M}
introduces a class named C with superclass D.
The reader is left to hypothesize whether
class is synonymous to class name
(this is suggested by e.g. writing C <: D
for the subtype relation between C and D)
or
perhaps to class declaration,
or
whether a class is meant to be a pair (x,y)
with x being a class name and y a class declaration
(no such statement appears in the text).
Overview
The objective of this document is to provide a clean abstract description
of Featherweight Java.
The description should focus on general foundations of OOP
and thus avoid specifics of Java or of type systems.
This results in the following characteristics:
There are no syntactic forms in the usual sense of textual strings.
Instead, the syntax is purely abstract.
Expressions are built from atomic entities using
set-theoretic constructs of maps, lists and tuples.
In particular, the Java syntax is dropped.
There are no constructors.
By abandoning Java syntax, constructor declarations became redundant.
Field declarations and method declarations are unordered
(unlike in Java or FJ).
There are no class names.
Classes are defined as abstract entities each of which identifies itself,
without a need of having a syntactic (string-form) identifier.
There is no need to introduce the notion of a class declaration.
There is a clear definition of which entities of the system are objects
and which entities are classes.
The system is described gradually by refinement of families of structures,
FJ_{1}–FJ_{4}.
The notions of objects and classes
as well as the fundamental relations of inheritance and instance-of are
already defined for
FJ_{2} structures which are much simpler
than the final family of FJ_{4} structures.
Sample structure
The diagram below shows a sample
FJ_{2} structure
–
a Featherweight Java structure without methods.
The definitory part is delimited by brown dashed line.
It is constituted by the set C of 8 classes
r,
A, B, S, P, Q, X and Y,
together with
the inheritance relation between them (indicated by green links)
and
instance variable declarations (the fields) which are given by assigning each
class x a possibly empty dictionary x.ѥ_{ɵ}() of classes.
The dictionaries are denoted
(ⅰ)–(ⅴ)
with (ⅰ) being the empty dictionary mapped to
by four classes.
There is also a derived dictionary x.ѥ_{ }()
of inherited instance variable declarations for each class
x, with the difference indicated by dotted black arrows.
(Both P and Q
inherit ('fst',A) from S.)
class X extends Object { X fst; }
class Y extends Object {}
class A extends Object {}
class B extends A {}
class S extends Object { A fst; }
class P extends S { A snd; }
class Q extends S { B snd; }
(ⅰ)=∅=r.ѥ_{ɵ}() =A.ѥ_{ɵ}()
=B.ѥ_{ɵ}()
=Y.ѥ_{ɵ}() (ⅱ)= {('fst', A)}=S.ѥ_{ɵ}() (ⅲ)= {('snd', A)}=P.ѥ_{ɵ}() (ⅳ)= {('snd', B)}=Q.ѥ_{ɵ}() (ⅴ)= {('fst', X)}O=O_{2}⊃O_{1}
●
O_{1}= {a,b,c,d} where
a = (A,∅),
b = (B,∅),
c = (r,∅),
d = (Y,∅),
●
O_{2}∖O_{1}= {e,f,g,h,i,j,k} where
e = (S,α),
f = (Q,β),
g = (P,β),
h = (P,γ),
i = (P,δ),
j = (Q,γ),
k = (P,ε)
where
α = {('fst',a)},
β = {('fst',a),('snd',b)},
γ = {('fst',b),('snd',b)},
δ = {('fst',b),('snd',a)},
ε = {('fst',a),('snd',a)}
The delimited area (class structure)
uniquely determines
the complementary outside part:
the set O of objects.
The sample structure is so crafted that
there are exactly 11 objects, a to k.
Each object o equals a pair (x,q) where
x is a class (the class of o, pointed to by a blue link)
and q is a dictionary of objects
(pointed to by a black link).
This dictionary is subject to typing constraints given by the x.ѥ_{ }()
dictionary:
q has the same keys as x.ѥ_{ }(), and
if (s,(y,q')) and (s,z) are key-value pairs
from q and x.ѥ_{ }(), respectively, then
y ≤ z.
If we restrict the structure to classes and objects
(that is, we throw away the dictionaries
(ⅰ)–(ⅴ)
and
α–ε together with all links that point to or from them)
then
we obtain (O, C, .class, ≤, r)
which is a standard core structure of a class-based object-oriented
programming language with
(a) single inheritance,
(b) single root class and
(c) classes not being objects.
The .class map
(which is simultaneously the direct instance-of relation)
is formed by the blue links,
the inheritance relation ≤ arises as the reflexive transitive closure
of green links.
Furthermore,
the instance-of relation, ϵ, arises as the composition
(.class) ○ (≤).
Note that the X class has no instances
(cf. the CycList class in
[]).
The P class can be considered as the class
of all pairs of instances of A.
Since A has exactly one strict descendant
(the B class), P has no strict descendants,
and both A and B have exactly one instance
(since they provide no field declarations)
it follows that there are exactly 4 instances of P,
corresponding to pairs from
{A,B} × {A,B}.
Similarly, the 2 instances of Q corespond to
pairs from
{A,B} × {B}.
Preliminaries
We will follow the notational conventions established in
[]
and other author's documents.
In addition, we introduce special notation
for finite partial maps and
and ordered finite partial maps.
As a result, there will be four set-theoretic operators
used
for the recursive definition of expressions:
the cartesian product operator × for building tuples,
the unary operator ^{∗} for building lists,
and the binary operators ⤼ and ⥤
for building dictionaries and ordered dictionaries, respectively.
By a dictionary we mean a finite map, that is,
a finite
functional relation.
The word dictionary is used to suggest that the elements
from the domain are considered to be names or keys.
We consider a (finite) list over X to be
a (finite) map from a subset I of the set ℕ of natural numbers
to X such that
i ≤ j ∈ I implies i ∈ I.
(That is, for finite lists,
I = {0, 1, …, n-1} for a natural n,
called the length of the list.)
By an ordered dictionary we mean
a pair (k,ℓ)
such that k and ℓ are finite lists of the same length
and, in addition, k is injective
(k[i] ≠ k[j] for i ≠ j).
That is, (k,ℓ) can be equivalently specified as
an (q,≤) where
q = k^{−1}○ ℓ is a dictionary
and
≤ is the linear order between keys of q
given by
k[i] ≤ k[j] ↔ i ≤ j.
The above definitions can be more formally summarized as follows.
For sets X, Y and Σ,
X × Y
is the set of all (ordered) pairs (x,y)
such that x ∈ X and y ∈ Y,
Σ ⤼ X
is the set of all dictionaries with keys from Σ and
values from X,
(i.e. Σ ⤼ X is the set of
all finite partial maps from Σ to X)
X^{∗}
is the set of all finite lists of elements from X,
(i.e. X^{∗} is the set of
all finite partial maps ℓ from ℕ to X
such that dom(ℓ) is a down-set in (ℕ, ≤))
Σ ⥤ X
is the set of all ordered dictionaries with keys from Σ and
values from X.
(I.e. Σ ⥤ X is the set of
all pairs (k,ℓ) from Σ^{∗}× X^{∗}
such that dom(k) =dom(ℓ) and k^{−1} is a dictionary.)
As already applied above, we let dom(R) denote the domain
of a (possibly functional) relation R,
i.e. dom(R) equals the set of all x such that
(x,y) ∈ R
for some y.
Similarly, the range of R is denoted
rng(R) and equals dom(R^{−1}) where
R^{−1} is the inverse of R.
The relational composition operator ○ is interpreted left-to-right,
i.e.
for relations R, S,
the composition
R ○ S consists of all pairs (x,z) such that
(x,y) ∈ R and (y,z) ∈ S for some y.
We use the ↷ operator for building general (not necessarily finite)
partial maps between sets,
i.e. X ↷ Y equals the set of all functional relations between
X and Y.
The straight arrow → then indicates a total map,
i.e.
X → Y equals the set of all functional relations between
X and Y.
FJ_{1}:
A finite tree of classes
By an FJ_{1} structure
we mean a single-sorted structure
S= (C, ≤, r)
where
C is a set of classes,
≤
is the inheritance relation between classes,
r
is the inheritance root, a distinguished class.
We might also use the term root class for r
as an equivalent alternative.
The structure is subject to axioms in the box on the right which just say
that
S is a finite tree (an inheritance tree).
Let us denote .sc the reflexive
transitive reduction
of ≤
and call it the superclass map.
Obviously, .sc is a map from
C∖ {r} to C.
If x is a class different from r then
x.sc is the superclass ofx or also
the (inheritance) parent of x.
For a natural i we denote .sc(i) the
i-th composition of .sc with itself.
(We let .sc(0) be the identity on C.)
FJ_{2}:
Fields (instance variable declarations)
Domains →C
Σ_{𝕚}
C
owner
name
bound
x
s
y
An FJ_{2} structure
is a two-sorted structure
(C, Σ_{𝕚}, ≤, r, .ѥ_{ɵ}())
where
(C, ≤, r) is an FJ_{1} structure
(an inheritance tree between classes),
Σ_{𝕚} is the set of instance variable names
(or also field names or just names),
.ѥ_{ɵ}() is a
partial function from C×Σ_{𝕚} to C.
The last constituent can be regarded as a relational database table
with three columns according to the diagram above right.
Underline in
owner and
name
indicates a
primary key.
Pairs (x,s) from the domain of .ѥ_{ɵ}()
are called own fields.
(The ɵ subscript refers to the own adjective.)
If (x,s) is an own field
then x.ѥ_{ɵ}(s) refers to the value of
.ѥ_{ɵ}() at (x,s),
which is a class
called the bound of (x,s).
The structure is subject to the following axioms:
Own fields are a special case of fields
which are by definition all pairs (x,s) from
C×Σ_{𝕚} such that
(a,s) is an own field for some a ≥ x.
Accordingly,
we extend the own-field bound map .ѥ_{ɵ}()
to the field bound map .ѥ_{ }() defined for all fields by
x.ѥ_{ }(s) = y↔a.ѥ_{ɵ}(s) = y
for some a ≥ x.
In particular, .ѥ_{ }() is a partial map from
C×Σ_{𝕚} to C just like .ѥ_{ɵ}().
By
currying,
.ѥ_{ }() and .ѥ_{ɵ}() can be regarded as
total maps from
the set C of classes
to
the set Σ_{𝕚}⤼C of dictionaries of classes.
Triples (x,s,y) such that
x.ѥ_{ɵ}(s) = y (i.e. (x,s,y) is a row of the above table)
are instance variable declarations.
An instance variable declaration (x,s,y) should be roughly
read as the x class declares an instance variable s whose
class is y or a descendant of y.
This is equivalent to say that
the x class has an own-field (x,s) whose bound is y.
Triples (x,s,y) such that
x.ѥ_{ }(s) = y
are instance variable provisions.
By definition, (x,s,y) is an instance variable provision
iff (a,s,y) is an instance variable declaration for
some (non-strict) ancestor a of x.
Axiom (FJ_{2}~3)
asserts a's uniqueness.
Semantically,
an instance variable provision (x,s,y) is meant to
impose the following constraint:
Each instance of x has an s-named instance variable
whose value is an instance of y.
Terminology used in this statement is defined below.
Objects
Given an FJ_{2} structure
S= (C, Σ_{𝕚}, ≤, r, .ѥ_{ɵ}()),
the set O of objects of S is
defined
cumulatively via stages
O_{0}, O_{1}, …
as follows:
O_{0}=∅.
For every natural i, the (i+1)-th stage
O_{i+1} equals the set of all pairs (x,d)
from C× (Σ_{𝕚}⤼O_{i})
(i.e. x is a class
and d is a dictionary with keys from
Σ_{𝕚} and values from O_{i})
such that
(ⅰ)
d(s) is defined ↔
x.ѥ_{ }(s) is defined,
(ⅱ)
if d(s) = (y,_) then
y ≤ x.ѥ_{ }(s).
O=∪ {O_{i}| i < ω}.
(The set O equals the union of all finite stages.)
Conditions (ⅰ) and
(ⅱ) assert
well-typedness of objects.
Using the terminology introduced later,
the conditions can be formulated as follows.
For every object o and every instance variable name s,
(ⅰ)
o has an s-named instance variable
↔
the class of o has an s-named instance variable provision
(ⅱ)
if o has an s-named instance variable
whose value is o' (another object)
and x and y
are the respective classes of o and o' then
y ≤ x.ѥ_{ }(s)
(i.e. y is subject to the upper bound constraint provided by
the s-named instance variable provision of x).
We also define the set Θ of pre-objects
(corresponding to values in
[])
as
Θ=∪ {Θ_{i}| i < ω}
where Θ_{i} are defined like O_{i} except
that
(ⅰ) and
(ⅱ) are dropped.
Equivalently,
Θ is the smallest set X such that
X =C× (Σ_{𝕚}⤼ X).
Given this, objects are exactly the well-typed pre-objects, i.e.
O is the set of all pre-objects for which
(ⅰ) and
(ⅱ) are recursively satisfied.
Further observations:
(FJ_{2}~1)
can be equivalently replaced by any of the following:
(r,∅) is an object (necessarily from O_{1}).
O≠∅.
O_{1}= { (x,∅) | x.ѥ_{ }() =∅ }.
(The first stage equals
X × {∅} where
X is the set of all classes without instance variable provision.)
Even for (arbitrarily many) multiple classes
it is possible that
(r,∅) is the only object.
(Consider the case when all non-root classes x have
at least one instance variable declaration of the form (x,s,x).)
The set O can be infinite.
(As a minimum example,
consider the case where there is exactly one non-root class x
and (x,s,r) is the only instance variable declaration.
Define by induction an infinite sequence
o_{0}, o_{1}, … of objects:
o_{0}= (r,∅),
o_{i+1}= (x,{(s,o_{i})}) for every natural i.
Then for every natural i,
O_{i+1}= {o_{i}}.)
Seeing objects abstractly
By establishing notation for projections of objects to their
coordinates,
objects can be viewed as abstract entities.
For an object o = (c,d) we
refer to c by o.class and call it the class of o.
This defines the class map, .class, which is a total map
from O to C.
The instance-of
relation is denoted ϵ and defined between objects and
classes as the composition
(.class) ○ (≤), i.e.
for every object o and every class c,
o ϵ c↔o.class ≤ c.
The .class map, as an obvious subrelation of ϵ,
is called direct instance-of.
As for the second coordinate,
for an object o = (c,d),
the object-valued dictionary d is referred to by
o.ю().
By
uncurrying,
this defines a partial map .ю() from
O×Σ_{𝕚} to O
called instance variable valuation.
That is, .ю() is such that for every object (c,d)
and every name s,
(c,d).ю(s) and d(s) are either both undefined
or both defined and equal.
Pairs (o,s) from the domain of .ю() are called
instance variables.
If p = (o,s) is an instance variable then
s is the name ofp and
o.ю(s) is the value ofp.
Moreover, p is said to be an instance variable ofo.
Well-typedness of objects can be (once again) formulated as follows.
For every object x and every instance variable name s,
(ⅰ)
x.ю(s) is defined
↔x.class.ѥ_{ }(s) is defined,
(ⅱ)
x.ю(s) ϵ x.class.ѥ_{ }(s).
FJ_{3}:
Expressions and unnamed methods
An FJ_{3} structure
is a 4-sorted structure
(C, Σ_{𝕚}, Σ_{𝕞}, E_{ʋ}, ≤, r, .ѥ_{ɵ}(), ʦ)
where
(C, Σ_{𝕚}, ≤, r, .ѥ_{ɵ}())
is an FJ_{2} structure,
Σ_{𝕞} is the set of method names,
E_{ʋ} is the set of local variable names
(or just local variables), and
ʦ is a distinguished local variable name,
corresponding to the Java's this keyword.
The structure is subject to no additional axioms.
Expressions
Given an FJ_{3} structure
S= (C, Σ_{𝕚}, …),
the set E of (evaluation) expressions of S is
the smallest set that equals the (necessarily disjoint) union
of the following five sets.
(Terms shown in parentheses are used for the elements of the sets.
The term field access is a shorthand for instance variable access.)
(a)
E_{ʋ}
(local variable)
(b)
E×Σ_{𝕚}
(field access)
(c)
E×Σ_{𝕞}×E^{∗}
(method invocation)
(d)
C× (Σ_{𝕚}⤼E)
(object creature)
(e)
C×E
(cast)
The sequence E_{0}, E_{1}, … of stages of
E is defined recursively by
E_{0}=∅ and
for each natural i,
the set E_{i+1} being equal to the (necessarily disjoint) union of
sets prescribed by (a)–(e) with E replaced by E_{i}.
Observe that every (pre-)object is an object creature.
(This sentence also explains why we prefer the term object creature
over object creation.)
Every local variable is an expression (from the first stage E_{1})
but no element of any of the remaining 3 definitory sorts
C, Σ_{𝕚} and Σ_{𝕞}
is an expression.
Let e, f be expressions.
Then e is said to be a child expression of f,
written
e ⥽ f,
if f ∉E_{ʋ}
and for some cartesian coordinate x of f
either e equals x or e is in the range of x,
the latter applied if x is a list or a dictionary.
(An expression f has 2 / 3 / 2 / 2 coordinates
according to which of the sets (b) / (c) / (d) / (e) it belongs.)
The subexpression relation is defined
as the reflexive transitive closure of ⥽
and denoted ⥽_{⁎}.
Obviously, (E, ⥽_{⁎}) is a partial order.
The set of all child expressions (resp. subexpressions)
of an expression x is denoted by x.⥾
(resp. x.⥾_{⁎}).
Observation:
An expression x is a pre-object
iff
every subexpression of x is an object creature.
Replacement
Let e be an expression and let q be a dictionary
from E_{ʋ}⤼E
(that is, q maps some local variables to expressions).
The replacement of the q's keys in e by q's values
is an expression g denoted e.repl(q)
and defined recursively as follows:
(a)
g = q(e) if q(e) is defined, g = e otherwise
(case e ∈E_{ʋ})
(b)
g = (x.repl(q), s)
(case e ∈E×Σ_{𝕚},
e = (x,s))
(c)
g = (x.repl(q), s, ℓ ○ .repl(q))
(case e ∈E×Σ_{𝕞}×E^{∗},
e = (x,s,ℓ))
(d)
g = (c, d ○ .repl(q))
(case e ∈C× (Σ_{𝕚}⤼E),
e = (c,d))
(e)
g = (c, x.repl(q))
(case e ∈C×E,
e = (c,x))
Typing context
By a typing context we mean
a (possibly empty) dictionary from E_{ʋ}⤼C.
That is, q is a typing context if
it is a function that maps a finite set of local variables to classes.
Methods
The set Π of (unnamed) methods
is defined as
the set of all 4-tuples m = (k,ℓ,c,e) such that
ʦ is not in (the range of) k
(this does not appear in method parameters),
(2)
every local variable x from e.⥾_{⁎} either equals ʦ or
is in (the range of) k.
(Therefore, x is bound in m).
Observe that
k^{−1}○ ℓ is a typing context
and so is (by (1)) (k^{−1}○ ℓ) ∪ {(ʦ,a)}
for any class a.
Pairs (s,m) from Σ_{𝕞}×Π
(i.e. s is a method name and m is an unnamed method)
are called
named methods.
A method dictionary is a dictionary from Σ_{𝕞}⤼Π,
i.e. it is a set of named methods with unique names.
FJ_{4}:
Method declarations
C
Σ_{𝕞}
Π
owner
name
method
a
s
m
An FJ_{4} structure
is an
FJ_{3} structure
equipped with
a mapping of classes to method dictionaries.
That is, there is one additional definitory constituent, .m_{ɵ}(),
called own method map,
such that
.m_{ɵ}() is a
partial function from C×Σ_{𝕚} to Π.
Similarly as with .ѥ_{ɵ}(),
if (a,s) is in the domain of .m_{ɵ}()
then a.m_{ɵ}(s) refers to the value of
.m_{ɵ}() at (a,s).
We call a triple (a,s,m) such that
a.m_{ɵ}(s) = m
a method declaration
(i.e. (a,s,m) is a row of the table on the right).
There is an induced partial order relation (.m_{ɵ}(), ≤)
of overriding between method declarations given by
(a,s,m) ≤ (a',s',m')↔a ≤ a' and s = s'.
The structure is subject to the following axioms:
The .type() map used in
(FJ_{4}~4)
is introduced below.
To this end we refer to the (more general) family of structures that
arise by removing (FJ_{4}~3)
and (FJ_{4}~4)
as to
pre-FJ_{4} structures.
Method provision
Similarly as with
instance variable declarations,
method declarations are inherited.
That is,
given a pre-FJ_{4} structure S= (C, …),
there is a derived partial function .m_{ʜ}()
from C×Σ_{𝕚} to Π,
called inherited method map
(or providing method map) and
defined as follows.
For every class x, every method name s and every unnamed method m,
x.m_{ʜ}(s) = m↔a.m_{ɵ}(s) = m
and a is the least ancestor of x such that
a.m_{ɵ}(s) is defined.
The corresponding relation between
classes and named methods is called method provision.
In addition, the same term can be used for a triple (x,s,m)
such that
x.m_{ʜ}(s) = m.
The type map
Given a pre-FJ_{4} structure S= (C, …),
the (static) type map, denoted .type(),
is a partial map from E× (E_{ʋ}⤼C)
to C defined recursively as follows.
Let e be an expression and q be a
typing context.
Then
e.type(q) = t
(the type of e under the q context is defined and equals the
t class)
if and only if the following conditions are recursively satisfied for each case
(a)–(e).
(a)
e is a local variable
e ∈E_{ʋ}
q(e) = t
(b)
e is a field access
e = (x,s)
e ∈E×Σ_{𝕚}
x.type(q).ѥ_{ }(s) = t
(c)
e is a method invocation
e = (x,s,ℓ)
e ∈E×Σ_{𝕞}×E^{∗}
x.type(q).m_{ʜ}(s) = (_,ℓ',t,_)
and
dom(ℓ') =dom(ℓ)
and
ℓ[i].type(q) ≤ ℓ'[i] for each i ∈dom(ℓ)
(d)
e is an object creature
e = (c,d)
e ∈C× (Σ_{𝕚}⤼E)
c = t
and
dom(c.ѥ_{ }()) =dom(d)
and
d(s).type(q) ≤ c.ѥ_{ }(s) for each s ∈dom(d)
(e)
e is a cast
e = (c,x)
e ∈C×E
c = t and x.type(q) is defined
(If c ≥ x.type(q) then e is called an upcast,
else if c < x.type(q) then e is a downcast
else e is a stupid cast,
all cases w.r.t. typing context q.)
If e.type(q) is defined then we also say that
e is well-typed under the context q.
If q is empty then e is just said to be well-typed.
We also abbreviate .type(∅)
to .type.
(Therefore, .type
is a partial function from the set E of expressions
to the set C of classes.)
Observations:
Every object is well-typed.
Moreover, (.class) ⊂ (.type), i.e.
for every object x,
x.type = x.class.
Objects are exactly the well-typed pre-objects.
Expression evaluation
Given a pre-FJ_{4} structure S= (C, …),
the one-step evaluation is a relation between expressions
denoted ⇽ (with the inverse denoted by ⇾)
and defined recursively as follows.
Let e, f be expressions. Then
e ⇾ f
(e evaluates (reduces) in one-step to f)
if one of the following conditions (b)–(e) is satisfied:
(b)
e is a field access
e = (x,s)
e ∈E×Σ_{𝕚}
f = (y,s) for some y such that x ⇾ y
or f = d(s) where d is a dictionary such that
x = (_,d) is an object creature and d(s) is defined
(c)
e is a method invocation
e = (x,s,ℓ)
e ∈E×Σ_{𝕞}×E^{∗}
f = (y,s,ℓ) for some y such that x ⇾ y
or f = (x,s,ℓ') where
ℓ ∖ ℓ' = {(i,y)}
and
ℓ' ∖ ℓ = {(i,z)}
for some i,y,z such that y ⇾ z
or f = y.repl(z)
where y and z are such that the following are satisfied:
x = (c,_) is an object creature,
c.m_{ʜ}(s) = (k,ℓ',_,y)
(the c class provides an s-named method (k,ℓ',_,y))
dom(ℓ) =dom(ℓ'),
z = k^{−1}○ ℓ ∪ {(ʦ,x)}
(z is the replacement map;
in particular, ʦ is to be replaced by x).
(d)
e is an object creature
e = (c,d)
e ∈C× (Σ_{𝕚}⤼E)
f = (x,d') where
d ∖ d' = {(s,y)}
and
d' ∖ d = {(s,z)}
for some s,y,z such that y ⇾ z
(e)
e is a cast
e = (c,x)
e ∈C×E
f = (c,y) for some y such that x ⇾ y
or f = x and
x = (b,_) is an object creature such that b ≤ c
Expressions that are minimal in (E, ⇽)
(i.e. they cannot be further reduced)
are said to be in normal form.
References
Davide Ancona, Elena Zucca,
Corecursive Featherweight Java,
Proceedings of the 14th Workshop on Formal Techniques for Java-like Programs,
ACM,
2012
Sven Apel, Christian Kästner, Christian Lengauer,
Feature Featherweight Java: A Calculus for Feature-Oriented Programming and Stepwise Refinement,
Proceedings of the 7th international conference on Generative programming and component engineering,
ACM,
2008/span>
Lorenzo Bettini, Sara Capecchi, Betti Venneri,
Featherweight Java with multi-methods,
Proceedings of the 5th international symposium on Principles and practice of programming in Java,
ACM,
2007
Lorenzo Bettini, Ferruccio Damiani, Ina Schaefer,
IFJ: a Minimal Imperative Variant of FJ,
Technical Report 133/2010,
Dipartimento di Informatica, Università di Torino,
2010http://www.di.unito.it/~damiani/papers/tr-133-2010.pdf
Gavin Bierman, Matthew Parkinson, Andrew Pitts,
MJ: An imperative core calculus for Java and Java with effects,
Technical Report 563,
Cambridge University Computer Laboratory,
2003
Atsushi Igarashi, Benjamin C. Pierce, Philip Wadler,
Featherweight Java: a minimal core calculus for Java and GJ,
ACM SIGPLAN Notices. Vol. 34. No. 10,
ACM,
1999
Atsushi Igarashi, Benjamin C. Pierce, Philip Wadler,
Featherweight Java: a minimal core calculus for Java and GJ,
ACM Transactions on Programming Languages and Systems (TOPLAS),
2001http://www.cis.upenn.edu/~bcpierce/papers/fj-toplas.pdf
Atsushi Igarashi,
A featherweight approach to FOOL,
ECOOP 2011–Object-Oriented Programming,
Springer Berlin Heidelberg,
2011
Luigi Liquori, Arnaud Spiwack,
FeatherTrait: a modest extension of Featherweight Java,
ACM Transactions on Programming Languages and Systems (TOPLAS),
2008