- knowing what
null
references are, - knowing the distinction between mutable and immutable types,
- knowing what aliased variables are, and
- knowing what a distinguished argument (i.e., a receiver object) is.
Some package-wide conventions stated here establish some additional preconditions for all methods beyond those stated explicitly in the method contracts.
First, no argument passed to a parameter shall have the value null
.
Second, no two mutable arguments shall be the same reference. That
is to say, if a
and b
are any two
mutable arguments to the same method, even if one of them is the
distinguished argument (i.e., the receiver object), a
!= b
.
Additionally, unless stated otherwise for a particular component,
there are requirements on client behavior with respect to aliases
that are advertised in the contracts. In the foregoing, let rcv
be a variable whose value is a reference to the receiver object
upon which the method bar
that advertises the alias
has been called. Let ali
be a variable now holding
that advertised alias. The requirements stated below reflect the
idea that the object referenced by rcv
owns the
object referenced by ali
, which is, for a short time,
borrowing that object. Consider the abstract value of the object
referenced by ali
immediately after calling method bar
on rcv
. This value is this object's restoration
value. Immediately after calling bar
on rcv
,
the client has the privilege of passing ali
to
methods as an argument (but only if the called method does not
advertise aliasing of the argument and does not also have rcv
as an argument) only until the next occurrence of rcv
being passed as an argument to some method, at which time the
object referred to by ali
must have been restored to
its restoration value. Furthermore, any subsequent use by any
client code that would dereference or otherwise follow the alias
is forbidden.