LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
Next revision 		Previous revision
sav08:semantics_of_dynamic_object_allocation [2008/04/08 23:34]
vkuncak 		sav08:semantics_of_dynamic_object_allocation [2009/03/18 10:48]
vkuncak
Line 7: Line 7:
    y = new();    y = new();
    ​assert (x != y);    ​assert (x != y);
- 
-Also: 
-  assume (ALL n. next n != x); 
-  y = new(); 
-  assert (ALL n. next n != x); 
  
 Solution: ++++| Solution: ++++|
Line 17: Line 12:
 Becomes: Becomes:
   assume (x1 notin S);   assume (x1 notin S);
-  x := x1;+  x = x1;
   S = S U {x1};   S = S U {x1};
 for fresh variable x1. for fresh variable x1.
 ++++ ++++
 +
 +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]]. We obtain formulas with sets, in FOL eliminate them using quantifiers as in [[Deciding a language of sets and relations]].