Admin CliCours
Java A minimal core calculus for Java and GJ, tutoriel extend Featherweight Java document pdf.
INTRODUCTION
“Inside every large language is a small language struggling to get out…” T. Hoare Formal modeling can offer a significant boost to the design of complex real-world artifacts such as programming languages. A formal model may be used to describe some aspect of a design precisely, to state and prove its properties, and to direct attention to issues that might otherwise be overlooked. In formulating a model, however, there is a tension between completeness and compactness:
The more aspects the model addresses at the same time, the more unwieldy it becomes. Often it is sensible to choose a model that is less complete but more compact, offering maximum insight for minimum investment. This strategy may be seen in a flurry of recent papers on the formal properties of Java,which omit advanced features such as concurrency and reflection and concentrate on fragments of the full language to which well-understood theory can be applied.
We propose Featherweight Java, or FJ, as a new contender for aminimalcore calculus for modeling Java’s type system. The design of FJ favors compactness over completeness almost obsessively, having just five forms of expression: object creation, method invocation, field access, casting, and variables. Its syntax, typing rules, and operational semantics fit comfortably on a few pages. Indeed,our aim has been to omit as many features as possible—even assignmentwhile retaining the core features of Java typing. There is a direct correspondence between FJ and a purely functional core of Java, in the sense that every FJ program is literally an executable Java program.
FEATHERWEIGHT JAVA
In FJ, a program consists of a collection of class definitions plus an expression to be evaluated. (This expression corresponds to the body of themainmethod in full Java.) Here are some typical class definitions in FJ.
class A extends Objectf
A()f super();)
)
class B extends Objectf
B()f super();)
)
class Pair extends Objectf
Object fst;
Object snd;
Pair(Object fst, Object snd)f
super(); this.fst=fst; this.snd=snd;
)
Pair setfst(Object newfst)f
return new Pair(newfst, this.snd);
)
)
For the sake of syntactic regularity, we always (1) include the supertype (even when it isObject); (2) write out the constructor (even for the trivial classesA andB); and (3) write the receiver for a field access (as inthis.snd) or a method invocation, even when the receiver isthis. Constructors always take the same stylized form: there is one parameter for each field, with the same name as the field; thesuperconstructor is invoked on the fields of the supertype; and the remaining fields are initialized to the corresponding parameters. In this example the supertype is alwaysObject, which has no fields, so the invocations ofsuperhave no arguments. Constructors are the only place wheresuperor=appears in an FJ program. Since FJ provides no side-effecting operations, a method body always consists ofreturnfollowed by an expression, as in the body ofsetfst().
Syntax
The abstract syntax of FJ class declarations, constructor declarations, method declarations, and expressions is given at the top of Figure 1. The metavariables A,B,C,D, andErange over class names;fandgrange over field names;mranges over method names;xranges over variables;danderange over expressions; Lranges over class declarations; Kranges over constructor declarations; andM ranges over method declarations. We assume that the set of variables includes the special variablethis, which cannot be used as the name of an argument to a method. (As we will see later, the restriction is imposed by the typing rules).
Instead, it is considered to be implicitly bound in every method declaration.The evaluation rule for method invocation will have the job of substituting an appropriate object forthis, in addition to substituting the argument values for the parameters. Note that since we treatthisin method bodies as an ordinary variable, no special syntax for it is required.
……..
Si le lien ne fonctionne pas correctement, veuillez nous contacter (mentionner le lien dans votre message)Featherweight Java (830 KO) (Cours PDF)
