This project originated from the idea of extending Java,
based on the OO paradigm, with higher order mechanisms to enhance its
expressivity and code reusability, in order to facilitate writing programs
which are correct, well suited to the applications and can be easily adapted
for a different use.
In 2004, \cite {bellia2004} through a case study we compare
the expressivity of five different programs, all based on the OO programming
paradigm but using also higher order mechanisms (mainly in the form of methods
with higher order functionalities), all solving the same problem. Three
programs are written in Java, one is written in J++ and the last one is written
in Pizza. As far as the higher
order mechanisms are concerned, the first two programs in Java use reflection,
the third one uses anonymous classes, the J++ program uses delegates and the
Pizza program uses function abstractions (closures).
The result of the comparison led to
identify three possible mechanisms to add to Java to extend it with higher
order: higher order methods, method extraction and closures.
In \cite{bellia2005} the
integration of such mechanisms in an OO paradigm is studied, through the
extension of the $\zeta$-calcolo \cite{abadi96}. The
new calculus $\zeta_x$-calculus provides for such
mechanisms the reduction semantics and the typing rules and prove calculus
confluence, subtyping, subtyping
controvariance, subject reductions hence type
soundness.
If the problem of the integration of HO mechanisms in an OO
language can be considered positively solved, the problem of how this can be
accomplished in Java is still open. As a matter of fact, the language Java has
an implementation based on a mixture of compilation and interpretation. At the
top level of the implementation process is a compiler that translates Java
programs into Java bytecodes for the Java virtual
machine, JVM. The machine is a collection of structures for processing bytecodes and has been designed to be defined once and to
have as many different implementations as the different platforms that run Java
programs.
This implementation ensures retargetability
of Java compilers and high portability of the Java object code. In extending
Java with new mechanisms is good practice to plan to preserve such appealing
features of its implementation.
In Bellia2007 we began to study the design of
HO mechanisms especially tailored for Java and its peculiar implementation,
defining the structure of m_parameters as a form of
higher order methods for Java. Bellia2007, Bellia2008
provide the
syntactic extensions to Java grammar to pass methods as parameters to other
methods. A formal semantics is also defined and examples that show the use of
the mechanism are shown. The expressivity is discussed by
comparing programs that use such a mechanism with programs that compute in an
almost equivalent way but are written in ordinary Java.
· One of the most
remarkable aspects of our study is the formal semantics which
is defined in the form of a translation semantics. This kind of semantics maps
programs of the extended language into programs of ordinary Java and has three main benefits.
· It defines the
meanings of the new constructs in terms of the well known constructs of Java,
without the introduction of the semantic structures needed in the definition of both
denotational and operational semantics.
· The translation
semantics helps in evaluating the expressivity power of the new constructs by
allowing an immediate comparison between a program that uses the new constructs
and its translation in a Java program.
· It allows an
implementation of the execution support of the extended language completely retargetable on all the compilers developed for Java.
This approach in the design of HO
extensions for Java is further discussed in \cite{bellia2008a}
where the translation semantics of Java 1.4, extended with {\em m-parameters}, is defined and used to form the kernel
\cite{bellia2008b} of a pre-processor for Java compilers.
The drawbacks of m\_parameters are the
impossibility to
·
statically check type
correctness and
·
pass overloaded
methods.
Such drawbacks are both overcome in Bellia2009a, Bellia2009b
where mc\_parameters are defined.
Mc\_parameters have a type which specifies also the
class hierarchy in which the passed method must be defined, allowing a static
type checking and overloading static resolution. To maintain retargetability and portability of the implementation of
the resulting language, the translation semantics of mc\_parameters is defined
resorting to the use of anonymous and inner classes, involved in the Java
methodology known as callback \cite{horstmann2007}.
In 2006, the Java community started a
debate about the opportunity to introduce function abstractions, improperly
called closures, in the language. The proposals resulting from such a debate
are contained in \cite{Bracha06,Cole06,Lee06} and more
recently
\cite{Bracha08,Cole08,Reinhold09}.
In such proposals Java is extended with different closure forms and other mechanisms with the aim
to allow a better use of closures
and integration in the language (closure conversion, shared variables, loop
abstraction). As a matter of fact, our paper \cite{bellia2005}
about $\zeta_x$-calculus already contained the definition of a form of closures. In Bellia2009c we
apply the translation semantics approach to the extension of Java with a form
of closures which contains (takes in) many of the
features of the above cited papers. As for higher order methods the approach
guarantees the goals of portability and retargetability
but is not well suited to the study different and alternative definitions of closures and
related mechanisms. For this reason we resorted to a minimal core calculus,
more meaningful and suited to Java features, to extend it with closures. Such
a calculus defined in Bellia2010a and
Bellia2011 is obtained extending Featherweight Java
\cite{Igarashi01}.
The implementation of the language
extended with m_parameters can be downloaded here
A dabate is currently
under way on whether closure should be added to Java or not. Some links are:
1.
http://javac.info/closures-v06a.html
2.
http://www.jroller.com/scolebourne/entry/closures_in_jdk_7
3.
http://www.infoq.com/news/2009/11/reinhold_closures_update
4.
http://blogs.sun.com/mr/entry/plan_b
A survey on Java Omega is in:
Marco Bellia and M. Eugenia Occhiuto, Java$\Omega$: Higher
Order Programming in Java. in Java in Academia and in Research, IConcept
Press, To appear
\begin {abstract}
The paper considers the problems and the solutions that
are concerned with the extension of Java with Higher Order mechanisms.
We start from the motivations namely the code reusability and the code expressivity.
Through the description of the Java$\Omega$
project we discuss the design of constructs for Higher Order methods, methods as parameters and for closures that can be integrated
in Java and whose implementation must preserve re-targetability and portability of the Java compilers and of the JVM. We give the
formal definition of such constructs, including the formalization of a translation semantics which can be converted into a source-to-
source translation
and implemented as one-pass preprocessor. Examples of the use of the formalized
constructs are included.
\end {abstract}
Marco Bellia and M. Eugenia Occhiuto,
Java$\Omega$: Higher Order Programming in Java -- The Technical Complements.
\begin {abstract}
The paper contains the technical complements, of a paper that describes the extensions of Java 1.5 with Higher Order mechanisms.
It contains the complete tables of (i) The translation semantics of a form of closure for Java; (ii) The translation semantics of H.O.
methods with mc\_parameters as arguments; (iii) The translation semantics of Java extended with the above mechanisms put together;
(iv) Theorems and lemmas and proofs of all the the properties of the mechanisms and of the semantics discussed. The material
includes several technicalities and considerations that relate to the above mentioned results. In particular, (a.1) An unambiguous
grammar for Java 1.5; (a.2) A formalism used to define a translation semantics; (a.3) A semi-formal description of the callback
methodology in Java.
\end {abstract}
Recent papers are:
Marco
Bellia and M. Eugenia Occhiuto, Proving Type Safety for Java Simple Closures,
CS\&P2010, vol.1, 61-72, Helenenau, Sept. 27-29, 2010 Marco
Bellia and M. Eugenia Occhiuto, Proving Translation and Reduction Semantics
Equivalent for Java Simple Closures, Extended Version \Lname\ is a minimal core calculus that extends Featherweight (generic)
Java, \FGJ, with lambda expressions. It has been used to study properties of
Simple Closure in Java, including type safety and the abstraction property.
Its formalization is based on a reduction semantics and a typing system that
extend those of \FGJ. ${\cal F}$ is a source-to-source, translation rule system
from Java 1.5 extended with lambda expressions back to ordinary Java 1.5. It
has been introduced to study implementation features of closures in Java, including
assignment of non local variables and relations with anonymous class objects.
In this paper we prove that the two semantics commute. \end {abstract}
begin {abstract}
In the last years, the Java community has been arguing about adding closures
to Java in order to improve expressivity. The debate has not yet terminated but
all proposals seem to converge towards a notion of Simple Closures which contain
only essential features. This paper addresses the problem of defining a rigorous
semantics for Simple Closures. The technique adopted is well known and has already
been used to prove interesting properties of the language. A minimal calculus
is defined: Featherweight Java extended with Simple Closures. Syntax and semantics
of such calculus are defined and type safety and backward compatibility are proved.
\end {abstract}
Marco Bellia and M. Eugenia Occhiuto, Properties of Java Simple Closures. Fundamenta
Informatica , To
appear
\begin {abstract}
In the last years, the Java community has been arguing about adding closures
to Java in order to improve expressivity. The debate has not yet terminated but
all proposals seem to converge towards a notion of Simple Closures which contain
only the essential features of anonymous functions. This paper addresses the
problem of defining a rigorous semantics for Simple Closures. The technique adopted
is well known and has already been used to prove interesting properties of other
extensions of Java. A minimal calculus is defined: Featherweight Java extended
with Simple Closures. Syntax and semantics of such a calculus are defined and
type safety, backward compatibility, and the abstraction property are proved.
\end {abstract}
\begin {abstract}
by M.E.Occhiuto