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/09 16:10]
ersoy
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 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]].