LARA This is an old revision of the document! Semantics of Array Manipulations Suggest an attempt to model Java arrays. Example: a = new T[10]; b = new T[10]; a = b; i = j; a[i] = 1; b[j] = 2; assert a[i]==1; One possible model: arrays ::