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. (n : alloc --> next n != x));
y = new();
assume (ALL n. (n : alloc --> 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 as in Deciding a language of sets and relations.