To the reader: four prerequisites for understanding the following technical rules are:
  1. knowing what null references are,
  2. knowing the distinction between mutable and immutable types,
  3. knowing what aliased variables are, and
  4. knowing what a distinguished argument (i.e., a receiver object) is.
Until you know and fully understand these four concepts, please ignore what follows.

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.