Reference aliasing

Two program references designate the same mutable object or overlapping mutable state. Binary-update contracts must account for this possibility: an update intended to combine two old values should snapshot both operands before modifying the receiver. A frame condition preserving a distinct operand cannot literally preserve a second reference that aliases the modified receiver.