LARA

Semantics of Array Manipulations

Suggest an attempt to model Java arrays.

Example:

a = new T[10];
b = new T[10];

a[i] = 1;
b[j] = 2;
assert a[i]==1;

One possible model:

What is desugaring of a[i]=x ?