| [ << ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |
This section describes how the Universe type system [Dietl-Drossopoulou-Mueller07] [Dietl-Mueller05] [Dietl-Mueller-Schregenberger-08] [Mueller-Poetzsch-Heffter01a] is realized in JML and the impact it has on JML specifications. The Universe type system is a lightweight ownership type system that hierarchically structures the object store and confines the possible effects of expressions.
The syntax for the Universe type system consists of three ownership modifiers.
ownership-modifiers ::= ownership-modifier [ ownership-modifier ] ownership-modifier ::= |
Depending on the options selected, one can use either form of the modifiers, with or without the backslash, in annotations. The forms without the backslashes are the only ones that can be used in Java code, and when they are enabled, they are treated as new reserved words in both JML annotations and in Java code.
Currently the Universe type checking and the
reserved-ownership-modifier syntax are not enabled by default in
JML, but is only available when various options are used in the tools.
It can also be used with different levels of checking. If the
--universesx no option is used, only the ownership-modifiers
\rep, \peer, and \readonly are available.
To enable just parsing of the full syntax, one can use the
--universesx parse option; in this case, all of the syntax is
parsed, and rep, peer, and readonly are treated as
reserved words. However, with this option, none of the checking
described below is done.
To enable checking, but without reserving the keywords rep,
peer, and readonly,
one uses the --universesx check option.
With this option, only the ownership-modifiers
\rep, \peer, and \readonly are available.
This allows the use of ownership modifiers in specifications, but not
in Java code.
Various other options control the generation of runtime checks and the storage of ownership modifiers in the created class files. See [Dietl-Mueller-Schregenberger08] for a complete list of the different supported compiler options.
One can also enable checking, all of the syntax, and default options
by using the --universesx full option. An equivalent option is
--universes (synonym -e). This parses and type checks all
the ownership-modifiers, not only in specifications, but also in
Java code.
For a simple reference type, one can use only one ownership-modifier where ownership-modifiers appears in the grammar. The only case where two ownership-modifiers can be used is for array types as described below.
Note that in [Dietl-Drossopoulou-Mueller07] the Universe type system is
extended to type genericity as found in Java 5. The JML tools support
Generic Universe Types and also recognize the any modifier as
synonym for readonly.
As the rest of this report is about non-generic Java, we refer to
[Dietl-Drossopoulou-Mueller07] [Dietl-Mueller-Schregenberger08]
for details.
In the sections below we just use the forms without the backslashes when discussing the semantics of each form.
18.1 Basic Concepts of Universes 18.2 Rep and Peer 18.3 Readonly 18.4 Ownership Modifiers for Array Types 18.5 Default Ownership Modifiers 18.6 Ownership Type Rules 18.7 Casts and Ownership Types
The Universe type system organizes
objects into ownership contexts [Dietl-Mueller05] [Mueller-Poetzsch-Heffter01a].
Each object has 0 or 1 owner objects.
The owner of an object (or the absence of an owner) is determined by the
new expression that creates the object.
Once determined, the owner of an object cannot be changed.
An ownership context is a set of objects with the same owner. There is also a root ownership context, which is the set of all objects that have no owner. Each object thus belongs to exactly one ownership context. The contexts form a hierarchy, with the root ownership context at the top. The owner of an ownership context is not considered to be part of the context it owns, but rather part of that context's parent context.
The Universe type system enforces the "owner-as-modifier" property (see section 1 of [Dietl-Mueller05]). This property says "an object X can be referenced by any other object, but reference chains that do not pass through X's owner must not be used to modify X" (section 1 of [Dietl-Mueller05]). Thus, if one looks at all the references from outside an ownership context into objects within the context, all of these references must be readonly references, with the exception of any references from the context's owner.
This owner-as-modifier property prevents the problem of
representation exposure, in which a reference to X can be
used to modify it, without calling one of the methods of X's owner
[Noble-Vitek-Potter98].
From the perspective of X's owner, X is part of the owner's
representation (and thus a field holding X would be declared with
the rep keyword), and passing out a mutable reference to X
exposes that representation to the rest of the program.
It is difficult to maintain invariants, for example, when the
representation of an object can be directly modified from outside an
object [Mueller02] [Mueller-Poetzsch-Heffter-Leavens06].
The rep and peer annotations are type modifiers
(see section 7.1.2.2 Type-Specs) that specify ownership relative to a receiver object.
The receiver object is defined as follows:
this.
A rep modifier says that the referenced object
is owned by the receiver object.
Thus if myList has a field head of type rep Node,
then myList.head is owned by myList,
because myList is the receiver.
If n is a local variable of type rep Node in an instance
method, then n is owned by this.
(Formal parameters are treated in exactly the same way as local
variables.)
Since the meaning of the rep modifier depends on the existence
of a receiver object, it cannot be used in static
declarations where there is no receiver object.
Hence, a rep modifier cannot be used in a static field
declaration. It also cannot be used in the declaration of a static method or
in its specification. Furthermore, it cannot be used in static
invariants or static history constraints.
A peer
modifier says that the referenced object has the same
owner as the receiver object.
Thus if myNode has a field next of type peer Node,
then myNode.next is owned by the owner of myNode,
because myNode is the receiver.
If n is a local variable of type peer Node in an instance
method, then n is owned by the owner of this.
The peer modifier can be used in all declarations, even in
static declarations.
Currently, a peer modifier in a static field declaration leads
to type unsafety and should therefore not be used. (The tools give a
warning in this situation, and a safe semantics is a subject of
current research.)
The same remark applies to static invariants and static history constraints.
When used in a static method or its specification, peer refers
to the current ownership context.
The current ownership context for a method execution
is defined as follows.
For executions of instance methods the current ownership context is the
one containing the this object.
For executions of static methods, the current ownership context is
determined by the current ownership context of the caller and the
ownership modifier (rep or peer) used in the call as follows:
peer T.m(...),
then m executes in the same ownership context as the code making
the call (and hence in the current ownership context of the caller).
rep T.m(...),
then m executes in the ownership context owned by the caller's
this object; hence this form
of static method call cannot be used in static declarations.
For example, if p is a local variable of type peer Node
in a static method, then p is in the current ownership
context, because there is no receiver object.
See section 18.4 Ownership Modifiers for Array Types, for the usage of these modifiers with array types.
The readonly (or \readonly) modifier does not specify an
ownership context.
Therefore, following the owner-as-modifier property, references
specified with the readonly modifier cannot be used to modify
the referenced object. (Note that this does not guarantee that the
object referenced cannot change, only that it cannot be changed using
this reference.)
A readonly type thus cannot be used as the type of the receiver
expression of: a field update, a call to a non-pure instance method
(See section 7.1.1.3 Pure Methods and Constructors, for more about pure methods.),
or a call to a static method.
In more detail, the cases are:
pure instance method call is guaranteed to
preserve the owner-as-modifier property and is therefore allowed
on a readonly receiver.
pure instance method call might change the receiver or objects reachable from
it and needs to be forbidden.
peer and rep determine
a current ownership context and therefore readonly is forbidden as the receiver type
of a static method call.
An array of reference types always has two ownership modifiers, the
first for the array object itself and the second for the elements.
Both modifiers express ownership relative to the receiver object and both
modifiers can be any of the ownership-modifiers.
For example, the type rep readonly Object[]
says that the array object itself is owned by the receiver object,
but the elements are readonly (and hence may belong to an arbitrary
ownership context).
A peer rep Object[] type says that the array object has the same
owner as the receiver object and that the array elements are owned by the
receiver object.
All array objects in a multidimensional array of a reference type are in the
same context, which is determined by the first ownership modifier.
For example, if an instance field, f, has type rep peer Object[][],
then f and f[3] are both owned by the receiver and
f[3][1] has the same owner as the receiver object.
For one-dimensional arrays of primitive types, the second ownership modifier is
omitted. Primitive types are not owned and do not take an ownership modifier.
A one-dimensional array of primitive types is one object that needs to specify
ownership information.
For example, the type readonly int[] says that the array object
can belong to any context, but cannot be modified through this reference.
A rep int[] references an array object that is owned by the receiver object
and that manages int values.
Multi-dimensional arrays of primitive types have two ownership modifiers, the first for the array object itself and the second for the one-dimensional array at the "lowest" level. All array objects in a multidimensional array are in the same context, which is determined by the first ownership modifier.
For example, if an instance field, g, has type rep peer int[][][],
then:
g references a rep peer int[][][] array object that is
owned by the receiver and the array manages rep peer int[][] references.
g[3] references a rep peer int[][] array object that is
owned by the receiver and the array manages peer int[] references.
g[3][1] references a peer int[] array object that has
the same owner as the receiver and the array manages int
values.
g[3][1][0] is an int value.
Note how the first modifier changes when going from a two- or more-dimensional array of a primitive type to a one-dimensional array of a primitive type.
Also note that java.lang.Object is a supertype of arrays, in
particular also of arrays of primitive type.
A peer int[] can be assigned to a peer Object
reference. Then a rep peer Object[][] type behaves consistently
with the rep peer int[][][] type.
Following the convention in Java, array types support covariant
subtyping that needs runtime checks on write accesses.
For example, a peer rep Object[] is a subtype
of a peer readonly Object[] and when an element is inserted it
needs to be checked that it is owned by the receiver object.
If the ownership-modifiers are omitted in a type-spec,
then a default is used. This default is normally peer, but
there are a few exceptions, described below.
readonly.
Currently, the set of immutable types only includes the Java wrapper
types for primitive types (e.g. java.lang.Integer and
java.lang.Long), java.lang.String, java.lang.Class,
and java.math.BigInteger.
pure
method (but not for the receiver, this) is
readonly.
(Note that this is not the case for pure constructors, however.)
throws clause
of a method header, and in the declaration of a catch clause of
a try statement is readonly [Dietl-Mueller04].
peer.
If the element type is an immutable type, then
the specified modifier is taken to be the array modifier, and
the element modifier defaults to readonly.
For example, the type readonly Object[] is the same as
peer readonly Object[].
A type rep Integer[] is the same as rep readonly Integer[].
Note that if one wants to specify a rep or readonly array
of mutable references, one is thus forced to use two ownership modifiers;
for example, rep readonly Object[].
One-dimensional arrays of primitive types default to peer.
For multi-dimensional arrays of primitive types there is no
distinction between immutable and mutable types and a single
ownership modifier is always taken to be the element modifier.
(T)E,
where T is a reference type that is not an array type,
the default ownership modifier of T is the ownership modifier of
the type of E; in this case, if the type of E is an array
type, this is the ownership modifier of the array object itself, not
the ownership modifier of the elements.
In a cast expression of the form (T)E,
where T is an array type,
the default ownership modifiers of T are the same as the ownership
modifiers of the type of E.
In a cast expression of the form (T)E,
where T is a primitive value type, there is no ownership
modifier attached to T.
instanceof expression of the form E instanceof T,
where T is a reference type that is not an array type,
the default ownership modifier of T is the ownership modifier of
the type of E; in this case, if the type of E is an array
type, this is the ownership modifier of the array object itself, not
the ownership modifier of the elements.
In an instanceof expression of the form E instanceof T,
where T is an array type,
the default ownership modifiers of T are the same as the ownership
modifiers of the type of E.
The defaults for casts and instanceof expressions allow one to only test for Java types, if the ownership modifiers are omitted [Dietl-Mueller05]. See section 18.7 Casts and Ownership Types, for more details on these expressions and their interaction with the Universe type system.
This section explains details of how the Universe type system does type checking.
18.6.1 Ownership Subtyping 18.6.2 Ownership Typing for Expressions
Type checking in the Universe type system uses a notion of subtyping that extends Java's rules to take ownership-modifiers into account (see section 3 of [Dietl-Mueller05]).
If two types have the same ownership modifiers,
then they are subtypes if the underlying Java types are subtypes.
For example, rep Stack is a subtype of rep Object,
because Stack is a subtype of Object.
If S is a reference type, then both peer S and rep
S are subtypes of the type readonly S. Moreover, both
peer om S[] and rep om S[]
are subtypes of the type readonly om S[], where
om is any ownership modifier. For instance, peer peer
Natural[] is a subtype of readonly peer Natural[].
The types peer S and rep S as well as the array
types peer om S[] and rep om
S[] are incomparable--neither is a subtype of the other.
Like Java, the Universe type system has covariant array subtyping:
"two array types
with the same ownership modifier are subtypes if their element types
are subtypes. ...
For instance, rep peer Object[] is a subtype of
rep readonly Object[]
because the element type peer Object is a subtype of the element type
readonly Object" (Section 3 of [Dietl-Mueller05]).
Most of the typing rules for the Universe type system are unchanged from standard Java (and JML) rules. For example, to type check an assignment expression, one checks that the type of the right hand side expression is a subtype of the type of the left hand side.
A small, but important change, is that
the type given in a new expression must be a rep or
peer type. The result type of the new expression has
the given ownership modifier.
The main difference is that the type of field accesses, method parameters, and method results is determined by combining the type of the receiver, R, and the type of the field, the return type of the method, or the type of the formal parameter, F. The Java type is taken from the type F, and the modifier is determined by the following cases (see Section 3 of [Dietl-Mueller05]):
peer types, then the combination is
also a peer type.
For example, if myList has type peer List and the field
head has type peer Node, then myList.head has
type peer Node.
this and F is a rep type,
then the combination is a rep type.
For example, if a Set class has
an instance field elems of type rep List,
then in its instance methods, this.elems has type rep List.
rep type and F is a peer type,
then the combination is a rep type.
For example, (this.elems).head has type rep Node,
because the receiver this.elems has type rep List,
and the type of field head is peer Node.
readonly type.
For example, if e has type readonly List, then
e.head has type readonly Node.
One can also illustrate these rules using method calls.
For example, consider a method lastNode with the following signature.
public peer Node lastNode() |
elems has type rep List,
then a call such as elems.lastNode() has type rep Node
(by case 3).
As another example, consider a method addNode with the
following signature.
public void addNode(peer Node n) |
elems has type rep List,
a call such as elems.addNode(p), requires that p has
type rep Node
(also by case 3),
because the argument, p, has to have the same owner as the
receiver of call, elems, namely this.
The rules are analogous for arrays.
For example, suppose that an instance field a has type
rep readonly Object[].
Then the expression this.a has the same type,
rep readonly Object[] (by case 2).
Similarly, if r has a readonly type,
then r.a would have type
readonly readonly Object[] (by case 4).
Finally, consider a static method that returns a peer object, such as
the following, in a class Cache.
public static peer int[] getInstance() |
peer Cache.getInstance() has type
peer int[]
(by case 1).
Since readonly types are supertypes of the corresponding
rep and peer types, it is possible to do a downcast.
Such a downcast will succeed when the object is in the context
specified by the peer or rep type.
For example, suppose ro has type readonly List.
Then the cast (rep List) ro will succeed only if the
object referenced by ro is owned by this.
The cast (peer List) ro will succeed only if the
object referenced by ro is owned by the owner of this.
Instanceof expressions of the form E instanceof T
yield true when the value of E is not null
and the corresponding cast would succeed.
For example, suppose ro has type readonly List.
Then ro instanceof rep List yields true only if
ro references an object that is owned by this.
Both casts and instanceof expressions have runtime overhead, in general. (Furthermore, as in Java, array updates also generate runtime checks.)
See [Dietl-Drossopoulou-Mueller07] [Dietl-Mueller-Schregenberger08] for a complete list of the Universe type system rules and the different supported compiler options.
| [ << ] | [ >> ] | [Top] | [Contents] | [Index] | [ ? ] |