Semantics of Dynamic Object Allocation
x = new()
Example program we wish we can prove:
x = new(); y = new(); assert (x != y);
What should we assume about references to and from allocated objects?
We obtain formulas with sets, in FOL eliminate them using quantifiers as in Deciding a language of sets and relations.