This is an old revision of the document!
Semantics of Dynamic Object Allocation
x = new()
Example program we wish we can prove:
x = new();
y = new();
assert (x != y);
Also:
assume (ALL n. next n != x);
y = new();
assert (ALL n. next n != x);
Solution:
x = new();
Becomes:
assume (x1 notin S);
x := x1;
S = S U {x1};
for fresh variable x1.
We obtain formulas with sets, in FOL eliminate them using quantifiers.