LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
sav08:semantics_of_dynamic_object_allocation [2009/03/18 10:47]
vkuncak 		sav08:semantics_of_dynamic_object_allocation [2009/03/18 10:48] (current)
vkuncak
Line 7: Line 7:
    y = new();    y = new();
    ​assert (x != y);    ​assert (x != y);
- 
-Also: 
-  assume (ALL n. (n : alloc --> next n != x)); 
-  y = new(); 
-  assume (ALL n. (n : alloc --> next n != x)); 
  
 Solution: ++++| Solution: ++++|
Line 21: Line 16:
 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]].